From c6f1ed5d379e746bbbdc2b164fef5a3ec9cb0242 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 3 Dec 2020 10:20:29 +0000
Subject: [PATCH] C library/time: fix wrong is-null test

The assignment should happen if the pointer is non-null, not when it is
null. Also test this library function.
---
 regression/cbmc-library/time-01/main.c    | 8 ++++++--
 regression/cbmc-library/time-01/test.desc | 2 +-
 src/ansi-c/library/time.c                 | 3 ++-
 3 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/regression/cbmc-library/time-01/main.c b/regression/cbmc-library/time-01/main.c
index ce78c8e4679..2dc5a9535b9 100644
--- a/regression/cbmc-library/time-01/main.c
+++ b/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;
 }
diff --git a/regression/cbmc-library/time-01/test.desc b/regression/cbmc-library/time-01/test.desc
index 9542d988e8d..96c9b4bcd7b 100644
--- a/regression/cbmc-library/time-01/test.desc
+++ b/regression/cbmc-library/time-01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/src/ansi-c/library/time.c b/src/ansi-c/library/time.c
index 71606de0012..93835781b4c 100644
--- a/src/ansi-c/library/time.c
+++ b/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;
 }