diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
index 356e1b9e003678bb05b4ca64134d1a8ded65905c..05e710af68b22e3f2a673bbe01c53cc7c0d0107b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
@@ -46,12 +46,10 @@ tests/e-acsl-runtime/bts1324.i:8:[kernel] warning: out of bounds read. assert \v
tests/e-acsl-runtime/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_i_2);
tests/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid.
-tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid, but it is unknown if the behavior is active.
+tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function e_acsl_assert
./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid.
-tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid, but it is unknown if the behavior is active.
+tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
index 02eae28e393acbbf8f70b56510ac6365e843bd2c..a12dca094f901f98e1d3112eba7282032b5d9f71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
@@ -20,11 +20,9 @@
./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid.
-tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid, but it is unknown if the behavior is active.
+tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid.
-tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid, but it is unknown if the behavior is active.
+tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
index cf5503ba38bb81cba818c5aba1d58259e2e2796b..07089a4e225ff07b109bf7af993453ba472cdc0b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
@@ -18,7 +18,8 @@ model __mpz_struct { ℤ n };
*/
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
index cf5503ba38bb81cba818c5aba1d58259e2e2796b..07089a4e225ff07b109bf7af993453ba472cdc0b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
@@ -18,7 +18,8 @@ model __mpz_struct { ℤ n };
*/
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
index c2bf90b4211d7efc16fc3c789de81e2d25ce2ff4..ae5e82f5a21aca8e86287574e3188912b493157e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
@@ -53,19 +53,19 @@ tests/e-acsl-runtime/function_contract.i:30:[value] Function j, behavior b1: pos
tests/e-acsl-runtime/function_contract.i:34:[value] Function j, behavior b2: postcondition got status valid.
tests/e-acsl-runtime/function_contract.i:30:[value] Function __e_acsl_j, behavior b1: postcondition got status valid.
tests/e-acsl-runtime/function_contract.i:34:[value] Function __e_acsl_j, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:40:[value] Function __e_acsl_k, behavior b1: assumption got status invalid; precondition not evaluated.
+tests/e-acsl-runtime/function_contract.i:40:[value] Function __e_acsl_k, behavior b1: assumes got status invalid; precondition not evaluated.
tests/e-acsl-runtime/function_contract.i:44:[value] Function __e_acsl_k, behavior b2: precondition got status valid.
tests/e-acsl-runtime/function_contract.i:45:[value] Function __e_acsl_k, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:40:[value] Function k, behavior b1: assumption got status invalid; precondition not evaluated.
+tests/e-acsl-runtime/function_contract.i:40:[value] Function k, behavior b1: assumes got status invalid; precondition not evaluated.
tests/e-acsl-runtime/function_contract.i:44:[value] Function k, behavior b2: precondition got status valid.
tests/e-acsl-runtime/function_contract.i:45:[value] Function k, behavior b2: precondition got status valid.
tests/e-acsl-runtime/function_contract.i:51:[value] Assertion got status valid.
tests/e-acsl-runtime/function_contract.i:49:[value] Function l: postcondition got status valid.
tests/e-acsl-runtime/function_contract.i:49:[value] Function __e_acsl_l: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:58:[value] Function m, behavior b1: assumes got status invalid; post-condition not evaluated.
+tests/e-acsl-runtime/function_contract.i:58:[value] Function m, behavior b1: assumes got status invalid; postcondition not evaluated.
tests/e-acsl-runtime/function_contract.i:62:[value] Function m, behavior b2: postcondition got status valid.
tests/e-acsl-runtime/function_contract.i:63:[value] Function m, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:58:[value] Function __e_acsl_m, behavior b1: assumes got status invalid; post-condition not evaluated.
+tests/e-acsl-runtime/function_contract.i:58:[value] Function __e_acsl_m, behavior b1: assumes got status invalid; postcondition not evaluated.
tests/e-acsl-runtime/function_contract.i:62:[value] Function __e_acsl_m, behavior b2: postcondition got status valid.
tests/e-acsl-runtime/function_contract.i:63:[value] Function __e_acsl_m, behavior b2: postcondition got status valid.
tests/e-acsl-runtime/function_contract.i:67:[value] Function __e_acsl_n: precondition got status valid.
@@ -73,9 +73,9 @@ tests/e-acsl-runtime/function_contract.i:68:[value] Function __e_acsl_n: precond
tests/e-acsl-runtime/function_contract.i:67:[value] Function n: precondition got status valid.
tests/e-acsl-runtime/function_contract.i:68:[value] Function n: precondition got status valid.
tests/e-acsl-runtime/function_contract.i:71:[value] Function n, behavior b1: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:74:[value] Function n, behavior b2: assumes got status invalid; post-condition not evaluated.
+tests/e-acsl-runtime/function_contract.i:74:[value] Function n, behavior b2: assumes got status invalid; postcondition not evaluated.
tests/e-acsl-runtime/function_contract.i:71:[value] Function __e_acsl_n, behavior b1: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; post-condition not evaluated.
+tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; postcondition not evaluated.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
index 27d1e2cd1b832a3370978df46d3450ba5d2a73ee..5caae7ded192dc0eef4a3444570c0477e23d7d18 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
@@ -37,19 +37,19 @@ tests/e-acsl-runtime/function_contract.i:30:[value] Function j, behavior b1: pos
tests/e-acsl-runtime/function_contract.i:34:[value] Function j, behavior b2: postcondition got status valid.
tests/e-acsl-runtime/function_contract.i:30:[value] Function __e_acsl_j, behavior b1: postcondition got status valid.
tests/e-acsl-runtime/function_contract.i:34:[value] Function __e_acsl_j, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:40:[value] Function __e_acsl_k, behavior b1: assumption got status invalid; precondition not evaluated.
+tests/e-acsl-runtime/function_contract.i:40:[value] Function __e_acsl_k, behavior b1: assumes got status invalid; precondition not evaluated.
tests/e-acsl-runtime/function_contract.i:44:[value] Function __e_acsl_k, behavior b2: precondition got status valid.
tests/e-acsl-runtime/function_contract.i:45:[value] Function __e_acsl_k, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:40:[value] Function k, behavior b1: assumption got status invalid; precondition not evaluated.
+tests/e-acsl-runtime/function_contract.i:40:[value] Function k, behavior b1: assumes got status invalid; precondition not evaluated.
tests/e-acsl-runtime/function_contract.i:44:[value] Function k, behavior b2: precondition got status valid.
tests/e-acsl-runtime/function_contract.i:45:[value] Function k, behavior b2: precondition got status valid.
tests/e-acsl-runtime/function_contract.i:51:[value] Assertion got status valid.
tests/e-acsl-runtime/function_contract.i:49:[value] Function l: postcondition got status valid.
tests/e-acsl-runtime/function_contract.i:49:[value] Function __e_acsl_l: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:58:[value] Function m, behavior b1: assumes got status invalid; post-condition not evaluated.
+tests/e-acsl-runtime/function_contract.i:58:[value] Function m, behavior b1: assumes got status invalid; postcondition not evaluated.
tests/e-acsl-runtime/function_contract.i:62:[value] Function m, behavior b2: postcondition got status valid.
tests/e-acsl-runtime/function_contract.i:63:[value] Function m, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:58:[value] Function __e_acsl_m, behavior b1: assumes got status invalid; post-condition not evaluated.
+tests/e-acsl-runtime/function_contract.i:58:[value] Function __e_acsl_m, behavior b1: assumes got status invalid; postcondition not evaluated.
tests/e-acsl-runtime/function_contract.i:62:[value] Function __e_acsl_m, behavior b2: postcondition got status valid.
tests/e-acsl-runtime/function_contract.i:63:[value] Function __e_acsl_m, behavior b2: postcondition got status valid.
tests/e-acsl-runtime/function_contract.i:67:[value] Function __e_acsl_n: precondition got status valid.
@@ -57,9 +57,9 @@ tests/e-acsl-runtime/function_contract.i:68:[value] Function __e_acsl_n: precond
tests/e-acsl-runtime/function_contract.i:67:[value] Function n: precondition got status valid.
tests/e-acsl-runtime/function_contract.i:68:[value] Function n: precondition got status valid.
tests/e-acsl-runtime/function_contract.i:71:[value] Function n, behavior b1: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:74:[value] Function n, behavior b2: assumes got status invalid; post-condition not evaluated.
+tests/e-acsl-runtime/function_contract.i:74:[value] Function n, behavior b2: assumes got status invalid; postcondition not evaluated.
tests/e-acsl-runtime/function_contract.i:71:[value] Function __e_acsl_n, behavior b1: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; post-condition not evaluated.
+tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; postcondition not evaluated.
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
index 3419cec9d999f99e90fd09ad38501fa7216e9121..f77e981e62c89fbb050bd5a834a00057cb1a389a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
index 3419cec9d999f99e90fd09ad38501fa7216e9121..f77e981e62c89fbb050bd5a834a00057cb1a389a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
index 869706a574cb58a4a60bc05738d3f04c77e54726..354709d844085b4b011580814a3389cfa9d9f619 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
index 4d8aa04446bc469a890909fa26a214cee08991ba..4e8da469bc9ae3ded74d0c3b294a7269bd8a5696 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
@@ -16,6 +16,7 @@ model __mpz_struct { ℤ n };
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -25,6 +26,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -35,14 +37,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
char const *str,
int base);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns *z1;
@@ -50,6 +55,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -59,6 +65,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_neg(__mpz_struct * /*[1]*/ z
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -68,6 +75,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -77,6 +85,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z
extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -86,6 +95,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -95,6 +105,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_r(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns *z1;
@@ -102,6 +113,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_r(__mpz_struct * /*[1]*
*/
extern __attribute__((__FC_BUILTIN__)) int __gmpz_com(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -109,9 +121,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -121,6 +135,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
index c8a0c32d7a99b9f5c6444e8ea6643bf8d13196e3..ea83a5be2ddaa1fd2433b2220fb2b8897a2238a0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int T1[3];
int T2[4];
int main(void)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
index 535eafd21994fbca213192dc3493d2a43d0f69f5..4d7a791597b133ccfcdab54c2548b7d16ece0e64 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
@@ -19,14 +19,17 @@ model __mpz_struct { ℤ n };
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -34,9 +37,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -46,6 +51,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int T1[3];
int T2[4];
int main(void)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
index 912eb9aa39532d21c3dc28b255f6d4be489e8ae0..d6839c71defb15c7649332785f29efd760667c1a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -31,14 +33,19 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int A = 0;
/*@ ensures \at(A,Post) ≡ 3; */
void f(void)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
index c2fbb79c193f808a0256075be56b7871deff5500..b6bb896a6a6b9bce8ce5adaf66892c7cdb618b2a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
@@ -16,6 +16,7 @@ model __mpz_struct { ℤ n };
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
/*@ requires \valid(z_orig);
requires ¬\initialized(z);
ensures \valid(\old(z));
@@ -25,6 +26,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set(__mpz_struct * /*[1]*/ z,
__mpz_struct const * /*[1]*/ z_orig);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -34,14 +36,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set(__mpz_struct * /*[1
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -51,6 +56,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -58,9 +64,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -72,14 +80,19 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int A = 0;
/*@ ensures \at(A,Post) ≡ 3; */
void f(void)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
index c195c5636b917ad73cb65f5295e6303f4a0316c4..033e30432aa81b884e398d26c3ded3d9dd0da0ba 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
@@ -33,9 +33,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = 32767UL;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -47,13 +49,17 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -61,7 +67,9 @@ extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
void read_sensor_4(unsigned int *m)
{
__store_block((void *)(& m),4U);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
index c195c5636b917ad73cb65f5295e6303f4a0316c4..033e30432aa81b884e398d26c3ded3d9dd0da0ba 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
@@ -33,9 +33,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = 32767UL;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -47,13 +49,17 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -61,7 +67,9 @@ extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
void read_sensor_4(unsigned int *m)
{
__store_block((void *)(& m),4U);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
index ccbc3504f989e4316d20342806b2e7610d63b824..474010e2dbecbb2b1c58ac0f5b45a0e873710d48 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -31,18 +33,24 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -50,7 +58,9 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ requires \valid(Mtmax_in);
requires \valid(Mwmax);
requires \valid(Mtmax_out);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
index 2f18d29e1b085670c06fb1a0a2eb38f0858b7bbc..00d72cb19c78ce71566ae42684ad9fcf0907343d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
@@ -16,6 +16,7 @@ model __mpz_struct { ℤ n };
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
/*@ requires \valid(z_orig);
requires ¬\initialized(z);
ensures \valid(\old(z));
@@ -25,6 +26,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set(__mpz_struct * /*[1]*/ z,
__mpz_struct const * /*[1]*/ z_orig);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -34,14 +36,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set(__mpz_struct * /*[1
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -51,9 +56,11 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -61,9 +68,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -75,18 +84,24 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -94,7 +109,9 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ requires \valid(Mtmax_in);
requires \valid(Mwmax);
requires \valid(Mtmax_out);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
index 84964e3b1dac1aab7fce4917c92ee8a09138f177..c360340c3e76d9a64396a6e2c591b029d0084a35 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -31,17 +33,23 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ behavior yes:
assumes ∀ long long i; 0 < i ∧ i < n ⇒ *(t+(i-1)) ≤ *(t+i);
ensures \result ≡ 1;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
index faafce0209931b1114e02266cb4989902a0b54d3..ab5b60c5a13910959d3b905c9fdca169cdf637c9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
@@ -16,6 +16,7 @@ model __mpz_struct { ℤ n };
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -25,6 +26,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(z_orig);
requires \valid(z);
assigns *z;
@@ -32,14 +34,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z,
__mpz_struct const * /*[1]*/ z_orig);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -49,6 +54,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -58,9 +64,11 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -68,9 +76,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -82,14 +92,19 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ behavior yes:
assumes ∀ ℤ i; 0 < i ∧ i < n ⇒ *(t+(i-1)) ≤ *(t+i);
ensures \result ≡ 1;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
index 59f30e2364764e4f4e9e6bdd0b281cd9eb2916f8..0637bc24f3be694fc551e06bf7e87034a4fdd1d7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
@@ -18,9 +18,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -32,16 +34,21 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -49,7 +56,9 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ ensures
*\old(AverageAccel) ≡
(((((*\old(Accel))[4]+(*\old(Accel))[3])+(*\old(Accel))[2])+(*\old(
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
index 2d4c79e971e5f9e70b186f3b024ee3f1a898cd23..553e4e9377f9d094a9f36d2bd0efa9901949cf82 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
@@ -17,6 +17,7 @@ model __mpz_struct { ℤ n };
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -26,14 +27,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -43,6 +47,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -52,6 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -59,9 +65,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -73,14 +81,19 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ ensures
*\old(AverageAccel) ≡
(((((*\old(Accel))[4]+(*\old(Accel))[3])+(*\old(Accel))[2])+(*\old(
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
index 53fe1bcbb7c162f4a280a02c11b9ce17eed2dcd6..f2405856e3dfc7fd86ec129a949771a80cb85951 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
index 2623e610bea0b97aa0886219d682fc569e60b784..9789dd1062e26e2813185080db78b55d006cad00 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
@@ -19,6 +19,7 @@ model __mpz_struct { ℤ n };
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__mpz_struct * /*[1]*/ z,
unsigned long n);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -28,6 +29,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__mpz_struct * /
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -38,17 +40,21 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
char const *str,
int base);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -56,9 +62,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -68,6 +76,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index 47664515b3be2e83c535d05dbfb91a441dae193c..e598f52f01a700cdd31aae0d2428f932f9474fff 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -31,11 +33,15 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
char *__e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
index 402166c9f4d4e46f19b1a99055dcc029f947558b..2648ddb539f621eac6de5aa3069c181149f2ca44 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
@@ -16,6 +16,7 @@ model __mpz_struct { ℤ n };
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -25,14 +26,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns *z1;
@@ -40,6 +44,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -47,9 +52,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -61,11 +68,15 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
char *__e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
index c71e41179b703354074b7493ce04944d77df846d..d6996ee4c2ec7c9d3b8b9f785fd836490b06f0f2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
index c71e41179b703354074b7493ce04944d77df846d..d6996ee4c2ec7c9d3b8b9f785fd836490b06f0f2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
index 386b4ecdc92e330bab22f0e4f26bd304aaa64778..30c66f8e764822274d7f190dc8bc0ea146718632 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int X = 0;
int Y = 2;
/*@ ensures X ≡ 1; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
index 95b3bd20df04a0c6ad60e1d5c02fcfc1ed2af57b..8c009cab9234ffc8260dfdda835a2f0cf76a9d7e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
@@ -16,6 +16,7 @@ model __mpz_struct { ℤ n };
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -25,14 +26,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -42,6 +46,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -49,9 +54,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -61,6 +68,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int X = 0;
int Y = 2;
/*@ ensures X ≡ 1; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
index 7882e5e214f12e66b749bb530518cd24c543dc81..51a972afb0477d74e37158a45cde97712d629489 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -31,18 +33,24 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -50,7 +58,9 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int G = 0;
int *P;
void e_acsl_global_init(void)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
index d26fb81c2dce8dbf6e00458889e5c14079d6a622..2743755c7f57c185469caf579c2624940467d71c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
@@ -19,14 +19,17 @@ model __mpz_struct { ℤ n };
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -34,9 +37,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -48,19 +53,26 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int G = 0;
int *P;
void e_acsl_global_init(void)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index f50c65f0a47a9df1131fb33038882d80196fd29a..4e352564c0861f136e32d1b6a19cc452eba88040 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -20,14 +20,17 @@ model __mpz_struct { ℤ n };
extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
char const *str,
int base);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -35,9 +38,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -47,6 +52,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
index 7d51514e4fd068d27e636a82d266bccb230a30ba..5f455554036617a025a911561ee1d0f4cbc08e95 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
@@ -19,6 +19,7 @@ model __mpz_struct { ℤ n };
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -29,14 +30,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
char const *str,
int base);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -44,9 +48,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -56,6 +62,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
index 7f9b3c10346a3c885814c772b626eb6082c83999..c0c4ec8cf552f125b6b9d1783e96cce283c74748 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
index d6ba8d34e02d5e8517bd1858998c246de9a39d2e..6d2d9f6d4380c833350f549d8d1f45f85dea42e4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
@@ -19,14 +19,17 @@ model __mpz_struct { ℤ n };
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -34,9 +37,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -46,6 +51,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
index 163d38337dd2e7b8088654d4ed4b339d97328f7d..956b02167dc1e80199b7457f25542d63e76a69a4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int X = 0;
/*@ ensures X ≡ 3; */
int __e_acsl_main(void)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
index 01f6e6522e339aebad5eec84c82baca82057628e..6ac94984fe3731fe100e0d11f01cf38a82a4ddb1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
@@ -19,14 +19,17 @@ model __mpz_struct { ℤ n };
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -34,9 +37,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -46,6 +51,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int X = 0;
/*@ ensures X ≡ 3; */
int __e_acsl_main(void)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
index e9d19cc47acf78fb9eef855ed80ff2fabecb3cd1..b617aa2c1b9de6a33ce350dabe57de600699eac7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
index 03122c968ffd7985d714c36c47509b767b883dff..cb7b01a0b37d9ac50b696173552944c0b5b36e97 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
@@ -16,6 +16,7 @@ model __mpz_struct { ℤ n };
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
/*@ requires \valid(z_orig);
requires ¬\initialized(z);
ensures \valid(\old(z));
@@ -25,6 +26,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set(__mpz_struct * /*[1]*/ z,
__mpz_struct const * /*[1]*/ z_orig);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -34,14 +36,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set(__mpz_struct * /*[1
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -51,6 +56,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -58,9 +64,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -70,6 +78,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index 40b0eb6b5bdf3cea81bd341db046af6659ec1d03..3b172105afaf1a3c63852f029f7731ac73b94f56 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int A[10];
/*@ requires ∀ int i; 0 ≤ i ∧ i < 9 ⇒ A[i] ≤ A[i+1];
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
index ba0de88b05d3156a557053828b4c35610a5f675c..a8da4e4ab162fe0c24f51b0e6902beb346b20019 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
@@ -16,6 +16,7 @@ model __mpz_struct { ℤ n };
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -25,6 +26,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(z_orig);
requires \valid(z);
assigns *z;
@@ -32,14 +34,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z,
__mpz_struct const * /*[1]*/ z_orig);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -49,9 +54,11 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -59,9 +66,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -71,6 +80,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int A[10];
/*@ requires ∀ ℤ i; 0 ≤ i ∧ i < 9 ⇒ A[i] ≤ A[i+1];
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
index c6ffe53da7b45f11bb02f906269911883b5eae64..ac92a79d108761b0238e42155e5eb1920a2f53b4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -31,17 +33,23 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -49,8 +57,11 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void);
+
char *T;
int G = 0;
void f(void)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
index af71abc591ed79c05f2489de6cc1986b70def8b8..dfc271b37df749d6e500265831d7f92d3fb54564 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
@@ -19,14 +19,17 @@ model __mpz_struct { ℤ n };
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -34,9 +37,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -48,17 +53,23 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -66,8 +77,11 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void);
+
char *T;
int G = 0;
void f(void)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
index 6ea6f2c3e76cb351422d0c8620471a9cd9c9cc8d..19399dd23687ceb2f6aaa7ab3ddb82cd5ab09745 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
@@ -21,9 +21,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -54,15 +56,20 @@ axiomatic
disjoint behaviors no_allocation, allocation;
*/
extern void *__malloc(size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -70,7 +77,9 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
assigns \result \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
index 6ea6f2c3e76cb351422d0c8620471a9cd9c9cc8d..19399dd23687ceb2f6aaa7ab3ddb82cd5ab09745 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
@@ -21,9 +21,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -54,15 +56,20 @@ axiomatic
disjoint behaviors no_allocation, allocation;
*/
extern void *__malloc(size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -70,7 +77,9 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
assigns \result \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
index 9d01bce35551a9648f24102a19775f3c2ff74623..e1f210fb1d7cde6e34f7f832936ce4141a8e4b59 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
index 1f47a37838364e310502e8301eca16c4fc9a7a16..7d1e802ed8a47df397f41dfd242eaf4e39c157a6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
@@ -19,14 +19,17 @@ model __mpz_struct { ℤ n };
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -34,9 +37,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -46,6 +51,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
index 0239ed1cfc65d6b32799d6d1e5a23b4f721390a3..f2aaff41fee38fcdec516db18e701cefd4000eb8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
index fc3838a11abf7609f6f8b96cfe71a787f1cb2d67..f343f34ce46ad620d22a7422eaa9fa626967d978 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
@@ -19,14 +19,17 @@ model __mpz_struct { ℤ n };
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -34,9 +37,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -46,6 +51,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
index da0414fba83f9906026f8aa740d652e5b78faa94..29f71ca94d3e9086f6be303753154edb5473704a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
index da0414fba83f9906026f8aa740d652e5b78faa94..29f71ca94d3e9086f6be303753154edb5473704a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
index b9c3cfc9201cf874273b58dcb0e50b0975051969..565dd233d56c4dc8362df2a9c274356cf3913dbd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
@@ -21,9 +21,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -33,6 +35,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
index bbcb40e25de6d6cca29264a317be80ff0a123b8f..a8c93928c0c14cfec543621baa7baa8d4b048622 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
@@ -23,14 +23,17 @@ model __mpz_struct { ℤ n };
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -38,9 +41,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -50,6 +55,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
index f0ec27407eb913353da2d910be3184f0f9dae2cd..9f9939284d91cfa8d8b70a7c8aee48ffffd406e9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -31,16 +33,21 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -48,7 +55,9 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
index 1e2faaa4e14e844be04a907d594a49456ef715f3..18c0a64a48fd2e68ed08582d9bd5c24dc2ffc84d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
@@ -16,6 +16,7 @@ model __mpz_struct { ℤ n };
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -25,14 +26,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -42,6 +46,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -51,6 +56,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -60,6 +66,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z
extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -69,9 +76,11 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -79,9 +88,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -93,14 +104,19 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
index 27fe27f3603e2196f4d3b4dbb03a38f6fcba0da3..a5a2c2bc22230d00fe87083f6ffa24db5212da80 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
index b317408e77f0206d0c7e22ed89dd63fc365a5438..bdc81e868064531d6c8da54a5461526386939d88 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
@@ -16,6 +16,7 @@ model __mpz_struct { ℤ n };
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -25,6 +26,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(z_orig);
requires \valid(z);
assigns *z;
@@ -32,14 +34,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z,
__mpz_struct const * /*[1]*/ z_orig);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -49,6 +54,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -58,6 +64,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -67,6 +74,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -76,6 +84,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_r(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -83,9 +92,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -95,6 +106,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
index 73cd010813f3d46a6a6a4eaa9e643d6efe351f33..23f4bab94895f02083ed213395e36d55ee1ccdf8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ ensures \result ≡ (int)(\old(x)-\old(x)); */
int f(int x)
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
index 6fc5b2411d8813a0b3b3536e45310cc43248ec42..1e288c0cb0d388927811a451895da9e06e111566 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
@@ -16,6 +16,7 @@ model __mpz_struct { ℤ n };
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -25,14 +26,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -42,9 +46,11 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires \valid(z);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -52,9 +58,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -64,6 +72,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ ensures \result ≡ (int)(\old(x)-\old(x)); */
int f(int x)
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
index 8a5cc2a0f042370c66703beeb7a95fca29e8aa04..987df2b5f03e23ec9df268995eed0e45e6b3f84a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
index 73d28f2f0286ae4ccd57afde6ffd66ff409de594..61216f0bf80278f24043bf42e8073e971f9b316e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
@@ -19,14 +19,17 @@ model __mpz_struct { ℤ n };
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -34,9 +37,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -46,6 +51,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
index c6af4924e53dd8745c434a2027c649d7b8d6003e..d63b597478849dc651bb42e825369000383f46a7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
index d08b0f1cca75a0eb9dcaee7c37640d11feabadde..37c7e7d978f3595b18737da7e10c5b6563cba4f7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
@@ -16,6 +16,7 @@ model __mpz_struct { ℤ n };
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -25,14 +26,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
@@ -42,6 +46,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -49,9 +54,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -61,6 +68,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
index ffbb60ab8238ab5988702d54e58196324654f71b..735d02a898ba12a416e77be9a8b1d4ea3d880dc6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
index ffbb60ab8238ab5988702d54e58196324654f71b..735d02a898ba12a416e77be9a8b1d4ea3d880dc6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -29,6 +31,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
index 2a37474874878566a9b84ec8daa0fb4826faaab9..5efe3e177ea228fc45d74b6010ed0fe1ddb6fbe1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
@@ -18,9 +18,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -30,6 +32,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
index 0527071d17717cc0f6d967a56f9cd18aa7d5cce7..54164f9997e3a1192615c46b6022aa5d87524c21 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
@@ -20,6 +20,7 @@ model __mpz_struct { ℤ n };
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__mpz_struct * /*[1]*/ z,
unsigned long n);
+
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
ensures \initialized(\old(z));
@@ -29,14 +30,17 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__mpz_struct * /
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -44,9 +48,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -56,6 +62,7 @@ axiomatic
}
*/
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index 285620ffdcffa1838616c8899d92ff1472225ecb..7793aa448566aac91b8e5d634d3c547b1cfe4d1d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -50,6 +52,7 @@ axiomatic
disjoint behaviors no_allocation, allocation;
*/
extern void *__malloc(size_t size);
+
/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
frees p;
@@ -70,15 +73,20 @@ extern void *__malloc(size_t size);
disjoint behaviors no_deallocation, deallocation;
*/
extern void __free(void *p);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -86,7 +94,9 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
assigns \result \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index 285620ffdcffa1838616c8899d92ff1472225ecb..7793aa448566aac91b8e5d634d3c547b1cfe4d1d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -50,6 +52,7 @@ axiomatic
disjoint behaviors no_allocation, allocation;
*/
extern void *__malloc(size_t size);
+
/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
frees p;
@@ -70,15 +73,20 @@ extern void *__malloc(size_t size);
disjoint behaviors no_deallocation, deallocation;
*/
extern void __free(void *p);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -86,7 +94,9 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
assigns \result \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
index 9ec932779c327bf2f1a59fb471fdb210ce7a43f8..9454eb28482fec302eea039b366b81efe809ad55 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
@@ -17,9 +17,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -50,6 +52,7 @@ axiomatic
disjoint behaviors no_allocation, allocation;
*/
extern void *__malloc(size_t size);
+
/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
frees p;
@@ -70,21 +73,28 @@ extern void *__malloc(size_t size);
disjoint behaviors no_deallocation, deallocation;
*/
extern void __free(void *p);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -92,7 +102,9 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
assigns \result \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
index 2cc0a9b8f82bf2944c7e7649f0eda258c44f705e..24b12b697e6aea926af6258ca918ed9ddf7469e8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
@@ -19,14 +19,17 @@ model __mpz_struct { ℤ n };
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
+
/*@ requires \valid(x);
assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
+
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -34,9 +37,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -67,6 +72,7 @@ axiomatic
disjoint behaviors no_allocation, allocation;
*/
extern void *__malloc(size_t size);
+
/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
frees p;
@@ -87,18 +93,24 @@ extern void *__malloc(size_t size);
disjoint behaviors no_deallocation, deallocation;
*/
extern void __free(void *p);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -106,7 +118,9 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
assigns \result \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index 595386a80d46f8057cc79e0490ebf8e9a558547b..43b4af65eba4f220671e04089423342f6a0349b0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -21,9 +21,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -35,12 +37,16 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -48,7 +54,9 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ behavior B1:
assumes l ≡ \null;
ensures \result ≡ \old(l);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
index 595386a80d46f8057cc79e0490ebf8e9a558547b..43b4af65eba4f220671e04089423342f6a0349b0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
@@ -21,9 +21,11 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *fct,
char *pred_txt,
int line);
+
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
+
/*@
axiomatic
dynamic_allocation {
@@ -35,12 +37,16 @@ axiomatic
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
@@ -48,7 +54,9 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
+
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
/*@ behavior B1:
assumes l ≡ \null;
ensures \result ≡ \old(l);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index 6b7fdc015875702a687cb1a5d4f19d0bdc01b88a..f4d24b8628a23dc409a64af7eeae3a5e96035b55 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -52,14 +52,10 @@ tests/e-acsl-runtime/linear_search.i:9:[value] Function search: precondition got
tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown, but it is unknown if the behavior is active.
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown, but it is unknown if the behavior is active.
-tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown, but it is unknown if the behavior is active.
-tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown, but it is unknown if the behavior is active.
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown.
[value] using specification for function __clean
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
index ed2ff3fe789c7bf771613960f80dc4b0d916ddc2..45ca0cc193e00528b0911d67936b49a2a39939b1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
@@ -24,14 +24,10 @@ tests/e-acsl-runtime/linear_search.i:9:[value] Function search: precondition got
tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown, but it is unknown if the behavior is active.
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown, but it is unknown if the behavior is active.
-tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown, but it is unknown if the behavior is active.
-tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown.
-tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown, but it is unknown if the behavior is active.
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown.
[value] using specification for function __clean
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
index f035ea15556fad1c11375d7c484305072707ab9f..f4236bc6ffd9193aba974d92d101d2939ac8cd20 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
@@ -21,10 +21,8 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown, but it is unknown if the behavior is active.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid, but it is unknown if the behavior is active.
+FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
[value] using specification for function __initialized
./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
index f035ea15556fad1c11375d7c484305072707ab9f..f4236bc6ffd9193aba974d92d101d2939ac8cd20 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
@@ -21,10 +21,8 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown, but it is unknown if the behavior is active.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid, but it is unknown if the behavior is active.
+FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
[value] using specification for function __initialized
./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index c45c5580d5bf4c5c2e0591cbe4aa8168fae16235..3a6f3fa7484c1a80f0ce02fe1e74d099c8c9fcf3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -39,10 +39,8 @@ tests/e-acsl-runtime/valid.c:27:[value] Non-termination in evaluation of functio
[value] using specification for function e_acsl_assert
./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown, but it is unknown if the behavior is active.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid, but it is unknown if the behavior is active.
+FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/valid.c:29:[value] Assertion got status valid.
./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
tests/e-acsl-runtime/valid.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index c45c5580d5bf4c5c2e0591cbe4aa8168fae16235..3a6f3fa7484c1a80f0ce02fe1e74d099c8c9fcf3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -39,10 +39,8 @@ tests/e-acsl-runtime/valid.c:27:[value] Non-termination in evaluation of functio
[value] using specification for function e_acsl_assert
./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown, but it is unknown if the behavior is active.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid, but it is unknown if the behavior is active.
+FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/valid.c:29:[value] Assertion got status valid.
./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
tests/e-acsl-runtime/valid.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index fab441dda3c325d787ad60179553c46725cd1ae5..aba852f6b7637d1a78b0b077cd303ca40e32496f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
@@ -37,10 +37,8 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Non-termination in evaluation of f
[value] using specification for function e_acsl_assert
./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown, but it is unknown if the behavior is active.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid, but it is unknown if the behavior is active.
+FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index 7df790d6b2d4350bcc1a3051603ae20033a5c11b..9c843d1b34f6ae34edbb7f549cee2a8d571816c6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
@@ -37,10 +37,8 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Non-termination in evaluation of f
[value] using specification for function e_acsl_assert
./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown, but it is unknown if the behavior is active.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid.
-FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid, but it is unknown if the behavior is active.
+FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
./share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
index 8c7141f72d68f6ecf372679170669c268a99a517..32a3ed46515ca89de988735716222a12a21d90cd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
@@ -23,13 +23,11 @@ tests/e-acsl-runtime/valid_in_contract.c:21:[value] Non-termination in evaluatio
(void *)l->next
[value] using specification for function __delete_block
tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid, but it is unknown if the behavior is active.
+tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function e_acsl_assert
./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function __e_acsl_f, behavior B1: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid, but it is unknown if the behavior is active.
+tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
index 8c7141f72d68f6ecf372679170669c268a99a517..32a3ed46515ca89de988735716222a12a21d90cd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
@@ -23,13 +23,11 @@ tests/e-acsl-runtime/valid_in_contract.c:21:[value] Non-termination in evaluatio
(void *)l->next
[value] using specification for function __delete_block
tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid, but it is unknown if the behavior is active.
+tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function e_acsl_assert
./share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function __e_acsl_f, behavior B1: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid, but it is unknown if the behavior is active.
+tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __clean
[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
[value] done for function main