Skip to content

Commit c6f1ed5

Browse files
committed
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.
1 parent 4bd3c2f commit c6f1ed5

File tree

3 files changed

+9
-4
lines changed

3 files changed

+9
-4
lines changed

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

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,11 @@
33

44
int main()
55
{
6-
time();
7-
assert(0);
6+
time_t t1 = time(0);
7+
8+
time_t t;
9+
time_t t2 = time(&t);
10+
assert(t2 == t);
11+
812
return 0;
913
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

src/ansi-c/library/time.c

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,8 @@ time_t __VERIFIER_nondet_time_t();
1212
time_t time(time_t *tloc)
1313
{
1414
time_t res=__VERIFIER_nondet_time_t();
15-
if(!tloc) *tloc=res;
15+
if(tloc)
16+
*tloc = res;
1617
return res;
1718
}
1819

0 commit comments

Comments
 (0)