[Libc] fix libc spec: utimes; add test

share/libc/sys/time.h

@@ -47,8 +47,9 @@ struct timezone {
 
 /*@
   requires valid_path: valid_read_string(path);
-  requires valid_times: \valid_read(times+(0..1));
-  assigns \result \from indirect:path[0..strlen(path)], indirect:times[0..1];
+  requires valid_times_or_null: \valid_read(times+(0..1)) || times == \null;
+  assigns \result \from indirect:path[0..strlen(path)],
+    indirect:times, indirect:times[0..1];
 */
 extern int utimes(const char *path, const struct timeval times[2]);
 

tests/libc/oracle/sys_time.res.oracle → tests/libc/oracle/sys_time_h.res.oracle

-[kernel] Parsing tests/libc/sys_time.c (with preprocessing)
+[kernel] Parsing tests/libc/sys_time_h.c (with preprocessing)
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
 [eva] computing for function setitimer <- main.
-  Called from tests/libc/sys_time.c:6.
+  Called from tests/libc/sys_time_h.c:6.
 [eva] using specification for function setitimer
-[eva] tests/libc/sys_time.c:6: 
+[eva] tests/libc/sys_time_h.c:6: 
   function setitimer: precondition 'valid_new_value' got status valid.
-[eva] tests/libc/sys_time.c:6: 
+[eva] tests/libc/sys_time_h.c:6: 
   function setitimer: precondition 'old_value_null_or_valid' got status valid.
-[eva:invalid-assigns] tests/libc/sys_time.c:6: 
+[eva:invalid-assigns] tests/libc/sys_time_h.c:6: 
   Completely invalid destination for assigns clause *old_value. Ignoring.
 [eva] Done for function setitimer
-[eva] tests/libc/sys_time.c:7: assertion got status valid.
+[eva] tests/libc/sys_time_h.c:7: assertion got status valid.
 [eva] computing for function setitimer <- main.
-  Called from tests/libc/sys_time.c:9.
-[eva] tests/libc/sys_time.c:9: 
+  Called from tests/libc/sys_time_h.c:9.
+[eva] tests/libc/sys_time_h.c:9: 
   function setitimer: precondition 'valid_new_value' got status valid.
-[eva] tests/libc/sys_time.c:9: 
+[eva] tests/libc/sys_time_h.c:9: 
   function setitimer: precondition 'old_value_null_or_valid' got status valid.
 [eva] Done for function setitimer
-[eva] tests/libc/sys_time.c:10: assertion got status valid.
-[eva] tests/libc/sys_time.c:11: assertion got status valid.
+[eva] tests/libc/sys_time_h.c:10: assertion got status valid.
+[eva] tests/libc/sys_time_h.c:11: assertion got status valid.
 [eva] computing for function getitimer <- main.
-  Called from tests/libc/sys_time.c:12.
+  Called from tests/libc/sys_time_h.c:12.
 [eva] using specification for function getitimer
-[eva] tests/libc/sys_time.c:12: 
+[eva] tests/libc/sys_time_h.c:12: 
   function getitimer: precondition 'valid_curr_value' got status valid.
 [eva] Done for function getitimer
-[eva] tests/libc/sys_time.c:13: assertion got status valid.
-[eva] tests/libc/sys_time.c:14: assertion got status valid.
+[eva] tests/libc/sys_time_h.c:13: assertion got status valid.
+[eva] tests/libc/sys_time_h.c:14: assertion got status valid.
 [eva] computing for function getitimer <- main.
-  Called from tests/libc/sys_time.c:16.
-[eva] tests/libc/sys_time.c:16: 
+  Called from tests/libc/sys_time_h.c:16.
+[eva] tests/libc/sys_time_h.c:16: 
   function getitimer: precondition 'valid_curr_value' got status valid.
 [eva] Done for function getitimer
-[eva] tests/libc/sys_time.c:17: assertion got status valid.
+[eva] tests/libc/sys_time_h.c:17: assertion got status valid.
 [eva] computing for function setitimer <- main.
-  Called from tests/libc/sys_time.c:19.
-[eva] tests/libc/sys_time.c:19: 
+  Called from tests/libc/sys_time_h.c:19.
+[eva] tests/libc/sys_time_h.c:19: 
   function setitimer: precondition 'valid_new_value' got status valid.
-[eva] tests/libc/sys_time.c:19: 
+[eva] tests/libc/sys_time_h.c:19: 
   function setitimer: precondition 'old_value_null_or_valid' got status valid.
 [eva] Done for function setitimer
-[eva] tests/libc/sys_time.c:20: assertion got status valid.
+[eva] tests/libc/sys_time_h.c:20: assertion got status valid.
+[eva] computing for function utimes <- main.
+  Called from tests/libc/sys_time_h.c:22.
+[eva] using specification for function utimes
+[eva] tests/libc/sys_time_h.c:22: 
+  function utimes: precondition 'valid_path' got status valid.
+[eva] tests/libc/sys_time_h.c:22: 
+  function utimes: precondition 'valid_times_or_null' got status valid.
+[eva] Done for function utimes
+[eva] computing for function utimes <- main.
+  Called from tests/libc/sys_time_h.c:28.
+[eva] tests/libc/sys_time_h.c:28: 
+  function utimes: precondition 'valid_path' got status valid.
+[eva] tests/libc/sys_time_h.c:28: 
+  function utimes: precondition 'valid_times_or_null' got status valid.
+[eva] Done for function utimes
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -59,4 +74,10 @@
     .it_interval.tv_usec ∈ {1000000}
     .it_value ∈ [--..--]
   INVALID_ITIMER ∈ {-1}
+  r1 ∈ [--..--]
+  tv[0].tv_sec ∈ {10000000}
+    [0].tv_usec ∈ {999999}
+    [1].tv_sec ∈ {-9000000}
+    [1].tv_usec ∈ {1}
+  r2 ∈ [--..--]
   __retres ∈ {0}

tests/libc/sys_time.c → tests/libc/sys_time_h.c

@@ -18,5 +18,14 @@ int main() {
   i2.it_interval.tv_usec = 1000000; // invalid tv_usec
   res = setitimer(ITIMER_VIRTUAL, &i2, &i1);
   //@ assert res == -1;
+
+  int r1 = utimes("/tmp/utimes", 0);
+  struct timeval tv[2] =
+    {
+     { .tv_sec = 10000000, .tv_usec = 999999 },
+     { .tv_sec = -9000000, .tv_usec = 1 },
+    };
+  int r2 = utimes("/tmp/utimes", tv);
+
   return 0;
 }