From 616a0c6ad42b2059c7f99e2fc78cd6bb87d6cdbf Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 18 Nov 2020 15:07:56 +0100
Subject: [PATCH] [Libc] remove obsolete attribute __FRAMA_C_MODEL__
Fixes #877.
Nowadays, Metrics has option -metrics-no-libc to exclude definitions from
the Frama-C standard library, which was the purpose of the __FRAMA_C_MODEL__.
Also, several libc variables were lacking the attribute, leading to
inconsistent results.
---
share/libc/__fc_alloc_axiomatic.h | 2 +-
share/libc/__fc_builtin.h | 2 +-
share/libc/alloca.h | 2 +-
share/libc/fenv.c | 4 +--
share/libc/stdlib.c | 2 +-
share/libc/stdlib.h | 8 ++---
share/libc/sys/time.h | 10 +++---
share/libc/time.h | 4 +--
tests/libc/oracle/fc_libc.0.res.oracle | 11 ++++---
tests/libc/oracle/fc_libc.1.res.oracle | 42 +++++++++-----------------
10 files changed, 38 insertions(+), 49 deletions(-)
diff --git a/share/libc/__fc_alloc_axiomatic.h b/share/libc/__fc_alloc_axiomatic.h
index b158a02d239..a5cae2a5c45 100644
--- a/share/libc/__fc_alloc_axiomatic.h
+++ b/share/libc/__fc_alloc_axiomatic.h
@@ -29,7 +29,7 @@ __PUSH_FC_STDLIB
__BEGIN_DECLS
-/*@ ghost extern int __fc_heap_status __attribute__((FRAMA_C_MODEL)); */
+/*@ ghost extern int __fc_heap_status; */
/*@ axiomatic dynamic_allocation {
@ predicate is_allocable{L}(integer n) // Can a block of n bytes be allocated?
diff --git a/share/libc/__fc_builtin.h b/share/libc/__fc_builtin.h
index ba911325872..48babc72906 100644
--- a/share/libc/__fc_builtin.h
+++ b/share/libc/__fc_builtin.h
@@ -28,7 +28,7 @@ __PUSH_FC_STDLIB
__BEGIN_DECLS
-extern volatile int Frama_C_entropy_source __attribute__((unused)) __attribute__((FRAMA_C_MODEL));
+extern volatile int Frama_C_entropy_source __attribute__((unused));
/*@ requires valid_p: \valid(p + (0 .. l-1));
assigns p[0 .. l-1] \from Frama_C_entropy_source;
diff --git a/share/libc/alloca.h b/share/libc/alloca.h
index 7d903f91b47..0745815cd98 100644
--- a/share/libc/alloca.h
+++ b/share/libc/alloca.h
@@ -28,7 +28,7 @@ __PUSH_FC_STDLIB
__BEGIN_DECLS
-/*@ ghost extern int __fc_stack_status __attribute__((FRAMA_C_MODEL)); */
+/*@ ghost extern int __fc_stack_status; */
// Note: alloca is considered to never fail, unlike malloc
// Currently, ACSL does not allow specifying that the memory allocated by
diff --git a/share/libc/fenv.c b/share/libc/fenv.c
index f9c9cff39a5..53644e303f7 100644
--- a/share/libc/fenv.c
+++ b/share/libc/fenv.c
@@ -33,13 +33,13 @@ __PUSH_FC_STDLIB
*/
int fetestexcept( int excepts )
{
- static volatile int __fc_random_fetestexcept __attribute__((FRAMA_C_MODEL)); /* random represent the FPU status word. */
+ static volatile int __fc_random_fetestexcept; /* random represent the FPU status word. */
return (0x00FF & __fc_random_fetestexcept); /* B, C3, TOSP, C2, C1, and C0 don't matter. Mask the selected bits. */
}
-volatile fenv_t __fc_fenv_state __attribute__((FRAMA_C_MODEL));
+volatile fenv_t __fc_fenv_state;
/** Saves the current floating-point environment in the object pointed to by
diff --git a/share/libc/stdlib.c b/share/libc/stdlib.c
index 0bd44d02100..7437c80fd77 100644
--- a/share/libc/stdlib.c
+++ b/share/libc/stdlib.c
@@ -74,7 +74,7 @@ void *calloc(size_t nmemb, size_t size)
return p;
}
-char *__fc_env[ARG_MAX] __attribute__((FRAMA_C_MODEL));
+char *__fc_env[ARG_MAX];
// To provide for some non-determinism, __fc_initenv initializes the
// environment with an arbitrary string
#define __FC_INITENV_LEN 64
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index e5e7a3e33e4..541fc9664bb 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -261,7 +261,7 @@ extern unsigned long long int strtoull(
char ** restrict endptr,
int base);
-//@ ghost extern int __fc_random_counter __attribute__((unused)) __attribute__((FRAMA_C_MODEL));
+//@ ghost extern int __fc_random_counter __attribute__((unused));
const unsigned long __fc_rand_max = __FC_RAND_MAX;
/* ISO C: 7.20.2 */
@@ -284,9 +284,9 @@ extern long int random(void);
extern void srandom(unsigned int seed);
// used to check if some *48() functions have called the seed initializer
-int __fc_random48_init __attribute__((FRAMA_C_MODEL));
+int __fc_random48_init;
-extern unsigned short __fc_random48_counter[3] __attribute__((FRAMA_C_MODEL));
+extern unsigned short __fc_random48_counter[3];
unsigned short *__fc_p_random48_counter = __fc_random48_counter;
/*@
@@ -480,7 +480,7 @@ extern void exit(int status) __attribute__ ((__noreturn__));
*/
extern void _Exit(int status) __attribute__ ((__noreturn__));
-extern char *__fc_env[ARG_MAX] __attribute__((FRAMA_C_MODEL));
+extern char *__fc_env[ARG_MAX];
/*@
requires valid_name: valid_read_string(name);
diff --git a/share/libc/sys/time.h b/share/libc/sys/time.h
index 163aeb422a5..e7f0f0ba66f 100644
--- a/share/libc/sys/time.h
+++ b/share/libc/sys/time.h
@@ -42,8 +42,8 @@ struct timezone {
};
/* Abstract representation of the current time. */
-//@ ghost volatile unsigned int __fc_time __attribute__((FRAMA_C_MODEL));
-//@ ghost extern int __fc_tz __attribute__((FRAMA_C_MODEL));
+//@ ghost volatile unsigned int __fc_time;
+//@ ghost extern int __fc_tz;
/*@
requires valid_path: valid_read_string(path);
@@ -111,9 +111,9 @@ struct itimerval {
};
/* Abstract representation of interval timers. */
-//@ ghost volatile struct itimerval __fc_itimer_real __attribute__((FRAMA_C_MODEL));
-//@ ghost volatile struct itimerval __fc_itimer_virtual __attribute__((FRAMA_C_MODEL));
-//@ ghost volatile struct itimerval __fc_itimer_prof __attribute__((FRAMA_C_MODEL));
+//@ ghost volatile struct itimerval __fc_itimer_real;
+//@ ghost volatile struct itimerval __fc_itimer_virtual;
+//@ ghost volatile struct itimerval __fc_itimer_prof;
// NOTE: for functions setitimer/getitimer, we do not currently model
// the signals generated by the timers when they reach zero.
diff --git a/share/libc/time.h b/share/libc/time.h
index 0083859f5e0..9b11b250358 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -78,7 +78,7 @@ struct itimerspec {
#define CLOCK_MONOTONIC 1
#define TIMER_ABSTIME 1
-//@ ghost volatile unsigned int __fc_time __attribute__((FRAMA_C_MODEL));
+//@ ghost volatile unsigned int __fc_time;
/*@ assigns \result \from __fc_time; */
extern clock_t clock(void);
@@ -206,7 +206,7 @@ extern int clock_gettime(clockid_t clk_id, struct timespec *tp);
@ } // calling thread
*/
-/*@ ghost volatile int __fc_interrupted __attribute__((FRAMA_C_MODEL)); */
+/*@ ghost volatile int __fc_interrupted; */
/*@ // missing: may assign to errno: EINTR, EINVAL, ENOTSUP
// missing: assigns \result, rmtp \from 'clock having id clock_id'
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 42687186222..9cd8d6f3657 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -173,12 +173,13 @@
=======================================
__builtin_abort (1 call);
- 'Extern' global variables (16)
+ 'Extern' global variables (20)
==============================
__fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_name;
- __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; __fc_hostname; __fc_locale;
- __fc_locale_names; __fc_mblen_state; __fc_mbtowc_state; __fc_wctomb_state;
- optarg; opterr; optopt; tzname
+ __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; __fc_heap_status;
+ __fc_hostname; __fc_locale; __fc_locale_names; __fc_mblen_state;
+ __fc_mbtowc_state; __fc_random_counter; __fc_stack_status; __fc_tz;
+ __fc_wctomb_state; optarg; opterr; optopt; tzname
Potential entry points (1)
==========================
@@ -188,7 +189,7 @@
==============
Sloc = 1127
Decision point = 213
- Global variables = 70
+ Global variables = 85
If = 198
Loop = 43
Goto = 97
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 1c7f3e7c948..5bd0c4fc591 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -380,8 +380,7 @@ struct termios {
tcflag_t c_lflag ;
cc_t c_cc[32] ;
};
-int volatile Frama_C_entropy_source __attribute__((__unused__,
- __FRAMA_C_MODEL__));
+int volatile Frama_C_entropy_source __attribute__((__unused__));
void Frama_C_make_unknown(char *p, size_t l);
int Frama_C_nondet(int a, int b);
@@ -1129,8 +1128,7 @@ int feholdexcept(fenv_t *envp);
int fesetenv(fenv_t const *envp);
-static int volatile fetestexcept___fc_random_fetestexcept __attribute__((
- __FRAMA_C_MODEL__));
+static int volatile fetestexcept___fc_random_fetestexcept;
int fetestexcept(int excepts)
{
int __retres;
@@ -1138,7 +1136,7 @@ int fetestexcept(int excepts)
return __retres;
}
-fenv_t volatile __fc_fenv_state __attribute__((__FRAMA_C_MODEL__));
+fenv_t volatile __fc_fenv_state;
int feholdexcept(fenv_t *envp)
{
int __retres;
@@ -1913,7 +1911,7 @@ int glob(char const *pattern, int flags,
void globfree(glob_t *pglob);
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic dynamic_allocation {
@@ -2179,9 +2177,7 @@ extern unsigned long strtoul(char const * __restrict nptr,
extern unsigned long long strtoull(char const * __restrict nptr,
char ** __restrict endptr, int base);
-/*@ ghost
-extern int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-*/
+/*@ ghost extern int __fc_random_counter __attribute__((__unused__)); */
unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ensures result_range: 0 ≤ \result ≤ __fc_rand_max;
@@ -2205,8 +2201,8 @@ extern long random(void);
assigns __fc_random_counter \from seed; */
extern void srandom(unsigned int seed);
-int __fc_random48_init __attribute__((__FRAMA_C_MODEL__));
-unsigned short __fc_random48_counter[3] __attribute__((__FRAMA_C_MODEL__));
+int __fc_random48_init;
+unsigned short __fc_random48_counter[3];
unsigned short *__fc_p_random48_counter = __fc_random48_counter;
/*@ ensures random48_initialized: __fc_random48_init ≡ 1;
assigns __fc_random48_counter[0 .. 2], __fc_random48_init;
@@ -2398,7 +2394,7 @@ extern __attribute__((__noreturn__)) void exit(int status);
assigns \nothing; */
extern __attribute__((__noreturn__)) void _Exit(int status);
-char *__fc_env[4096] __attribute__((__FRAMA_C_MODEL__));
+char *__fc_env[4096];
char *getenv(char const *name);
int putenv(char *string);
@@ -6292,8 +6288,7 @@ char *strsignal(int signum)
return __retres;
}
-/*@ ghost unsigned int volatile __fc_time __attribute__((__FRAMA_C_MODEL__));
- */
+/*@ ghost unsigned int volatile __fc_time; */
/*@ assigns \result;
assigns \result \from __fc_time; */
extern clock_t clock(void);
@@ -6431,8 +6426,7 @@ axiomatic nanosleep_predicates {
}
*/
-/*@ ghost int volatile __fc_interrupted __attribute__((__FRAMA_C_MODEL__));
- */
+/*@ ghost int volatile __fc_interrupted; */
/*@ requires valid_request: \valid_read(rqtp);
requires
initialization: initialized_request:
@@ -6941,7 +6935,7 @@ wchar_t *wcsncat(wchar_t *dest, wchar_t const *src, size_t n)
return dest;
}
-/*@ ghost extern int __fc_stack_status __attribute__((__FRAMA_C_MODEL__)); */
+/*@ ghost extern int __fc_stack_status; */
/*@ ensures allocation: \fresh{Old, Here}(\result,\old(size));
assigns __fc_stack_status, \result;
@@ -7423,7 +7417,7 @@ extern int __va_openat_void(int dirfd, char const *filename, int flags);
extern int __va_openat_mode_t(int dirfd, char const *filename, int flags,
mode_t mode);
-/*@ ghost extern int __fc_tz __attribute__((__FRAMA_C_MODEL__)); */
+/*@ ghost extern int __fc_tz; */
/*@ requires valid_path: valid_read_string(path);
requires
@@ -7507,15 +7501,9 @@ extern int gettimeofday(struct timeval * __restrict tv, void * __restrict tz);
*/
extern int settimeofday(struct timeval const *tv, struct timezone const *tz);
-/*@ ghost
- struct itimerval volatile __fc_itimer_real __attribute__((__FRAMA_C_MODEL__));
- */
-/*@ ghost
- struct itimerval volatile __fc_itimer_virtual __attribute__((__FRAMA_C_MODEL__));
- */
-/*@ ghost
- struct itimerval volatile __fc_itimer_prof __attribute__((__FRAMA_C_MODEL__));
- */
+/*@ ghost struct itimerval volatile __fc_itimer_real; */
+/*@ ghost struct itimerval volatile __fc_itimer_virtual; */
+/*@ ghost struct itimerval volatile __fc_itimer_prof; */
/*@ requires valid_curr_value: \valid(curr_value);
ensures initialization: curr_value: \initialized(\old(curr_value));
assigns \result, *curr_value;
--
GitLab