From 48edefe223c9292f8388182201a40fb3a8fdefac Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 11 Nov 2025 10:03:18 +0000
Subject: [PATCH] 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
---
 .../cbmc-library/clock_gettime-01/main.c      | 60 ++++++++++++++++++
 .../cbmc-library/clock_gettime-01/test.desc   |  8 +++
 src/ansi-c/library/time.c                     | 61 +++++++++++++++++++
 3 files changed, 129 insertions(+)
 create mode 100644 regression/cbmc-library/clock_gettime-01/main.c
 create mode 100644 regression/cbmc-library/clock_gettime-01/test.desc

diff --git a/regression/cbmc-library/clock_gettime-01/main.c b/regression/cbmc-library/clock_gettime-01/main.c
new file mode 100644
index 00000000000..0d0d669294c
--- /dev/null
+++ b/regression/cbmc-library/clock_gettime-01/main.c
@@ -0,0 +1,60 @@
+#include <assert.h>
+#include <errno.h>
+#include <stdint.h>
+#include <time.h>
+
+// 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;
+}
diff --git a/regression/cbmc-library/clock_gettime-01/test.desc b/regression/cbmc-library/clock_gettime-01/test.desc
new file mode 100644
index 00000000000..96c9b4bcd7b
--- /dev/null
+++ b/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
diff --git a/src/ansi-c/library/time.c b/src/ansi-c/library/time.c
index 7f9e141a0ce..a68ae59c758 100644
--- a/src/ansi-c/library/time.c
+++ b/src/ansi-c/library/time.c
@@ -280,3 +280,64 @@ __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
+  if(!tp)
+  {
+    errno = EFAULT;
+    return -1;
+  }
+
+  // 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;
+  }
+}