[Libc] update test oracles

src/plugins/variadic/tests/known/oracle/exec.res.oracle

@@ -35,7 +35,6 @@
   sentinel ∈ {0}
   __retres ∈ {0}
 /* Generated by Frama-C */
-#include "sys/time.h"
 #include "unistd.h"
 int main(void)
 {

src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle

@@ -17,7 +17,6 @@
 [eva:final-states] Values at end of function main:
   NON TERMINATING FUNCTION
 /* Generated by Frama-C */
-#include "sys/time.h"
 #include "unistd.h"
 int main(void)
 {

tests/libc/oracle/fc_libc.0.res.oracle

@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] tests/libc/fc_libc.c:149: assertion got status valid.
-[eva] tests/libc/fc_libc.c:150: assertion got status valid.
 [eva] tests/libc/fc_libc.c:151: assertion got status valid.
 [eva] tests/libc/fc_libc.c:152: assertion got status valid.
+[eva] tests/libc/fc_libc.c:153: assertion got status valid.
+[eva] tests/libc/fc_libc.c:154: assertion got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -157,12 +157,12 @@
    wcstombs (0 call); wctomb (0 call); wmemchr (0 call); wmemcmp (0 call);
    wmemmove (0 call); write (0 call); 
   
-  'Extern' global variables (15)
+  'Extern' global variables (17)
   ==============================
    __fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_name;
-   __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; __fc_hostname;
-   __fc_mblen_state; __fc_mbtowc_state; __fc_ttyname; __fc_wctomb_state;
-   optarg; opterr; optopt; tzname
+   __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; __fc_hostname; __fc_locale;
+   __fc_locale_names; __fc_mblen_state; __fc_mbtowc_state; __fc_ttyname;
+   __fc_wctomb_state; optarg; opterr; optopt; tzname
   
   Potential entry points (1)
   ==========================
@@ -172,7 +172,7 @@
   ============== 
   Sloc = 1083
   Decision point = 204
-  Global variables = 66
+  Global variables = 68
   If = 195
   Loop = 43
   Goto = 89
@@ -186,7 +186,6 @@
 #include "__fc_builtin.c"
 #include "__fc_builtin.h"
 #include "__fc_define_fd_set_t.h"
-#include "__fc_define_useconds_t.h"
 #include "__fc_gcc_builtins.h"
 #include "__fc_select.h"
 #include "alloca.h"
@@ -214,6 +213,7 @@
 #include "math.h"
 #include "netdb.c"
 #include "netdb.h"
+#include "netinet/in.h"
 #include "poll.h"
 #include "pthread.h"
 #include "pwd.h"

tests/libc/oracle/fc_libc.3.res.oracle

+[kernel] Parsing tests/libc/fc_libc.c (with preprocessing)
+[kernel] parsing c11_functions.json
+[kernel] parsing glibc_functions.json
+[kernel] parsing posix_identifiers.json
+[kernel] parsing nonstandard_identifiers.json

tests/metrics/oracle/libc.1.res.oracle

@@ -4,31 +4,46 @@
    bar (1 call); f (0 call); foo (1 call); g (address taken) (0 call);
    getopt (1 call); main (0 call); 
   
-  Undefined functions (70)
-  ========================
-   clearerr (0 call); clearerr_unlocked (0 call); fclose (0 call);
-   fdopen (0 call); feof (0 call); feof_unlocked (0 call); ferror (0 call);
-   ferror_unlocked (0 call); fflush (0 call); fgetc (0 call); fgetpos (0 call);
-   fgets (0 call); fileno (0 call); fileno_unlocked (0 call);
-   flockfile (0 call); fopen (0 call); fputc (0 call); fputs (0 call);
+  Undefined functions (120)
+  =========================
+   _exit (0 call); access (0 call); chdir (0 call); chown (0 call);
+   chroot (0 call); clearerr (0 call); clearerr_unlocked (0 call);
+   close (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); fclose (0 call); fdopen (0 call); feof (0 call);
+   feof_unlocked (0 call); ferror (0 call); ferror_unlocked (0 call);
+   fflush (0 call); fgetc (0 call); fgetpos (0 call); fgets (0 call);
+   fileno (0 call); fileno_unlocked (0 call); flockfile (0 call);
+   fopen (0 call); fork (0 call); fputc (0 call); fputs (0 call);
    fread (0 call); freopen (0 call); fseek (0 call); fsetpos (0 call);
    ftell (0 call); ftrylockfile (0 call); funlockfile (0 call);
    fwrite (0 call); getc (0 call); getc_unlocked (0 call); getchar (1 call);
-   getchar_unlocked (0 call); getopt_long (0 call); getopt_long_only (0 call);
-   gets (0 call); isalnum (0 call); isalpha (1 call); isascii (0 call);
+   getchar_unlocked (0 call); getcwd (0 call); getegid (0 call);
+   geteuid (0 call); getgid (0 call); gethostname (0 call);
+   getopt_long (0 call); getopt_long_only (0 call); getpgid (0 call);
+   getpgrp (0 call); getpid (0 call); getppid (0 call); getresgid (0 call);
+   getresuid (0 call); gets (0 call); getsid (0 call); getuid (0 call);
+   isalnum (0 call); isalpha (1 call); isascii (0 call); isatty (0 call);
    isblank (1 call); iscntrl (0 call); isdigit (0 call); isgraph (0 call);
    islower (0 call); isprint (0 call); ispunct (0 call); isspace (0 call);
-   isupper (0 call); isxdigit (0 call); pclose (0 call); perror (0 call);
-   popen (0 call); putc (0 call); putc_unlocked (0 call); putchar (0 call);
-   putchar_unlocked (0 call); puts (0 call); remove (0 call); rename (0 call);
-   rewind (0 call); setbuf (0 call); setvbuf (0 call); tmpfile (0 call);
-   tmpnam (0 call); tolower (0 call); toupper (0 call); ungetc (0 call);
-   vfprintf (0 call); vfscanf (0 call); vprintf (0 call); vscanf (0 call);
-   vsnprintf (0 call); vsprintf (0 call); 
+   isupper (0 call); isxdigit (0 call); lseek (0 call); pathconf (0 call);
+   pclose (0 call); perror (0 call); pipe (0 call); popen (0 call);
+   putc (0 call); putc_unlocked (0 call); putchar (0 call);
+   putchar_unlocked (0 call); puts (0 call); read (0 call); remove (0 call);
+   rename (0 call); rewind (0 call); setbuf (0 call); setegid (0 call);
+   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); 
   
