From 249387ad3112a2f1d38f6f7f42e59d9b43ea5187 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 19 Sep 2013 15:05:30 +0000
Subject: [PATCH] [E-ACSL] __memory_size is not ghost
---
src/plugins/e-acsl/TODO | 3 ++-
src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_function_contract2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c | 2 +-
90 files changed, 91 insertions(+), 90 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index a02b796d2f0..07864bf4047 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -19,8 +19,9 @@
- logic functions
- disjoint and complete behaviors (cf. Bernard's feature wish)
- loop variant
-- grep "not_yet" *.ml
- logical shift (at least in non GMP mode)
+- let-in
+- grep "not_yet" *.ml
########
# CODE #
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 3b3ca403e8a..a0318bfaab9 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 38ce731e0a0..bd18e36abde 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 38ce731e0a0..bd18e36abde 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 b5dc0547cc2..1e622200510 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
@@ -57,7 +57,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 b5dc0547cc2..1e622200510 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
@@ -57,7 +57,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 8247aa4992b..36ab63332e1 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 fcee7f175df..89fa5f21b5b 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
@@ -143,7 +143,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 c765bd1a860..015b35c243a 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 f71079b2b56..87fb64c5b7a 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
@@ -56,7 +56,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 adb8d3f3949..4c602ab97f6 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
@@ -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_at2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
index 1873c61ab0c..00e3ebcd609 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
@@ -111,7 +111,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 84d80fddce8..3f26caf2671 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
@@ -74,7 +74,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 84d80fddce8..3f26caf2671 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
@@ -74,7 +74,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 fd29f6f50aa..0160cac5eaa 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
@@ -67,7 +67,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 6d5eca108d2..b872ad3acc4 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
@@ -121,7 +121,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 45db6aa2ea3..f44557de11f 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
@@ -58,7 +58,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 30baaf36a7c..5911ab58328 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
@@ -112,7 +112,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 baf3324a7a3..1b88864c5e3 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
@@ -59,7 +59,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 7458a7b0141..2fda90e2b44 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
@@ -101,7 +101,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 15f35cd5da0..4c531e56922 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
@@ -64,7 +64,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 374f6e4e8c9..e56b1063601 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
@@ -118,7 +118,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 ece5f598615..8a8c27d00a5 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
@@ -73,7 +73,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 ece5f598615..8a8c27d00a5 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
@@ -73,7 +73,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 cc50b25167e..ad98bcaa035 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
@@ -119,7 +119,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;
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 adf78f451cc..a822b5d1d22 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
@@ -165,7 +165,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;
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 06a3fc11150..8c31c2be641 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
@@ -52,7 +52,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 45b976cd0c2..45e2779238a 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
@@ -74,7 +74,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_call.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
index 5be9e13a315..22cc9127f74 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
@@ -82,7 +82,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;
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 5be9e13a315..22cc9127f74 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
@@ -82,7 +82,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;
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 aa39b2d317a..0e0116db4b0 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 843262da152..f0380484b9a 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
@@ -82,7 +82,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 fc83ac463e5..9f6b718deff 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
@@ -44,7 +44,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 7c04b61e3aa..242e3ed9de1 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
@@ -82,7 +82,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 0acbead3158..d58163f6eae 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 0acbead3158..d58163f6eae 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 4ff593abac4..065fcd3a5af 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 4b38a411b4f..439d27cdee2 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
@@ -74,7 +74,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 7fc2a37b8b0..2639706e849 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
@@ -75,7 +75,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 f285d9af85d..86886d6ea0f 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
@@ -89,7 +89,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 d9b773df2af..c402d80e4b0 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
@@ -58,7 +58,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 4bf8fa7ca42..db41d63ff1b 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
@@ -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_invariant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
index 9766e975635..36bb23f2f4a 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 cac4f9f5601..99b21692ac6 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
@@ -56,7 +56,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 3f7d2a0d79c..78eb6439248 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 665a2ba7cca..49e3d41cd17 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
@@ -56,7 +56,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 daf1108de6c..0214f345a1a 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 0ad85db3985..20f32dc1f19 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
@@ -84,7 +84,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 12112426a52..339de2ad9a8 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 9ff25d12ee2..90634371c74 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
@@ -86,7 +86,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 38f5fc307d2..60cd8c741c2 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
@@ -74,7 +74,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 34412b95e25..1a56981dacf 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
@@ -96,7 +96,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 9575a1af7e8..a747e0f120e 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
@@ -94,7 +94,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;
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 9575a1af7e8..a747e0f120e 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
@@ -94,7 +94,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;
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 92f224da6a1..ac20ccb0b85 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
@@ -111,7 +111,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 ffa38aecaff..d43da113978 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
@@ -107,7 +107,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 c8d331edc7c..793907b521a 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 fae1d6072a7..658a5be7b19 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
@@ -96,7 +96,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 ef2552990a1..533e4005411 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 04594103a97..0ced9c9df11 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
@@ -56,7 +56,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 1c0d0332fa6..ae8fc87a09c 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 26339cbef18..07ed6a8b54a 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
@@ -56,7 +56,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 32f5d86c996..622632d2f58 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 32f5d86c996..622632d2f58 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 afa63f7ba33..82119838d46 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 a58807aaba4..cbf8fc10b2c 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
@@ -60,7 +60,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 f53a0ce559e..74807c6ded6 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
@@ -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_ptr2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
index f412c98ea21..8badf9bff2f 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
@@ -127,7 +127,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 60c19368ccf..1b69d5b87f9 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
@@ -80,7 +80,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;
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 60c19368ccf..1b69d5b87f9 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
@@ -80,7 +80,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;
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 68298283100..9d5de4c6142 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 cc5e68a6ace..f22fcce7a0e 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
@@ -112,7 +112,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 fadefe1f3e4..afc317085a4 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 598dfd06302..af96189d5f5 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
@@ -78,7 +78,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 863e5ba0a29..af9745bdbba 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 1cfac9428e1..cb3a469567b 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
@@ -56,7 +56,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_stmt_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
index 6db54aa859e..b5b19adb7d1 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 d65ca485419..958c110111f 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
@@ -74,7 +74,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 8e1101b3c27..69b21a7190f 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 8e1101b3c27..69b21a7190f 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 eecf507b2d7..055b304e4d7 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 46f9f4d8717..18406e17f11 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
@@ -67,7 +67,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 f515828c7de..650bf234c54 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
@@ -115,7 +115,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;
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 f515828c7de..650bf234c54 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
@@ -115,7 +115,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;
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 feeade9ce0e..8be2b64352b 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
@@ -119,7 +119,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;
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 553033f26ca..206cdf6b927 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
@@ -133,7 +133,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;
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 2f82ee66383..376bde687ed 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
@@ -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_valid_in_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
index 2f82ee66383..376bde687ed 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
@@ -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_vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
index 939790becc1..a58e7d18889 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
@@ -105,7 +105,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;
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 a77d7b0fd86..bb49efe02e3 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
@@ -127,7 +127,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;
assigns __fc_heap_status \from size, __fc_heap_status;
--
GitLab