From 56a7f14eb7c4fd01d75d94d854a60ba512662da0 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Sun, 20 Jul 2014 11:06:27 +0200
Subject: [PATCH] patch the fix of bug #1715 in a way that __memory_size is
still usable (no more ghost)
---
.../e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h | 2 +-
.../tests/e-acsl-runtime/oracle/empty.1.res.oracle | 2 +-
.../tests/e-acsl-runtime/oracle/empty.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_array.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_at.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_call.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_comparison.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_comparison2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_false.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c | 2 +-
.../e-acsl-runtime/oracle/gen_function_contract.c | 2 +-
.../e-acsl-runtime/oracle/gen_function_contract2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c | 2 +-
.../e-acsl-runtime/oracle/gen_integer_constant.c | 2 +-
.../e-acsl-runtime/oracle/gen_integer_constant2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_invariant.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_invariant2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_labeled_stmt.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_linear_search.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_linear_search2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_literal_string.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_literal_string2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_localvar2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_longlong2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c | 2 +-
.../e-acsl-runtime/oracle/gen_nested_code_annot.c | 2 +-
.../e-acsl-runtime/oracle/gen_nested_code_annot2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_not.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_null.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_other_constants.c | 2 +-
.../e-acsl-runtime/oracle/gen_other_constants2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_ptr_init2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_result.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_stmt_contract.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_stmt_contract2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_true.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_valid_alias.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_valid_alias2.c | 2 +-
.../e-acsl-runtime/oracle/gen_valid_in_contract.c | 2 +-
.../e-acsl-runtime/oracle/gen_valid_in_contract2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c | 2 +-
src/plugins/e-acsl/visit.ml | 11 ++++++-----
97 files changed, 102 insertions(+), 101 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
index 7454e06c2c1..1910afc7b8a 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
@@ -142,7 +142,7 @@ size_t __get_memory_size(void)
__attribute__((FC_BUILTIN));
/* for predicates */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ predicate diffSize{L1,L2}(integer i) =
\at(__memory_size, L1) - \at(__memory_size, L2) == i;
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 a64cb680946..6ef9c766961 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
@@ -38,7 +38,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 a64cb680946..6ef9c766961 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
@@ -38,7 +38,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 fab581fe35d..5309e60cd67 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
@@ -59,7 +59,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 fab581fe35d..5309e60cd67 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
@@ -59,7 +59,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
index 3595848a662..000d6dc934b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
@@ -63,7 +63,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
index 3595848a662..000d6dc934b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
@@ -63,7 +63,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 474a027f305..42f1d9bddef 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 8e826c19967..bc971c55db2 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
@@ -144,7 +144,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_com(__mpz_struct * /*[1]*/ z1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 426291f1f93..550860b8b8a 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 3465af736a5..287d37fe27c 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
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 a86d2c65f52..b737ff9a321 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
@@ -63,7 +63,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 fbad827ab06..8274bfc731c 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
@@ -114,7 +114,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 45945925656..ced75079abe 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
@@ -76,7 +76,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 45945925656..ced75079abe 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
@@ -76,7 +76,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 a3882707f84..e83ffad6da6 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
@@ -70,7 +70,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 f2953f32515..3e5432daf5d 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
@@ -126,7 +126,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 97c05e9203a..96e7fb5af57 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
@@ -60,7 +60,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 669dbe87e7b..7187305f794 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
@@ -115,7 +115,7 @@ extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 d0e407c5451..8f9343ee1e8 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
@@ -61,7 +61,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 50e0edfc00c..abcc1e5f2da 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
@@ -103,7 +103,7 @@ extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
index 17b721b9dd2..6e7b2c4e8e7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
@@ -68,7 +68,7 @@ extern __attribute__((__FC_BUILTIN__)) int __offset(void *ptr);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
index 27a2a4a4de8..94d119f763a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
@@ -123,7 +123,7 @@ extern __attribute__((__FC_BUILTIN__)) int __offset(void *ptr);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
index 7cb3e53d8fe..5e7a4dda725 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
@@ -74,7 +74,7 @@ extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
index 7cb3e53d8fe..5e7a4dda725 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
@@ -74,7 +74,7 @@ extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
index d4a592d8a9f..0d1435a2cb8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
@@ -123,7 +123,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
index 3074489280d..d53e74c8f75 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
@@ -170,7 +170,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
index 356c8305d69..e521c474f04 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
@@ -54,7 +54,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
index 0e3f2d02f3d..45acef9f359 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
@@ -77,7 +77,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
index bd982bc4f57..b6de2bea6c5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
@@ -69,7 +69,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
index 58a1bbf0c1a..2ceb18f2949 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
@@ -66,7 +66,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
index 58a1bbf0c1a..2ceb18f2949 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
@@ -66,7 +66,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
index c16bdde76b0..6c0ac16ffad 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
@@ -85,7 +85,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
index c16bdde76b0..6c0ac16ffad 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
@@ -85,7 +85,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
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 d802950c13e..f60a4466aa7 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 ef9d9264b5f..ec6d146ae29 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
@@ -84,7 +84,7 @@ extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 dc712b9c16d..75a78120891 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
@@ -45,7 +45,7 @@ extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 d7ab417d961..3fb2085702d 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
@@ -84,7 +84,7 @@ extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 5c50649668f..f868895c131 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 5c50649668f..f868895c131 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 78ffa12f7d1..e1ce7c11b9f 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 9a70717d351..85c5fc2ed81 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
@@ -75,7 +75,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 8ab2658f325..f5d1e8efd05 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
@@ -79,7 +79,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 0b1470d48fd..37bdf66318a 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
@@ -93,7 +93,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 5b40837b516..e96fd92f535 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
@@ -59,7 +59,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 0b51e70cba2..8eed7fb940f 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
@@ -69,7 +69,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 de35de137c1..a3086e7756a 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 80bb06d09f8..96805b2246a 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
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 16a26a9cadd..710d5a14fdb 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 ec4b8be154f..58d35baf16f 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
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 8a626071746..0dcf8afc82f 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 59a282d47a3..a0b007954e3 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
@@ -85,7 +85,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 973a2e326c5..78b44f28a9d 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 ef1ee65866d..9c512a28651 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
@@ -88,7 +88,7 @@ extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 7838fe63692..ef102f88c41 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
@@ -78,7 +78,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 53ce9fc3add..e5d0a0280dd 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
@@ -101,7 +101,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 03b15f9c862..2b8ed535735 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
@@ -98,7 +98,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \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 03b15f9c862..2b8ed535735 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
@@ -98,7 +98,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
index 97898f346f9..c51118701e8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
@@ -113,7 +113,7 @@ extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
index bc7a9170e29..a355b7d0367 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
@@ -108,7 +108,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_r(__mpz_struct * /*[1]*
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
index de414ac3045..5358205e357 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
index af979f21b34..3b4567d368a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
@@ -98,7 +98,7 @@ extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 3dc445f2d17..2828fd2c7d8 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 ef5acd7d55f..a37818a8a03 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
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 16d7ced41ac..fb650ced871 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 5ccb318714b..4a7daa2481d 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
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 89bd9045ef4..f1cfe20bdc8 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 89bd9045ef4..f1cfe20bdc8 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 0d46e1f187d..d4e78da1104 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
@@ -38,7 +38,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 6f5faa3091b..82431c97c2c 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
@@ -61,7 +61,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 dd216a8bc8d..da9e0f50eb9 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
@@ -72,7 +72,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 066c297a322..97ed477275e 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
@@ -130,7 +130,7 @@ extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
index 908867a4633..ff3b77ce0e1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
@@ -83,7 +83,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
index 908867a4633..ff3b77ce0e1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
@@ -83,7 +83,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
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 8779cbdeabd..a808779ab9e 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 7eba41bee98..da34c241b4a 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
@@ -113,7 +113,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_r(__mpz_struct * /*[1]*
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 cc0712eb477..3feb1351016 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 40ddcec7016..83e2e2cb511 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
@@ -80,7 +80,7 @@ extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 403b4169c17..eef7334720d 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 6930a9c4741..cad3806eb15 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
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
index 758997853d3..bfb8ca6d0bb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
@@ -87,7 +87,7 @@ extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
index 758997853d3..bfb8ca6d0bb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
@@ -87,7 +87,7 @@ extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 e0bcf266375..24887d7d7f9 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 63a290eedce..981fd6bc764 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
@@ -75,7 +75,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 16f0e40ddaa..7c58c054a3b 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 16f0e40ddaa..7c58c054a3b 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
@@ -34,7 +34,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 b09462117d4..a66c8e14519 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
@@ -35,7 +35,7 @@ axiomatic
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 7d7245dcaef..fc9a529ebc9 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
@@ -68,7 +68,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 d43659faf50..2bdff399157 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
@@ -120,7 +120,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \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 d43659faf50..2bdff399157 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
@@ -120,7 +120,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \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 8187bd9b1d2..5444decbe4b 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
@@ -124,7 +124,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \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 563cb72ec73..0d609bc8857 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
@@ -138,7 +138,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \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 dc069fd655e..133d0d4c7c4 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
@@ -79,7 +79,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
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 dc069fd655e..133d0d4c7c4 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
@@ -79,7 +79,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
index 94f13e139d4..84460b287a8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
@@ -108,7 +108,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
index 5db867a9f76..95005ee9287 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
@@ -131,7 +131,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 5af377d2bf8..a7dd86cb6c0 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -472,13 +472,14 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
| ret :: l ->
let loc = Stmt.loc stmt in
let delete_stmts =
- Globals.Vars.fold_in_file_order
- (fun vi _ acc ->
- if Pre_analysis.must_model_vi vi then
- let vi = Cil.get_varinfo self#behavior vi in
- Misc.mk_delete_stmt vi :: acc
+ Varinfo.Hashtbl.fold_sorted
+ (fun old_vi _ acc ->
+ if Pre_analysis.must_model_vi old_vi then
+ let new_vi = Cil.get_varinfo self#behavior old_vi in
+ Misc.mk_delete_stmt new_vi :: acc
else
acc)
+ global_vars
[ Misc.mk_call ~loc "__e_acsl_memory_clean" []; ret ]
in
b.bstmts <- List.rev l @ delete_stmts
--
GitLab