Merge pull request #5655 from tautschnig/library-time

C library/time: fix wrong is-null test

Author: kroening

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

@@ -3,7 +3,11 @@
 
 int main()
 {
-  time();
-  assert(0);
+  time_t t1 = time(0);
+
+  time_t t;
+  time_t t2 = time(&t);
+  assert(t2 == t);
+
   return 0;
 }

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

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

src/ansi-c/library/time.c

@@ -12,7 +12,8 @@ time_t __VERIFIER_nondet_time_t();
 time_t time(time_t *tloc)
 {
   time_t res=__VERIFIER_nondet_time_t();
-  if(!tloc) *tloc=res;
+  if(tloc)
+    *tloc = res;
   return res;
 }