Skip to content

Commit 04a4a51

Browse files
authored
Merge pull request #8268 from tautschnig/features/time64
C library: add __time64
2 parents 2324d8c + 7fd92dd commit 04a4a51

File tree

2 files changed

+16
-0
lines changed

2 files changed

+16
-0
lines changed

src/ansi-c/library/time.c

+15
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,23 @@
88
#undef time
99

1010
time_t __VERIFIER_nondet_time_t(void);
11+
time_t __time64(time_t *);
1112

1213
time_t time(time_t *tloc)
14+
{
15+
return __time64(tloc);
16+
}
17+
18+
/* FUNCTION: __time64 */
19+
20+
#ifndef __CPROVER_TIME_H_INCLUDED
21+
# include <time.h>
22+
# define __CPROVER_TIME_H_INCLUDED
23+
#endif
24+
25+
time_t __VERIFIER_nondet_time_t(void);
26+
27+
time_t __time64(time_t *tloc)
1328
{
1429
time_t res=__VERIFIER_nondet_time_t();
1530
if(tloc)

src/ansi-c/library_check.sh

+1
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,7 @@ perl -p -i -e 's/^__fprintf_chk\n//' __functions # fprintf-01/__fprintf_chk.desc
6363
perl -p -i -e 's/^__fread_chk\n//' __functions # fread-01/__fread_chk.desc
6464
perl -p -i -e 's/^__printf_chk\n//' __functions # printf-01/__printf_chk.desc
6565
perl -p -i -e 's/^__syslog_chk\n//' __functions # syslog-01/__syslog_chk.desc
66+
perl -p -i -e 's/^__time64\n//' __functions # time
6667
perl -p -i -e 's/^__vfprintf_chk\n//' __functions # vfprintf-01/__vfprintf_chk.desc
6768

6869
# Some functions are covered by tests in other folders:

0 commit comments

Comments
 (0)