File tree 2 files changed +16
-0
lines changed
2 files changed +16
-0
lines changed Original file line number Diff line number Diff line change 8
8
#undef time
9
9
10
10
time_t __VERIFIER_nondet_time_t (void );
11
+ time_t __time64 (time_t * );
11
12
12
13
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 )
13
28
{
14
29
time_t res = __VERIFIER_nondet_time_t ();
15
30
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
63
63
perl -p -i -e ' s/^__fread_chk\n//' __functions # fread-01/__fread_chk.desc
64
64
perl -p -i -e ' s/^__printf_chk\n//' __functions # printf-01/__printf_chk.desc
65
65
perl -p -i -e ' s/^__syslog_chk\n//' __functions # syslog-01/__syslog_chk.desc
66
+ perl -p -i -e ' s/^__time64\n//' __functions # time
66
67
perl -p -i -e ' s/^__vfprintf_chk\n//' __functions # vfprintf-01/__vfprintf_chk.desc
67
68
68
69
# Some functions are covered by tests in other folders:
You can’t perform that action at this time.
0 commit comments