-  'Extern' global variables (7)
-  =============================
-   __fc_errno; __fc_stdin; __fc_stdout; optarg; opterr; optind; optopt
+  'Extern' global variables (10)
+  ==============================
+   Frama_C_entropy_source; __fc_errno; __fc_hostname; __fc_stdin; __fc_stdout;
+   __fc_ttyname; optarg; opterr; optind; optopt
   
   Potential entry points (2)
   ==========================
@@ -38,13 +53,13 @@
   ============== 
   Sloc = 17
   Decision point = 0
-  Global variables = 10
+  Global variables = 15
   If = 0
   Loop = 0
   Goto = 0
   Assignment = 8
   Exit point = 6
-  Function = 76
+  Function = 126
   Function call = 7
   Pointer dereferencing = 1
   Cyclomatic complexity = 6
@@ -72,7 +87,7 @@
   ----------------------------------------------------------------------------
 [metrics] Eva coverage statistics
   =======================
-  Syntactically reachable functions = 7 (out of 76)
+  Syntactically reachable functions = 7 (out of 126)
   Semantically reached functions = 7
   Coverage estimation = 100.0%
 [metrics] References to non-analyzed functions

tests/spec/clash_double_file_bts1598.c

@@ -11,7 +11,7 @@ OPT: @PTEST_FILE@ -cpp-extra-args " -Ishare/libc -nostdinc" -print -then -ocode
 #include "errno.h"
 //#include "fenv.h"
 #include "float.h"
-#include "getopt.h"
+//#include "getopt.h"
 #include "inttypes.h"
 #include "iso646.h"
 #include "limits.h"

tests/spec/oracle/clash_double_file_bts1598.res.oracle

@@ -4,7 +4,6 @@
 #include "assert.h"
 #include "ctype.h"
 #include "errno.h"
-#include "getopt.h"
 #include "inttypes.h"
 #include "locale.h"
 #include "math.h"
@@ -26,7 +25,6 @@
 #include "assert.h"
 #include "ctype.h"
 #include "errno.h"
-#include "getopt.h"
 #include "inttypes.h"
 #include "locale.h"
 #include "math.h"