diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 27d51d73125d488deb50c9b03993abb5f11e6c64..2cb4208b4b8543fdc33daf7ffb990420c03315a2 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -44,7 +44,7 @@
wcscpy (0 call); wcsdup (0 call); wcslen (3 calls); wcsncat (0 call);
wcsncpy (0 call); wmemcpy (1 call); wmemset (0 call);
- Specified-only functions (415)
+ Specified-only functions (416)
==============================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -148,27 +148,27 @@
sigaction (0 call); sigaddset (0 call); sigdelset (0 call);
sigemptyset (0 call); sigfillset (0 call); sigismember (0 call);
siglongjmp (0 call); signal (0 call); sigprocmask (0 call); sin (0 call);
- sinf (0 call); sinl (0 call); socket (0 call); socketpair (0 call);
- sqrt (0 call); sqrtf (0 call); sqrtl (0 call); srand (0 call);
- srand48 (0 call); srandom (0 call); stat (0 call); stpcpy (0 call);
- strcasestr (0 call); strchrnul (0 call); strcoll (0 call); strcspn (0 call);
- strftime (0 call); strlcat (0 call); strlcpy (0 call); strncasecmp (0 call);
- strpbrk (0 call); strsep (0 call); strspn (0 call); strtod (0 call);
- strtof (0 call); strtoimax (0 call); strtok (0 call); strtok_r (0 call);
- strtol (0 call); strtold (0 call); strtoll (0 call); strtoul (0 call);
- strtoull (0 call); strxfrm (0 call); sync (0 call); sysconf (0 call);
- syslog (0 call); system (0 call); tcflush (0 call); tcgetattr (0 call);
- tcsetattr (0 call); time (0 call); times (0 call); tmpfile (0 call);
- tmpnam (0 call); trunc (0 call); truncf (0 call); truncl (0 call);
- ttyname (0 call); tzset (0 call); umask (0 call); uname (0 call);
- ungetc (0 call); unlink (0 call); usleep (0 call); utimes (0 call);
- vfprintf (0 call); vfscanf (0 call); vprintf (0 call); vscanf (0 call);
- vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call); wait (0 call);
- waitpid (0 call); wcscasecmp (0 call); wcschr (0 call); wcscmp (0 call);
- wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call); wcsncmp (0 call);
- wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call); wcsstr (0 call);
- wcstombs (0 call); wctomb (0 call); wmemchr (0 call); wmemcmp (0 call);
- wmemmove (0 call); write (0 call);
+ sinf (0 call); sinl (0 call); sleep (0 call); socket (0 call);
+ socketpair (0 call); sqrt (0 call); sqrtf (0 call); sqrtl (0 call);
+ srand (0 call); srand48 (0 call); srandom (0 call); stat (0 call);
+ stpcpy (0 call); strcasestr (0 call); strchrnul (0 call); strcoll (0 call);
+ strcspn (0 call); strftime (0 call); strlcat (0 call); strlcpy (0 call);
+ strncasecmp (0 call); strpbrk (0 call); strsep (0 call); strspn (0 call);
+ strtod (0 call); strtof (0 call); strtoimax (0 call); strtok (0 call);
+ strtok_r (0 call); strtol (0 call); strtold (0 call); strtoll (0 call);
+ strtoul (0 call); strtoull (0 call); strxfrm (0 call); sync (0 call);
+ sysconf (0 call); syslog (0 call); system (0 call); tcflush (0 call);
+ tcgetattr (0 call); tcsetattr (0 call); time (0 call); times (0 call);
+ tmpfile (0 call); tmpnam (0 call); trunc (0 call); truncf (0 call);
+ truncl (0 call); ttyname (0 call); tzset (0 call); umask (0 call);
+ uname (0 call); ungetc (0 call); unlink (0 call); usleep (0 call);
+ utimes (0 call); vfprintf (0 call); vfscanf (0 call); vprintf (0 call);
+ vscanf (0 call); vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call);
+ wait (0 call); waitpid (0 call); wcscasecmp (0 call); wcschr (0 call);
+ wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
+ wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
+ wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
+ wmemcmp (0 call); wmemmove (0 call); write (0 call);
Undefined and unspecified functions (1)
=======================================
@@ -197,7 +197,7 @@
Goto = 99
Assignment = 466
Exit point = 84
- Function = 500
+ Function = 501
Function call = 98
Pointer dereferencing = 161
Cyclomatic complexity = 299
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 7ede7566e8cec61541875f914b64a6038a2c83e4..6c0be414fd6dc9145f3e6106aa51a3ac0c2448ea 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -1741,6 +1741,12 @@ extern pid_t setsid(void);
*/
extern int setuid(uid_t uid);
+/*@ ensures unslept: 0 ≤ \result ≤ \old(seconds);
+ assigns \result;
+ assigns \result \from seconds;
+ */
+extern unsigned int sleep(unsigned int seconds);
+
/*@ assigns \nothing; */
extern void sync(void);
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index ce170ab4761f6c58b3616ea4f242c97c7524ccec..9a9d6d24921562fb1b27ac6e9b243bb85fe834aa 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -54,13 +54,13 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/libc/netdb_c.c:33: Call to builtin memset
-[eva] tests/libc/netdb_c.c:33:
+[eva] tests/libc/netdb_c.c:25: Call to builtin memset
+[eva] tests/libc/netdb_c.c:25:
function memset: precondition 'valid_s' got status valid.
[eva] share/libc/string.h:121:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[eva] computing for function getaddrinfo <- main.
- Called from tests/libc/netdb_c.c:42.
+ Called from tests/libc/netdb_c.c:34.
[eva] share/libc/netdb.c:56: Call to builtin malloc
[eva] share/libc/netdb.c:56: allocating variable __malloc_getaddrinfo_l56
[eva] share/libc/netdb.c:58: Call to builtin malloc
@@ -142,57 +142,57 @@
[eva] Recording results for getaddrinfo
[eva] Done for function getaddrinfo
[eva] computing for function gai_strerror <- main.
- Called from tests/libc/netdb_c.c:44.
+ Called from tests/libc/netdb_c.c:36.
[eva] using specification for function gai_strerror
[eva] Done for function gai_strerror
[eva] computing for function fprintf_va_1 <- main.
- Called from tests/libc/netdb_c.c:44.
+ Called from tests/libc/netdb_c.c:36.
[eva] using specification for function fprintf_va_1
-[eva] tests/libc/netdb_c.c:44:
+[eva] tests/libc/netdb_c.c:36:
function fprintf_va_1: precondition valid_read_string(format) got status valid.
-[eva] tests/libc/netdb_c.c:44:
+[eva] tests/libc/netdb_c.c:36:
function fprintf_va_1: precondition valid_read_string(param0) got status valid.
[eva] Done for function fprintf_va_1
[eva] computing for function exit <- main.
- Called from tests/libc/netdb_c.c:45.
+ Called from tests/libc/netdb_c.c:37.
[eva] using specification for function exit
[eva] Done for function exit
[eva] computing for function socket <- main.
- Called from tests/libc/netdb_c.c:54.
+ Called from tests/libc/netdb_c.c:46.
[eva] using specification for function socket
[eva] Done for function socket
[eva] computing for function bind <- main.
- Called from tests/libc/netdb_c.c:59.
+ Called from tests/libc/netdb_c.c:51.
[eva] using specification for function bind
-[eva] tests/libc/netdb_c.c:59:
+[eva] tests/libc/netdb_c.c:51:
function bind: precondition 'valid_sockfd,sockfd' got status valid.
-[eva] tests/libc/netdb_c.c:59:
+[eva] tests/libc/netdb_c.c:51:
function bind: precondition 'valid_read_addr' got status valid.
[eva] Done for function bind
[eva] computing for function close <- main.
- Called from tests/libc/netdb_c.c:62.
+ Called from tests/libc/netdb_c.c:54.
[eva] using specification for function close
-[eva] tests/libc/netdb_c.c:62:
+[eva] tests/libc/netdb_c.c:54:
function close: precondition 'valid_fd' got status valid.
[eva] Done for function close
[eva] computing for function fprintf_va_2 <- main.
- Called from tests/libc/netdb_c.c:65.
+ Called from tests/libc/netdb_c.c:57.
[eva] using specification for function fprintf_va_2
-[eva] tests/libc/netdb_c.c:65:
+[eva] tests/libc/netdb_c.c:57:
function fprintf_va_2: precondition got status valid.
[eva] Done for function fprintf_va_2
[eva] computing for function exit <- main.
- Called from tests/libc/netdb_c.c:66.
+ Called from tests/libc/netdb_c.c:58.
[eva] Done for function exit
[eva] computing for function freeaddrinfo <- main.
- Called from tests/libc/netdb_c.c:69.
+ Called from tests/libc/netdb_c.c:61.
[eva] using specification for function freeaddrinfo
-[eva] tests/libc/netdb_c.c:69: Warning: ignoring unsupported \allocates clause
-[eva] tests/libc/netdb_c.c:69:
+[eva] tests/libc/netdb_c.c:61: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/netdb_c.c:61:
function freeaddrinfo: precondition 'addrinfo_valid' got status valid.
[eva] Done for function freeaddrinfo
[eva] computing for function gethostbyname <- main.
- Called from tests/libc/netdb_c.c:71.
+ Called from tests/libc/netdb_c.c:63.
[eva] computing for function res_search <- gethostbyname <- main.
Called from share/libc/netdb.c:141.
[eva] computing for function Frama_C_char_interval <- res_search <-
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index 23bd3f50c5392a7f5ff4ec33796919b99c80672b..55e6a1c528de73a57f89e7f4b640206bc2f38233 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -558,6 +558,14 @@
Called from tests/libc/unistd_h.c:104.
[eva] Done for function pipe
[eva] tests/libc/unistd_h.c:105: check 'ok' got status valid.
+[eva] computing for function sleep <- main.
+ Called from tests/libc/unistd_h.c:107.
+[eva] using specification for function sleep
+[eva] Done for function sleep
+[eva] computing for function sleep <- main.
+ Called from tests/libc/unistd_h.c:107.
+[eva] Done for function sleep
+[eva] tests/libc/unistd_h.c:108: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -585,4 +593,5 @@
tty ∈ {{ NULL ; &__fc_ttyname[0] }}
halfpipe ∈ UNINITIALIZED
pipefd[0..1] ∈ [0..1023] or UNINITIALIZED
+ unslept ∈ [0..42]
__retres ∈ {0; 1}
diff --git a/tests/libc/oracle/unistd_h.1.res.oracle b/tests/libc/oracle/unistd_h.1.res.oracle
index 32c8e8164076a62e38d24dc837301d2d539dd3d8..1ce6be573a566003223a378d330cfdb7e4c1744b 100644
--- a/tests/libc/oracle/unistd_h.1.res.oracle
+++ b/tests/libc/oracle/unistd_h.1.res.oracle
@@ -558,6 +558,14 @@
Called from tests/libc/unistd_h.c:104.
[eva] Done for function pipe
[eva] tests/libc/unistd_h.c:105: check 'ok' got status valid.
+[eva] computing for function sleep <- main.
+ Called from tests/libc/unistd_h.c:107.
+[eva] using specification for function sleep
+[eva] Done for function sleep
+[eva] computing for function sleep <- main.
+ Called from tests/libc/unistd_h.c:107.
+[eva] Done for function sleep
+[eva] tests/libc/unistd_h.c:108: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -585,4 +593,5 @@
tty ∈ {{ NULL ; &__fc_ttyname[0] }}
halfpipe ∈ UNINITIALIZED
pipefd[0..1] ∈ [0..1023] or UNINITIALIZED
+ unslept ∈ [0..42]
__retres ∈ {0; 1}
diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle
index d92d25d82ea958fd39f5c38000f47e44e1bd1080..81dff3785c2b1652942601044ed27093a3858cc1 100644
--- a/tests/metrics/oracle/libc.1.res.oracle
+++ b/tests/metrics/oracle/libc.1.res.oracle
@@ -4,7 +4,7 @@
bar (1 call); f (0 call); foo (1 call); g (address taken) (0 call);
getopt (1 call); h (1 call); main (0 call);
- Specified-only functions (122)
+ Specified-only functions (123)
==============================
_exit (0 call); access (0 call); chdir (0 call); chown (0 call);
chroot (0 call); clearerr (0 call); clearerr_unlocked (0 call);
@@ -34,11 +34,11 @@
seteuid (0 call); setgid (0 call); sethostname (0 call); setpgid (0 call);
setregid (0 call); setresgid (0 call); setresuid (0 call);
setreuid (0 call); setsid (0 call); setuid (0 call); setvbuf (0 call);
- sync (0 call); sysconf (0 call); tmpfile (0 call); tmpnam (0 call);
- tolower (0 call); toupper (0 call); ttyname (0 call); ungetc (0 call);
- unlink (0 call); usleep (0 call); vfprintf (0 call); vfscanf (0 call);
- vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
- write (0 call);
+ sleep (0 call); sync (0 call); sysconf (0 call); tmpfile (0 call);
+ tmpnam (0 call); tolower (0 call); toupper (0 call); ttyname (0 call);
+ ungetc (0 call); unlink (0 call); usleep (0 call); vfprintf (0 call);
+ vfscanf (0 call); vprintf (0 call); vscanf (0 call); vsnprintf (0 call);
+ vsprintf (0 call); write (0 call);
Undefined and unspecified functions (0)
=======================================
@@ -63,7 +63,7 @@
Goto = 0
Assignment = 9
Exit point = 7
- Function = 129
+ Function = 130
Function call = 8
Pointer dereferencing = 1
Cyclomatic complexity = 7
@@ -91,7 +91,7 @@
----------------------------------------------------------------------------
[metrics] Eva coverage statistics
=======================
- Syntactically reachable functions = 8 (out of 129)
+ Syntactically reachable functions = 8 (out of 130)
Semantically reached functions = 8
Coverage estimation = 100.0%
[metrics] References to non-analyzed functions
diff --git a/tests/metrics/oracle/libc.json b/tests/metrics/oracle/libc.json
index beaef667824195860e65dd80e77a5ed91e266313..a6de1ef4b0825780204b04cccd14a34ef61ddacc 100644
--- a/tests/metrics/oracle/libc.json
+++ b/tests/metrics/oracle/libc.json
@@ -114,6 +114,7 @@
{ "setsid": { "calls": 0, "address_taken": false } },
{ "setuid": { "calls": 0, "address_taken": false } },
{ "setvbuf": { "calls": 0, "address_taken": false } },
+ { "sleep": { "calls": 0, "address_taken": false } },
{ "sync": { "calls": 0, "address_taken": false } },
{ "sysconf": { "calls": 0, "address_taken": false } },
{ "tmpfile": { "calls": 0, "address_taken": false } },