update test oracles

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

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);
 

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 <- 

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}

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}

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

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 } },