Add clock_gettime model

Add a library model for `clock_gettime`:
- Model follows POSIX specification with proper error handling
- Non-deterministic behavior covers both success and failure paths
- Validates timespec structure with appropriate constraints
- Sets errno correctly (EFAULT for null pointer, EINVAL on failure)

Fixes: #7639

Author: tautschnig

regression/cbmc-library/clock_gettime-01/main.c

@@ -0,0 +1,68 @@
+#include <assert.h>
+#include <errno.h>
+#include <stdint.h>
+#include <time.h>
+
+// MSVC doesn't have CLOCK_* macros
+#ifndef CLOCK_MONOTONIC
+#  define CLOCK_MONOTONIC 1
+#endif
+#ifndef CLOCK_REALTIME
+#  define CLOCK_REALTIME 1
+#endif
+
+// Test function from the issue description
+uint32_t my_time(void)
+{
+  struct timespec t;
+  int ret = clock_gettime(CLOCK_MONOTONIC, &t);
+
+  // If clock_gettime fails, return a safe value
+  if(ret != 0)
+  {
+    return 0;
+  }
+
+  return (t.tv_nsec / 1000000) + ((t.tv_sec % 86400) * 1000);
+}
+
+int main()
+{
+  // Test null pointer behavior
+  int result_null = clock_gettime(CLOCK_REALTIME, 0);
+  if(result_null == -1)
+  {
+    // errno should be set to EFAULT for null pointer
+    assert(errno == EFAULT);
+  }
+
+  struct timespec ts;
+
+  // Test basic functionality with different clock types
+  int result1 = clock_gettime(CLOCK_REALTIME, &ts);
+  assert(result1 == 0 || result1 == -1);
+
+  if(result1 == 0)
+  {
+    // If successful, tv_nsec should be in valid range
+    assert(ts.tv_nsec >= 0 && ts.tv_nsec <= 999999999L);
+  }
+
+  // Test with CLOCK_MONOTONIC
+  int result2 = clock_gettime(CLOCK_MONOTONIC, &ts);
+  assert(result2 == 0 || result2 == -1);
+
+  if(result2 == 0)
+  {
+    // If successful, tv_nsec should be in valid range
+    assert(ts.tv_nsec >= 0 && ts.tv_nsec <= 999999999L);
+  }
+
+  // Test the my_time function from the issue
+  // Note: my_time() handles the failure case internally
+  uint32_t time_result = my_time();
+  // Should return either 0 (on failure) or valid millisecond value within a day
+  assert(time_result < 86400000 || time_result == 0);
+
+  return 0;
+}

regression/cbmc-library/clock_gettime-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/library/time.c

@@ -280,3 +280,68 @@ __CPROVER_size_t _strftime(
   s[length] = '\0';
   return length;
 }
+
+/* FUNCTION: clock_gettime */
+
+#ifndef __CPROVER_TIME_H_INCLUDED
+#  include <time.h>
+#  define __CPROVER_TIME_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+int __VERIFIER_nondet_int(void);
+time_t __VERIFIER_nondet_time_t(void);
+long __VERIFIER_nondet_long(void);
+
+int clock_gettime(clockid_t clockid, struct timespec *tp)
+{
+__CPROVER_HIDE:;
+
+  // Use the clockid parameter (all clock types are modeled the same way)
+  (void)clockid;
+
+  // Check for null pointer - should set errno to EFAULT
+  // Some systems have C headers where `tp` is annotated to be nonnull
+#pragma GCC diagnostic push
+#pragma GCC diagnostic ignored "-Wnonnull-compare"
+  if(!tp)
+  {
+    errno = EFAULT;
+    return -1;
+  }
+#pragma GCC diagnostic pop
+
+  // Non-deterministically choose success or failure
+  int result = __VERIFIER_nondet_int();
+
+  if(result == 0)
+  {
+    // Success case: fill in the timespec structure with non-deterministic but valid values
+    time_t sec = __VERIFIER_nondet_time_t();
+    // Assume reasonable time values (non-negative for typical use cases)
+    __CPROVER_assume(sec >= 0);
+    tp->tv_sec = sec;
+
+    // Nanoseconds should be between 0 and 999,999,999
+    long nanosec = __VERIFIER_nondet_long();
+    __CPROVER_assume(nanosec >= 0 && nanosec <= 999999999L);
+    tp->tv_nsec = nanosec;
+
+    return 0;
+  }
+  else
+  {
+    // Failure case: set errno and return -1
+    int error_code = __VERIFIER_nondet_int();
+    // Most common error codes for clock_gettime
+    __CPROVER_assume(
+      error_code == EINVAL || error_code == EACCES || error_code == ENODEV ||
+      error_code == ENOTSUP || error_code == EOVERFLOW || error_code == EPERM);
+    errno = error_code;
+    return -1;
+  }
+}