diff --git a/share/libc/malloc.h b/share/libc/malloc.h index 3508e681088d7156a2c1ef1463ec483a387ca669..89992c10aea72c5a5bdde5caef588caf988166c4 100644 --- a/share/libc/malloc.h +++ b/share/libc/malloc.h @@ -21,4 +21,4 @@ /**************************************************************************/ // This file is not in the C standard; it exists for compatibility purposes -#include <stdlib.h> +#include "stdlib.h" diff --git a/share/libc/memory.h b/share/libc/memory.h index 4c1227c6134fc888153acd73db5fca43ba6b1bdd..767739595b490bb6f0e2ec0afee4168883959f7f 100644 --- a/share/libc/memory.h +++ b/share/libc/memory.h @@ -21,4 +21,4 @@ /**************************************************************************/ // This file is not in the C standard; it exists for compatibility purposes -#include <string.h> +#include "string.h" diff --git a/share/libc/pthread.h b/share/libc/pthread.h index d55ece32dee5c2f5a6c474d7495635726e9a7d5e..ac9f78bc234e099c4e77ec0690697b2173030e18 100644 --- a/share/libc/pthread.h +++ b/share/libc/pthread.h @@ -366,8 +366,8 @@ extern void pthread_testcancel(void); // From POSIX: "Inclusion of the <pthread.h> header shall make symbols defined // in the headers <sched.h> and <time.h> visible." -#include <sched.h> -#include <time.h> +// (sched.h has already been included) +#include "time.h" __POP_FC_STDLIB #endif diff --git a/share/libc/pwd.h b/share/libc/pwd.h index c93e3126becd9bd2cc455f9cd2783fa1d10ef277..7e12b710fbb93488ae04d18036a9c9d5079a586a 100644 --- a/share/libc/pwd.h +++ b/share/libc/pwd.h @@ -25,6 +25,7 @@ #include "features.h" __PUSH_FC_STDLIB +#include "__fc_builtin.h" #include "__fc_define_uid_and_gid.h" #include "__fc_string_axiomatic.h" @@ -45,16 +46,12 @@ struct passwd { extern char __fc_getpwuid_pw_name[64]; extern char __fc_getpwuid_pw_passwd[64]; -extern uid_t __fc_getpwuid_pw_uid; -extern gid_t __fc_getpwuid_pw_gid; extern char __fc_getpwuid_pw_dir[64]; extern char __fc_getpwuid_pw_shell[64]; struct passwd __fc_pwd = {.pw_name = __fc_getpwuid_pw_name, .pw_passwd = __fc_getpwuid_pw_passwd, - .pw_uid = __fc_getpwuid_pw_uid, - .pw_gid = __fc_getpwuid_pw_gid, .pw_dir = __fc_getpwuid_pw_dir, .pw_shell = __fc_getpwuid_pw_shell}; diff --git a/share/libc/semaphore.h b/share/libc/semaphore.h index 264a85bfeda14cc93d550b93bdae55e390fc78b6..765cd52cb54e180d73188d19c4973ee4b3eb615d 100644 --- a/share/libc/semaphore.h +++ b/share/libc/semaphore.h @@ -26,7 +26,7 @@ #define __FC_SEMAPHORE #include "features.h" __PUSH_FC_STDLIB -#include <time.h> +#include "time.h" __BEGIN_DECLS diff --git a/share/libc/time.h b/share/libc/time.h index ffe74960d94212f40e32a517a2904e5ff256bbc4..60e5031571f9ef5e2d527e9b5e8a81907ae66a36 100644 --- a/share/libc/time.h +++ b/share/libc/time.h @@ -31,7 +31,7 @@ __PUSH_FC_STDLIB #include "__fc_string_axiomatic.h" #include "errno.h" - +#include "signal.h" /* * Names of the interval timers, and structure * defining a timer setting: diff --git a/share/libc/unistd.h b/share/libc/unistd.h index 3e790d2126994b6800877bfbed1493e67e19ebae..019c35bdad2fab505c9beb3be0f3c573f28a9e47 100644 --- a/share/libc/unistd.h +++ b/share/libc/unistd.h @@ -36,8 +36,8 @@ __PUSH_FC_STDLIB #include "__fc_define_intptr_t.h" #include "__fc_select.h" -#include <getopt.h> -#include <limits.h> +#include "getopt.h" +#include "limits.h" extern volatile int Frama_C_entropy_source; diff --git a/share/libc/utmpx.h b/share/libc/utmpx.h index cc1c85dc142c5fed93416b518f92ef9fc5e4d068..8e38de8057f31eb2173cd8c56e560dc8a8d0f98e 100644 --- a/share/libc/utmpx.h +++ b/share/libc/utmpx.h @@ -26,7 +26,7 @@ __PUSH_FC_STDLIB #include "__fc_define_pid_t.h" -#include <sys/time.h> +#include "sys/time.h" __BEGIN_DECLS diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle index 6468d9e5be5263ef8d9f565e6a6f053d9d7730bf..d3eac0b8fd4d4f2e18e10087b2a1bc0f9c5d0f3a 100644 --- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle +++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle @@ -155,6 +155,7 @@ /* Generated by Frama-C */ #include "errno.h" #include "inttypes.h" +#include "signal.h" #include "stdarg.h" #include "stddef.h" #include "stdint.h" diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle index 304d4dc1977dc8951401f9d5e953da093460bcea..84ee5740088cec6cd2618b26d7d683bdb34bcea8 100644 --- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle +++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle @@ -54,6 +54,7 @@ __retres ∈ {0} /* Generated by Frama-C */ #include "errno.h" +#include "signal.h" #include "stdarg.h" #include "stdio.h" #include "time.h" diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle index 0f8d049bfce33a5a0d3672e0ca5738d642229c0a..6d0225a773070bb675e09debc3d519189cff1cc1 100644 --- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle +++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle @@ -83,6 +83,7 @@ S___fc_stdout[0..1] ∈ [--..--] /* Generated by Frama-C */ #include "errno.h" +#include "signal.h" #include "stdarg.h" #include "stdio.h" #include "time.h" diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle index eab1d99264c45d6300692246cc0ac9ef6fca48d0..ba81dc3d6039cf8489dcec07f828cb488595f2b3 100644 --- a/tests/libc/oracle/fc_libc.0.res.oracle +++ b/tests/libc/oracle/fc_libc.0.res.oracle @@ -156,12 +156,12 @@ wcstombs (0 call); wctomb (0 call); wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call); write (0 call); - 'Extern' global variables (17) + 'Extern' global variables (15) ============================== - __fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_gid; - __fc_getpwuid_pw_name; __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; - __fc_getpwuid_pw_uid; __fc_hostname; __fc_mblen_state; __fc_mbtowc_state; - __fc_ttyname; __fc_wctomb_state; optarg; opterr; optopt; tzname + __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 Potential entry points (1) ========================== @@ -171,7 +171,7 @@ ============== Sloc = 1083 Decision point = 204 - Global variables = 68 + Global variables = 66 If = 195 Loop = 43 Goto = 89 diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle index a0d63cf77b129c701a89d1e3da29808ad515ff32..c0bb6e199f8b77143bc6427264ab126e5e3480cc 100644 --- a/tests/libc/oracle/fc_libc.1.res.oracle +++ b/tests/libc/oracle/fc_libc.1.res.oracle @@ -7050,10 +7050,6 @@ extern char __fc_getpwuid_pw_name[64]; extern char __fc_getpwuid_pw_passwd[64]; -extern uid_t __fc_getpwuid_pw_uid; - -extern gid_t __fc_getpwuid_pw_gid; - extern char __fc_getpwuid_pw_dir[64]; extern char __fc_getpwuid_pw_shell[64]; @@ -7061,8 +7057,8 @@ extern char __fc_getpwuid_pw_shell[64]; struct passwd __fc_pwd = {.pw_name = __fc_getpwuid_pw_name, .pw_passwd = __fc_getpwuid_pw_passwd, - .pw_uid = __fc_getpwuid_pw_uid, - .pw_gid = __fc_getpwuid_pw_gid, + .pw_uid = 0U, + .pw_gid = 0U, .pw_gecos = (char *)0, .pw_dir = __fc_getpwuid_pw_dir, .pw_shell = __fc_getpwuid_pw_shell};