From 675f630ffb14034b71ab8b821407d7859d8b29f5 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 1 Feb 2013 15:11:46 +0000
Subject: [PATCH] [E-ACSL] update oracles according to kernel's and Value's
changes
---
.../oracle/bts1324.1.res.oracle | 6 ++----
.../e-acsl-runtime/oracle/bts1324.res.oracle | 6 ++----
.../e-acsl-runtime/oracle/empty.1.res.oracle | 3 ++-
.../e-acsl-runtime/oracle/empty.res.oracle | 3 ++-
.../oracle/function_contract.1.res.oracle | 12 ++++++------
.../oracle/function_contract.res.oracle | 12 ++++++------
.../tests/e-acsl-runtime/oracle/gen_addrOf.c | 5 ++++-
.../tests/e-acsl-runtime/oracle/gen_addrOf2.c | 5 ++++-
.../tests/e-acsl-runtime/oracle/gen_arith.c | 5 ++++-
.../tests/e-acsl-runtime/oracle/gen_arith2.c | 17 ++++++++++++++++-
.../tests/e-acsl-runtime/oracle/gen_array.c | 5 ++++-
.../tests/e-acsl-runtime/oracle/gen_array2.c | 8 +++++++-
.../tests/e-acsl-runtime/oracle/gen_at.c | 9 ++++++++-
.../tests/e-acsl-runtime/oracle/gen_at2.c | 15 ++++++++++++++-
.../tests/e-acsl-runtime/oracle/gen_bts1304.c | 10 +++++++++-
.../e-acsl-runtime/oracle/gen_bts13042.c | 10 +++++++++-
.../tests/e-acsl-runtime/oracle/gen_bts1307.c | 12 +++++++++++-
.../e-acsl-runtime/oracle/gen_bts13072.c | 19 ++++++++++++++++++-
.../tests/e-acsl-runtime/oracle/gen_bts1324.c | 10 +++++++++-
.../e-acsl-runtime/oracle/gen_bts13242.c | 17 ++++++++++++++++-
.../tests/e-acsl-runtime/oracle/gen_bts1326.c | 11 ++++++++++-
.../e-acsl-runtime/oracle/gen_bts13262.c | 15 ++++++++++++++-
.../tests/e-acsl-runtime/oracle/gen_cast.c | 5 ++++-
.../tests/e-acsl-runtime/oracle/gen_cast2.c | 11 ++++++++++-
.../e-acsl-runtime/oracle/gen_comparison.c | 8 +++++++-
.../e-acsl-runtime/oracle/gen_comparison2.c | 13 ++++++++++++-
.../tests/e-acsl-runtime/oracle/gen_false.c | 5 ++++-
.../tests/e-acsl-runtime/oracle/gen_false2.c | 5 ++++-
.../oracle/gen_function_contract.c | 5 ++++-
.../oracle/gen_function_contract2.c | 10 +++++++++-
.../tests/e-acsl-runtime/oracle/gen_ghost.c | 12 +++++++++++-
.../tests/e-acsl-runtime/oracle/gen_ghost2.c | 14 +++++++++++++-
.../oracle/gen_integer_constant.c | 8 +++++++-
.../oracle/gen_integer_constant2.c | 9 ++++++++-
.../e-acsl-runtime/oracle/gen_invariant.c | 5 ++++-
.../e-acsl-runtime/oracle/gen_invariant2.c | 8 +++++++-
.../e-acsl-runtime/oracle/gen_labeled_stmt.c | 5 ++++-
.../e-acsl-runtime/oracle/gen_labeled_stmt2.c | 8 +++++++-
.../tests/e-acsl-runtime/oracle/gen_lazy.c | 5 ++++-
.../tests/e-acsl-runtime/oracle/gen_lazy2.c | 11 ++++++++++-
.../e-acsl-runtime/oracle/gen_linear_search.c | 5 ++++-
.../oracle/gen_linear_search2.c | 12 +++++++++++-
.../oracle/gen_literal_string.c | 13 ++++++++++++-
.../oracle/gen_literal_string2.c | 16 +++++++++++++++-
.../e-acsl-runtime/oracle/gen_localvar.c | 11 ++++++++++-
.../e-acsl-runtime/oracle/gen_localvar2.c | 11 ++++++++++-
.../oracle/gen_nested_code_annot.c | 5 ++++-
.../oracle/gen_nested_code_annot2.c | 8 +++++++-
.../tests/e-acsl-runtime/oracle/gen_not.c | 5 ++++-
.../tests/e-acsl-runtime/oracle/gen_not2.c | 8 +++++++-
.../tests/e-acsl-runtime/oracle/gen_null.c | 5 ++++-
.../tests/e-acsl-runtime/oracle/gen_null2.c | 5 ++++-
.../oracle/gen_other_constants.c | 5 ++++-
.../oracle/gen_other_constants2.c | 8 +++++++-
.../tests/e-acsl-runtime/oracle/gen_ptr.c | 11 ++++++++++-
.../tests/e-acsl-runtime/oracle/gen_ptr2.c | 18 +++++++++++++++++-
.../tests/e-acsl-runtime/oracle/gen_quantif.c | 5 ++++-
.../e-acsl-runtime/oracle/gen_quantif2.c | 14 +++++++++++++-
.../tests/e-acsl-runtime/oracle/gen_result.c | 5 ++++-
.../tests/e-acsl-runtime/oracle/gen_result2.c | 11 ++++++++++-
.../tests/e-acsl-runtime/oracle/gen_sizeof.c | 5 ++++-
.../tests/e-acsl-runtime/oracle/gen_sizeof2.c | 8 +++++++-
.../e-acsl-runtime/oracle/gen_stmt_contract.c | 5 ++++-
.../oracle/gen_stmt_contract2.c | 10 +++++++++-
.../tests/e-acsl-runtime/oracle/gen_true.c | 5 ++++-
.../tests/e-acsl-runtime/oracle/gen_true2.c | 5 ++++-
.../tests/e-acsl-runtime/oracle/gen_typedef.c | 5 ++++-
.../e-acsl-runtime/oracle/gen_typedef2.c | 9 ++++++++-
.../tests/e-acsl-runtime/oracle/gen_valid.c | 12 +++++++++++-
.../tests/e-acsl-runtime/oracle/gen_valid2.c | 12 +++++++++++-
.../e-acsl-runtime/oracle/gen_valid_alias.c | 14 +++++++++++++-
.../e-acsl-runtime/oracle/gen_valid_alias2.c | 16 +++++++++++++++-
.../oracle/gen_valid_in_contract.c | 10 +++++++++-
.../oracle/gen_valid_in_contract2.c | 10 +++++++++-
.../oracle/linear_search.1.res.oracle | 12 ++++--------
.../oracle/linear_search.res.oracle | 12 ++++--------
.../oracle/localvar.1.res.oracle | 6 ++----
.../e-acsl-runtime/oracle/localvar.res.oracle | 6 ++----
.../e-acsl-runtime/oracle/valid.1.res.oracle | 6 ++----
.../e-acsl-runtime/oracle/valid.res.oracle | 6 ++----
.../oracle/valid_alias.1.res.oracle | 6 ++----
.../oracle/valid_alias.res.oracle | 6 ++----
.../oracle/valid_in_contract.1.res.oracle | 6 ++----
.../oracle/valid_in_contract.res.oracle | 6 ++----
84 files changed, 603 insertions(+), 138 deletions(-)
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 356e1b9e003..05e710af68b 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 02eae28e393..a12dca094f9 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 cf5503ba38b..07089a4e225 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 cf5503ba38b..07089a4e225 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 c2bf90b4211..ae5e82f5a21 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 27d1e2cd1b8..5caae7ded19 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 3419cec9d99..f77e981e62c 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 3419cec9d99..f77e981e62c 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 869706a574c..354709d8440 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 4d8aa04446b..4e8da469bc9 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 c8a0c32d7a9..ea83a5be2dd 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 535eafd2199..4d7a791597b 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 912eb9aa395..d6839c71def 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 c2fbb79c193..b6bb896a6a6 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 c195c5636b9..033e30432aa 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 c195c5636b9..033e30432aa 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 ccbc3504f98..474010e2dbe 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 2f18d29e1b0..00d72cb19c7 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 84964e3b1da..c360340c3e7 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 faafce02099..ab5b60c5a13 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 59f30e23647..0637bc24f3b 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 2d4c79e971e..553e4e9377f 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 53fe1bcbb7c..f2405856e3d 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 2623e610bea..9789dd1062e 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 47664515b3b..e598f52f01a 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 402166c9f4d..2648ddb539f 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 c71e41179b7..d6996ee4c2e 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 c71e41179b7..d6996ee4c2e 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 386b4ecdc92..30c66f8e764 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 95b3bd20df0..8c009cab923 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 7882e5e214f..51a972afb04 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 d26fb81c2dc..2743755c7f5 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 f50c65f0a47..4e352564c08 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 7d51514e4fd..5f455554036 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 7f9b3c10346..c0c4ec8cf55 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 d6ba8d34e02..6d2d9f6d438 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 163d38337dd..956b02167dc 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 01f6e6522e3..6ac94984fe3 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 e9d19cc47ac..b617aa2c1b9 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 03122c968ff..cb7b01a0b37 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 40b0eb6b5bd..3b172105afa 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 ba0de88b05d..a8da4e4ab16 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 c6ffe53da7b..ac92a79d108 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 af71abc591e..dfc271b37df 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 6ea6f2c3e76..19399dd2368 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 6ea6f2c3e76..19399dd2368 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 9d01bce3555..e1f210fb1d7 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 1f47a378383..7d1e802ed8a 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 0239ed1cfc6..f2aaff41fee 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 fc3838a11ab..f343f34ce46 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 da0414fba83..29f71ca94d3 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 da0414fba83..29f71ca94d3 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 b9c3cfc9201..565dd233d56 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 bbcb40e25de..a8c93928c0c 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 f0ec27407eb..9f9939284d9 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 1e2faaa4e14..18c0a64a48f 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 27fe27f3603..a5a2c2bc222 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 b317408e77f..bdc81e86806 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 73cd010813f..23f4bab9489 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 6fc5b2411d8..1e288c0cb0d 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 8a5cc2a0f04..987df2b5f03 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 73d28f2f028..61216f0bf80 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 c6af4924e53..d63b5974788 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 d08b0f1cca7..37c7e7d978f 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 ffbb60ab823..735d02a898b 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 ffbb60ab823..735d02a898b 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 2a374748748..5efe3e177ea 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 0527071d177..54164f9997e 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 285620ffdcf..7793aa44856 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 285620ffdcf..7793aa44856 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 9ec932779c3..9454eb28482 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 2cc0a9b8f82..24b12b697e6 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 595386a80d4..43b4af65eba 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 595386a80d4..43b4af65eba 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 6b7fdc01587..f4d24b8628a 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 ed2ff3fe789..45ca0cc193e 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 f035ea15556..f4236bc6ffd 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 f035ea15556..f4236bc6ffd 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 c45c5580d5b..3a6f3fa7484 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 c45c5580d5b..3a6f3fa7484 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 fab441dda3c..aba852f6b76 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 7df790d6b2d..9c843d1b34f 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 8c7141f72d6..32a3ed46515 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 8c7141f72d6..32a3ed46515 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
--
GitLab