diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 36de74a9f38df23c208828edc7d84fa141a14027..509d0627ae8b5724d772b34288850461b48a0cf7 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -293,6 +293,7 @@ share/libc/syslog.h: CEA_LGPL
share/libc/termios.h: CEA_LGPL
share/libc/tgmath.h: CEA_LGPL
share/libc/time.h: CEA_LGPL
+share/libc/time.c: CEA_LGPL
share/libc/uchar.h: CEA_LGPL
share/libc/unistd.h: CEA_LGPL
share/libc/utime.h: CEA_LGPL
diff --git a/share/libc/time.c b/share/libc/time.c
new file mode 100644
index 0000000000000000000000000000000000000000..5873b4c76d2491dc09ccb183b21a81a34b41045f
--- /dev/null
+++ b/share/libc/time.c
@@ -0,0 +1,37 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2018 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#include "time.h"
+#include "__fc_builtin.h"
+__PUSH_FC_STDLIB
+
+extern char __fc_ctime[26];
+
+extern char *ctime(const time_t *timer) {
+ //@ assert \valid_read(timer);
+ //@ assert \initialized(timer);
+ Frama_C_make_unknown(__fc_ctime, 26);
+ __fc_ctime[25] = 0;
+ return __fc_ctime;
+}
+
+__POP_FC_STDLIB
diff --git a/share/libc/time.h b/share/libc/time.h
index eaedd90b305382315161acbbb68cf4a79c3960cb..9ca1d0cadab05c06e25d70c1771262e87be61a89 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -104,8 +104,19 @@ extern time_t mktime(struct tm *timeptr);
*/
extern time_t time(time_t *timer);
+char __fc_ctime[26];
+char * const __fc_p_ctime = &__fc_ctime;
+
extern char *asctime(const struct tm *timeptr);
+/*@
+ requires valid_timer: \valid_read(timer);
+ requires initialization:init_timer: \initialized(timer);
+ assigns __fc_ctime[0..25] \from indirect:*timer, indirect:__fc_time;
+ assigns \result \from indirect:*timer, indirect:__fc_time, __fc_p_ctime;
+ ensures result_points_to_ctime: \result == __fc_p_ctime;
+ ensures result_valid_string: valid_read_string(__fc_p_ctime);
+*/
extern char *ctime(const time_t *timer);
struct tm __fc_time_tm;
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index c20ad3c51dd3215ec23183ee400ac4ffd9809d77..ffa163ed517ced7ae131d1bd9f87f61300909256 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -37,7 +37,7 @@
wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call);
wmemset (0 call);
- Undefined functions (357)
+ Undefined functions (358)
=========================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_abort (1 call); Frama_C_char_interval (0 call);
@@ -74,29 +74,29 @@
clearerr (0 call); clearerr_unlocked (0 call); clock (0 call);
clock_gettime (0 call); clock_nanosleep (0 call); close (0 call);
closedir (0 call); closelog (0 call); connect (0 call); cos (0 call);
- cosf (0 call); cosl (0 call); creat (0 call); difftime (0 call);
- div (0 call); dup (0 call); dup2 (0 call); execl (0 call); execle (0 call);
- execlp (0 call); execv (0 call); execve (0 call); execvp (0 call);
- exit (0 call); exp (0 call); expf (0 call); fabsl (0 call); fclose (0 call);
- fcntl (0 call); fdopen (0 call); feof (2 calls); feof_unlocked (0 call);
- ferror (2 calls); ferror_unlocked (0 call); fflush (0 call); fgetc (1 call);
- fgetpos (0 call); fgets (0 call); fgetws (0 call); fileno (0 call);
- fileno_unlocked (0 call); flock (0 call); flockfile (0 call);
- floor (0 call); floorf (0 call); floorl (0 call); fmod (0 call);
- fmodf (0 call); fopen (0 call); fork (0 call); fputc (0 call);
- fputs (0 call); fread (0 call); free (1 call); freeaddrinfo (0 call);
- freopen (0 call); fseek (0 call); fsetpos (0 call); ftell (0 call);
- ftrylockfile (0 call); funlockfile (0 call); fwrite (0 call);
- gai_strerror (0 call); getc (0 call); getc_unlocked (0 call);
- getchar (0 call); getchar_unlocked (0 call); getcwd (0 call);
- getegid (0 call); geteuid (0 call); getgid (0 call); gethostname (0 call);
- getitimer (0 call); getopt (0 call); getopt_long (0 call);
- getopt_long_only (0 call); getpid (0 call); getppid (0 call);
- getpriority (0 call); getpwuid (0 call); getresgid (0 call);
- getresuid (0 call); getrlimit (0 call); getrusage (0 call); gets (0 call);
- getsid (0 call); getsockopt (0 call); gettimeofday (0 call);
- getuid (0 call); gmtime (0 call); htonl (0 call); htons (0 call);
- iconv (0 call); iconv_close (0 call); iconv_open (0 call);
+ cosf (0 call); cosl (0 call); creat (0 call); ctime (0 call);
+ difftime (0 call); div (0 call); dup (0 call); dup2 (0 call);
+ execl (0 call); execle (0 call); execlp (0 call); execv (0 call);
+ execve (0 call); execvp (0 call); exit (0 call); exp (0 call);
+ expf (0 call); fabsl (0 call); fclose (0 call); fcntl (0 call);
+ fdopen (0 call); feof (2 calls); feof_unlocked (0 call); ferror (2 calls);
+ ferror_unlocked (0 call); fflush (0 call); fgetc (1 call); fgetpos (0 call);
+ fgets (0 call); fgetws (0 call); fileno (0 call); fileno_unlocked (0 call);
+ flock (0 call); flockfile (0 call); floor (0 call); floorf (0 call);
+ floorl (0 call); fmod (0 call); fmodf (0 call); fopen (0 call);
+ fork (0 call); fputc (0 call); fputs (0 call); fread (0 call);
+ free (1 call); freeaddrinfo (0 call); freopen (0 call); fseek (0 call);
+ fsetpos (0 call); ftell (0 call); ftrylockfile (0 call);
+ funlockfile (0 call); fwrite (0 call); gai_strerror (0 call); getc (0 call);
+ getc_unlocked (0 call); getchar (0 call); getchar_unlocked (0 call);
+ getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call);
+ gethostname (0 call); getitimer (0 call); getopt (0 call);
+ getopt_long (0 call); getopt_long_only (0 call); getpid (0 call);
+ getppid (0 call); getpriority (0 call); getpwuid (0 call);
+ getresgid (0 call); getresuid (0 call); getrlimit (0 call);
+ getrusage (0 call); gets (0 call); getsid (0 call); getsockopt (0 call);
+ gettimeofday (0 call); getuid (0 call); gmtime (0 call); htonl (0 call);
+ htons (0 call); iconv (0 call); iconv_close (0 call); iconv_open (0 call);
inet_addr (0 call); inet_ntoa (0 call); inet_ntop (0 call);
inet_pton (0 call); isascii (0 call); kill (0 call); labs (0 call);
ldiv (0 call); listen (0 call); llabs (0 call); lldiv (0 call);
@@ -163,13 +163,13 @@
==============
Sloc = 948
Decision point = 183
- Global variables = 52
+ Global variables = 54
If = 174
Loop = 40
Goto = 78
Assignment = 379
Exit point = 73
- Function = 430
+ Function = 431
Function call = 73
Pointer dereferencing = 146
Cyclomatic complexity = 256
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 7df313ff573d895684146f84abed98e0fc6a2906..067e748dee0d9bac5c07fd617c82abee7f0a29b4 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -5137,6 +5137,20 @@ extern time_t mktime(struct tm *timeptr);
*/
extern time_t time(time_t *timer);
+char __fc_ctime[26];
+char * const __fc_p_ctime = (char *)(& __fc_ctime);
+/*@ requires valid_timer: \valid_read(timer);
+ requires initialization: init_timer: \initialized(timer);
+ ensures result_points_to_ctime: \result ≡ __fc_p_ctime;
+ ensures result_valid_string: valid_read_string(__fc_p_ctime);
+ assigns __fc_ctime[0 .. 25], \result;
+ assigns __fc_ctime[0 .. 25]
+ \from (indirect: *timer), (indirect: __fc_time);
+ assigns \result
+ \from (indirect: *timer), (indirect: __fc_time), __fc_p_ctime;
+ */
+extern char *ctime(time_t const *timer);
+
struct tm __fc_time_tm;
struct tm * const __fc_p_time_tm = & __fc_time_tm;
/*@ ensures
diff --git a/tests/libc/oracle/time_c.res.oracle b/tests/libc/oracle/time_c.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2b6021a7f03a5dd174de37138c6d674ede2e1b88
--- /dev/null
+++ b/tests/libc/oracle/time_c.res.oracle
@@ -0,0 +1,34 @@
+[kernel] Parsing tests/libc/time_c.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ v ∈ [--..--]
+[eva] computing for function ctime <- main.
+ Called from tests/libc/time_c.c:8.
+[eva] share/libc/time.c:30: assertion got status valid.
+[eva:alarm] share/libc/time.c:31: Warning: assertion got status unknown.
+[eva] computing for function Frama_C_make_unknown <- ctime <- main.
+ Called from share/libc/time.c:32.
+[eva] using specification for function Frama_C_make_unknown
+[eva] share/libc/time.c:32:
+ function Frama_C_make_unknown: precondition 'valid_p' got status valid.
+[eva] Done for function Frama_C_make_unknown
+[eva] Recording results for ctime
+[eva] Done for function ctime
+[eva] tests/libc/time_c.c:9: assertion got status valid.
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function ctime:
+ __fc_ctime[0..24] ∈ [--..--]
+ [25] ∈ {0}
+ Frama_C_entropy_source ∈ [--..--]
+ __retres ∈ {{ &__fc_ctime[0] }}
+[eva:final-states] Values at end of function main:
+ __fc_ctime[0..24] ∈ [--..--]
+ [25] ∈ {0}
+ Frama_C_entropy_source ∈ [--..--]
+ t ∈ {42}
+ s ∈ {{ &__fc_ctime[0] }}
+ __retres ∈ {0}
diff --git a/tests/libc/oracle/time_h.res.oracle b/tests/libc/oracle/time_h.res.oracle
index dd05409c1abbb38d6e69d462c654f258af058285..5fcd6c6d027bc01e634adfc623934e6e724e7607 100644
--- a/tests/libc/oracle/time_h.res.oracle
+++ b/tests/libc/oracle/time_h.res.oracle
@@ -102,14 +102,29 @@
[eva] computing for function clock_nanosleep <- main.
Called from tests/libc/time_h.c:36.
[eva] Done for function clock_nanosleep
+[eva] computing for function ctime <- main.
+ Called from tests/libc/time_h.c:43.
+[eva] using specification for function ctime
+[eva] tests/libc/time_h.c:43:
+ function ctime: precondition 'valid_timer' got status valid.
+[eva] tests/libc/time_h.c:43:
+ function ctime: precondition 'initialization,init_timer' got status valid.
+[eva] Done for function ctime
+[eva] computing for function ctime <- main.
+ Called from tests/libc/time_h.c:43.
+[eva] Done for function ctime
+[eva:alarm] tests/libc/time_h.c:44: Warning: assertion got status unknown.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+ __fc_ctime[0..25] ∈ [--..--]
req.tv_sec ∈ [--..--]
.tv_nsec ∈ [0..999999999]
rem ∈ [--..--] or UNINITIALIZED
r ∈ {-1; 0; 4; 22}
creq.tv_sec ∈ [--..--] or UNINITIALIZED
.tv_nsec ∈ [0..999999999] or UNINITIALIZED
+ tt ∈ {42}
+ time_str ∈ {{ &__fc_ctime[0] }}
__retres ∈ {0; 1; 2}
diff --git a/tests/libc/oracle/time_misc.res.oracle b/tests/libc/oracle/time_misc.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..11b3437a14bb4490511094ca437543e11a7ed99e
--- /dev/null
+++ b/tests/libc/oracle/time_misc.res.oracle
@@ -0,0 +1,71 @@
+[kernel] Parsing tests/libc/time_misc.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ v ∈ [--..--]
+[eva] computing for function test_gettimeofday <- main.
+ Called from tests/libc/time_misc.c:37.
+[eva] computing for function gettimeofday <- test_gettimeofday <- main.
+ Called from tests/libc/time_misc.c:7.
+[eva] using specification for function gettimeofday
+[eva] Done for function gettimeofday
+[eva] tests/libc/time_misc.c:8: assertion got status valid.
+[eva] tests/libc/time_misc.c:9: assertion got status valid.
+[eva] Recording results for test_gettimeofday
+[eva] Done for function test_gettimeofday
+[eva] computing for function test_strftime <- main.
+ Called from tests/libc/time_misc.c:38.
+[eva] computing for function time <- test_strftime <- main.
+ Called from tests/libc/time_misc.c:18.
+[eva] using specification for function time
+[eva] Done for function time
+[eva] computing for function localtime <- test_strftime <- main.
+ Called from tests/libc/time_misc.c:19.
+[eva] using specification for function localtime
+[eva] Done for function localtime
+[eva] computing for function strftime <- test_strftime <- main.
+ Called from tests/libc/time_misc.c:21.
+[eva] using specification for function strftime
+[eva] tests/libc/time_misc.c:21:
+ function strftime: precondition 'dst_has_room' got status valid.
+[eva] tests/libc/time_misc.c:21:
+ function strftime: precondition 'valid_format' got status valid.
+[eva] tests/libc/time_misc.c:21:
+ function strftime: precondition 'valid_tm' got status valid.
+[eva] Done for function strftime
+[eva] Recording results for test_strftime
+[eva] Done for function test_strftime
+[eva] computing for function test_ctime <- main.
+ Called from tests/libc/time_misc.c:39.
+[eva] computing for function ctime <- test_ctime <- main.
+ Called from tests/libc/time_misc.c:31.
+[eva] using specification for function ctime
+[eva] tests/libc/time_misc.c:31:
+ function ctime: precondition 'valid_timer' got status valid.
+[eva:alarm] tests/libc/time_misc.c:31: Warning:
+ function ctime: precondition 'initialization,init_timer' got status unknown.
+[eva] Done for function ctime
+[eva:alarm] tests/libc/time_misc.c:32: Warning: assertion got status unknown.
+[eva] Recording results for test_ctime
+[eva] Done for function test_ctime
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function test_ctime:
+ __fc_ctime[0..25] ∈ [--..--]
+ t ∈ {42}
+ s ∈ {{ &__fc_ctime[0] }}
+[eva:final-states] Values at end of function test_gettimeofday:
+ tv.tv_sec ∈ [--..--]
+ .tv_usec ∈ [0..999999]
+[eva:final-states] Values at end of function test_strftime:
+ __fc_time_tm ∈ [--..--]
+ outstr[0..199] ∈ [--..--] or UNINITIALIZED
+ t ∈ [--..--]
+ tmp ∈ {{ NULL ; &__fc_time_tm }}
+ res ∈ [0..200] or UNINITIALIZED
+[eva:final-states] Values at end of function main:
+ __fc_ctime[0..25] ∈ [--..--]
+ __fc_time_tm ∈ [--..--]
+ __retres ∈ {0}
diff --git a/tests/libc/time_c.c b/tests/libc/time_c.c
new file mode 100644
index 0000000000000000000000000000000000000000..c833527b0c07b22bd568457b94bd7dcfd628de3a
--- /dev/null
+++ b/tests/libc/time_c.c
@@ -0,0 +1,12 @@
+#include "time.c"
+
+volatile int v;
+
+int main() {
+ time_t t;
+ if (v) t = 42;
+ char *s = ctime(&t); // warn about initialization
+ //@ assert valid_read_string(s);
+
+ return 0;
+}
diff --git a/tests/libc/time_h.c b/tests/libc/time_h.c
index a265f44be03db228fa54b67a63d79090dc19650a..0ce0180a8c7a2892d0da7f2dafafa7c3fd04bc8b 100644
--- a/tests/libc/time_h.c
+++ b/tests/libc/time_h.c
@@ -38,5 +38,9 @@ int main() {
return 1;
}
}
+
+ time_t tt = 42;
+ char *time_str = ctime(&tt);
+ //@ assert valid_string(time_str);
return 0;
}
diff --git a/tests/libc/time.c b/tests/libc/time_misc.c
similarity index 78%
rename from tests/libc/time.c
rename to tests/libc/time_misc.c
index 5cec32d3ff1ffa35b917686439a78c60f5a807df..8123a1641dc5e5ff829cde5f958e3b14d5f24656 100644
--- a/tests/libc/time.c
+++ b/tests/libc/time_misc.c
@@ -22,10 +22,21 @@ void test_strftime(void)
}
}
+volatile int v;
+
+void test_ctime(void)
+{
+ time_t t;
+ if (v) t = 42;
+ char *s = ctime(&t); // warn about initialization
+ //@ assert valid_read_string(s);
+}
+
int main(int argc, char **argv)
{
test_gettimeofday();
test_strftime();
+ test_ctime();
return 0;
}