diff --git a/share/libc/glob.h b/share/libc/glob.h index 44a09d7cf703ace46ef5d27fe45be33adb4aa7a1..66ec7c4f03fb7307cf93daf39e4543849155be21 100644 --- a/share/libc/glob.h +++ b/share/libc/glob.h @@ -36,7 +36,16 @@ __PUSH_FC_STDLIB #define GLOB_APPEND (1 << 5)/* Append to results of a previous call. */ #define GLOB_NOESCAPE (1 << 6)/* Backslashes don't quote metacharacters. */ #define GLOB_PERIOD (1 << 7)/* Leading `.' can be matched by metachars. */ -#define GLOB_MAGCHAR (1 << 8)/* GNU-specific */ + +// Non-POSIX +#define GLOB_MAGCHAR (1 << 8) +#define GLOB_ALTDIRFUNC (1 << 9) +#define GLOB_BRACE (1 << 10) +#define GLOB_NOMAGIC (1 << 11) +#define GLOB_TILDE (1 << 12) +#define GLOB_ONLYDIR (1 << 13) +#define GLOB_TILDE_CHECK (1 << 14) + #define GLOB_NOSPACE 1 /* Ran out of memory. */ #define GLOB_ABORTED 2 /* Read error. */ diff --git a/share/libc/sys/statvfs.h b/share/libc/sys/statvfs.h index c48d398cf7340eebe2881474ba9b68287b75940b..80c3dcb7f0e5fb85078863fb4850dba72bed40b4 100644 --- a/share/libc/sys/statvfs.h +++ b/share/libc/sys/statvfs.h @@ -46,6 +46,13 @@ struct statvfs { unsigned long f_namemax; // Maximum filename length. }; +enum { + ST_RDONLY = 1, +#define ST_RDONLY ST_RDONLY + ST_NOSUID = 2 +#define ST_NOSUID ST_NOSUID +}; + extern int fstatvfs(int fildes, struct statvfs *buf); extern int statvfs(const char *restrict path, struct statvfs *restrict buf); diff --git a/share/libc/time.h b/share/libc/time.h index ae0a660a0b0c93959f17ec6deb05acdeec3115c3..5b7c0fcfc10e707ab1b7d6feabe81b97daffbab1 100644 --- a/share/libc/time.h +++ b/share/libc/time.h @@ -73,10 +73,28 @@ struct itimerspec { // Note: macros and specifications in this file consider that no // other clocks exist (CLOCK_*_CPUTIME_ID and Linux-specific clocks) -#define CLOCK_REALTIME 666 +#define CLOCK_REALTIME 0 #define CLOCK_MONOTONIC 1 #define TIMER_ABSTIME 1 +// In POSIX, but optional (CPT extension) +#define CLOCK_PROCESS_CPUTIME_ID 2 +#define CLOCK_THREAD_CPUTIME_ID 3 + +// Non-POSIX +#define CLOCK_MONOTONIC_RAW 4 +#define CLOCK_REALTIME_COARSE 5 +#define CLOCK_MONOTONIC_COARSE 6 +#define CLOCK_BOOTTIME 7 +#define CLOCK_REALTIME_ALARM 8 +#define CLOCK_BOOTTIME_ALARM 9 +#define CLOCK_SGI_CYCLE 10 +#define CLOCK_TAI 11 +#define MAX_CLOCKS 16 +#define CLOCKS_MASK (CLOCK_REALTIME | CLOCK_MONOTONIC) +#define CLOCKS_MONO CLOCK_MONOTONIC + + //@ ghost volatile unsigned int __fc_time; /*@ assigns \result \from __fc_time; */ diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_vdso.c b/src/plugins/e-acsl/tests/memory/oracle/gen_vdso.c index 1c80eb77fcbeb081447f7649f409af016e5ed96b..f00ba949c5080c9e564feee61d276feed713016a 100644 --- a/src/plugins/e-acsl/tests/memory/oracle/gen_vdso.c +++ b/src/plugins/e-acsl/tests/memory/oracle/gen_vdso.c @@ -85,7 +85,7 @@ time_t __gen_e_acsl_time(time_t *timer) __gen_e_acsl_assert_data.pred_txt = "\\valid(timer)"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/time.h"; __gen_e_acsl_assert_data.fct = "time"; - __gen_e_acsl_assert_data.line = 102; + __gen_e_acsl_assert_data.line = 120; __gen_e_acsl_assert_data.name = "not_null/valid_timer"; __e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data); __e_acsl_assert_clean(& __gen_e_acsl_assert_data); @@ -102,7 +102,7 @@ time_t __gen_e_acsl_time(time_t *timer) __gen_e_acsl_assert_data_2.pred_txt = "all behaviors complete"; __gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/time.h"; __gen_e_acsl_assert_data_2.fct = "time"; - __gen_e_acsl_assert_data_2.line = 95; + __gen_e_acsl_assert_data_2.line = 113; __e_acsl_assert(__gen_e_acsl_active_bhvrs >= 1, & __gen_e_acsl_assert_data_2); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2); @@ -111,7 +111,7 @@ time_t __gen_e_acsl_time(time_t *timer) __gen_e_acsl_assert_data_3.pred_txt = "all behaviors disjoint"; __gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/time.h"; __gen_e_acsl_assert_data_3.fct = "time"; - __gen_e_acsl_assert_data_3.line = 95; + __gen_e_acsl_assert_data_3.line = 113; __e_acsl_assert(__gen_e_acsl_active_bhvrs <= 1, & __gen_e_acsl_assert_data_3); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3); @@ -140,7 +140,7 @@ time_t __gen_e_acsl_time(time_t *timer) __gen_e_acsl_assert_data_4.pred_txt = "\\initialized(\\old(timer))"; __gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/time.h"; __gen_e_acsl_assert_data_4.fct = "time"; - __gen_e_acsl_assert_data_4.line = 104; + __gen_e_acsl_assert_data_4.line = 122; __gen_e_acsl_assert_data_4.name = "not_null/initialization/timer"; __e_acsl_assert(__gen_e_acsl_initialized,& __gen_e_acsl_assert_data_4); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4); diff --git a/src/plugins/e-acsl/tests/memory/oracle/vdso.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/vdso.res.oracle index 6cabe8f3250166efb72a129dd35a6ec035930847..9c2f89c255754a11262b466c9b9cc683ec979a2d 100644 --- a/src/plugins/e-acsl/tests/memory/oracle/vdso.res.oracle +++ b/src/plugins/e-acsl/tests/memory/oracle/vdso.res.oracle @@ -2,10 +2,10 @@ [e-acsl] Warning: annotating undefined function `time': the generated program may miss memory instrumentation if there are memory-related annotations. -[e-acsl] FRAMAC_SHARE/libc/time.h:95: Warning: +[e-acsl] FRAMAC_SHARE/libc/time.h:113: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/time.h:98: Warning: +[e-acsl] FRAMAC_SHARE/libc/time.h:116: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] translation done in project "e-acsl".