File tree Expand file tree Collapse file tree 2 files changed +16
-0
lines changed
Expand file tree Collapse file tree 2 files changed +16
-0
lines changed Original file line number Diff line number Diff line change 88#undef time
99
1010time_t __VERIFIER_nondet_time_t (void );
11+ time_t __time64 (time_t * );
1112
1213time_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 )
Original file line number Diff line number Diff line change @@ -63,6 +63,7 @@ perl -p -i -e 's/^__fprintf_chk\n//' __functions # fprintf-01/__fprintf_chk.desc
6363perl -p -i -e ' s/^__fread_chk\n//' __functions # fread-01/__fread_chk.desc
6464perl -p -i -e ' s/^__printf_chk\n//' __functions # printf-01/__printf_chk.desc
6565perl -p -i -e ' s/^__syslog_chk\n//' __functions # syslog-01/__syslog_chk.desc
66+ perl -p -i -e ' s/^__time64\n//' __functions # time
6667perl -p -i -e ' s/^__vfprintf_chk\n//' __functions # vfprintf-01/__vfprintf_chk.desc
6768
6869# Some functions are covered by tests in other folders:
You can’t perform that action at this time.
0 commit comments