diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 78d485f3c20fa13e5098968a1bc9e0c55b212f36..8336ee75a9c1c3d0d3a976549a3bf5ad53b3333d 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2014/03/17] Fix bug #1715 about -e-acsl-full-mmodel which
+ generates incorrect code.
-* E-ACSL [2014/03/17] Fix bug #1700 about non-ISO empty struct.
###############################
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 1910afc7b8a96888d46a5e019e14f96d374dd0e2..7454e06c2c1399233454b94b554563a11eb80129 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 */
-extern size_t __memory_size;
+/*@ ghost 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 bd18e36abde7a0fee4c31bbcae789a2774719349..38ce731e0a0e0ea119f9f13d3f0249b83b91ec1c 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; */
-extern size_t __memory_size;
+/*@ ghost 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 bd18e36abde7a0fee4c31bbcae789a2774719349..38ce731e0a0e0ea119f9f13d3f0249b83b91ec1c 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; */
-extern size_t __memory_size;
+/*@ ghost 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 d2ea17e8280590b14863adfd5f6b5deff3cdb4df..78d13f82b67c368ee3a63855fa688aa47c86a5b2 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);
-extern size_t __memory_size;
+/*@ ghost 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 d2ea17e8280590b14863adfd5f6b5deff3cdb4df..78d13f82b67c368ee3a63855fa688aa47c86a5b2 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);
-extern size_t __memory_size;
+/*@ ghost 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 971e9bac5cb5b3615e684fb6f4e3a0eeb491526f..21d3dee0e0f030f66ac342a53dc280c04406bcb0 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);
-extern size_t __memory_size;
+/*@ ghost 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 971e9bac5cb5b3615e684fb6f4e3a0eeb491526f..21d3dee0e0f030f66ac342a53dc280c04406bcb0 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);
-extern size_t __memory_size;
+/*@ ghost 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 36ab63332e1ebc015ae646538a516e13639d74a6..8247aa4992b277a595fe1a382605022369903f86 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; */
-extern size_t __memory_size;
+/*@ ghost 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 489a47330d4ca861b06a431f0ca326f8e12910dd..820086317114462508624a70a06064a4945a2433 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; */
-extern size_t __memory_size;
+/*@ ghost 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 015b35c243ae8db3efe12eabd530086ac8aeecff..c765bd1a860143148c2b182ed6978dee10a24bf9 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; */
-extern size_t __memory_size;
+/*@ ghost 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 8b4d0850ca16b11ffb656b21b294ba76d84ca746..bf258eef4aa8b408b9f9f6614ed08ae1140ea16b 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; */
-extern size_t __memory_size;
+/*@ ghost 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 dcc63bf13794831382cc743092f8a56ad8e4615a..7e96f4e79052c789e709ed1994a7b36f05f1db06 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);
-extern size_t __memory_size;
+/*@ ghost 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 d873c78c0cf19c6c62a23ba95adaa8b3d69c1b51..3da7bdfbfa61874ceea3bdeaf71462c707bb30fe 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);
-extern size_t __memory_size;
+/*@ ghost 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 4d60ecb29f7e69e62d6bc66782a09c3b43cacace..efdb482b820a7b5c40527c92f786aac9dcdd94c6 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);
-extern size_t __memory_size;
+/*@ ghost 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 4d60ecb29f7e69e62d6bc66782a09c3b43cacace..efdb482b820a7b5c40527c92f786aac9dcdd94c6 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);
-extern size_t __memory_size;
+/*@ ghost 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 d569807f0cad5e63e4a7d50c831e8642fac0f3ab..31a9781a1007907da2d0e67b2dda838bd09e2074 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);
-extern size_t __memory_size;
+/*@ ghost 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 1df025d2ea74699ff253d0caa17020c4b0edc339..3b4af93775d4e858061c87f93a503a03dc7ff2ab 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);
-extern size_t __memory_size;
+/*@ ghost 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 85bd3898d745c1055c6226158879b03756ad28e2..560261c0f557090fc2db80dc6af50b238e3b0580 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);
-extern size_t __memory_size;
+/*@ ghost 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 c90ffec48ba377692f79cf6ce599a225098d45d0..89edfb78504c7af7a6753a678d3f93c8c27952e0 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);
-extern size_t __memory_size;
+/*@ ghost 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 7a8f09a8ea5d20dd57f8c95f08112c6fef405943..eb2080fc217d181bed7ae86727654bba84fd810b 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);
-extern size_t __memory_size;
+/*@ ghost 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 2aee796a1207b5472376acf338c8cbe99258da0c..8c3ebbe99700f48e7476ffde0cfdbf6f473e803d 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);
-extern size_t __memory_size;
+/*@ ghost 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 f869f9352a6a5a028c3c291dde80e315dda59387..2b98891e4a70b7f4f3c062cb2785dbf22e4b3c07 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);
-extern size_t __memory_size;
+/*@ ghost 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 dd862826c73d01b9c8dcc8b61686a889a4a933c8..b4ea1d9be57be3006931d9da16780fea4f06541e 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);
-extern size_t __memory_size;
+/*@ ghost 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 9866acdacf7365137e57b4ad742efa8eb9517266..f09bf2f1116c0f70e52d9f3e87d324ccc6b27974 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; */
-extern size_t __memory_size;
+/*@ ghost 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 9866acdacf7365137e57b4ad742efa8eb9517266..f09bf2f1116c0f70e52d9f3e87d324ccc6b27974 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; */
-extern size_t __memory_size;
+/*@ ghost 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 80855417abaa467a8f230b9c5d7fa4f8788cad96..45a8c5865d8ec62066579026e41ee9a880ad12fe 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);
-extern size_t __memory_size;
+/*@ ghost 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 89d751bccd4a3791138705820201c79ae7a37cd8..9b75f0ffe84564c135e12bad95eabd3e811ef524 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);
-extern size_t __memory_size;
+/*@ ghost 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 4c2e650b0627c1739f590b340e6b9ea8da3caa16..d9defb9f39085df3a61f9f88a36b6afd350f806e 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);
-extern size_t __memory_size;
+/*@ ghost 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 e8a08dd3c5ac398e5eff581a74b306079ff2cebd..2f5253714910fda4ff031c1058dcd8c4d0e1a4db 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);
-extern size_t __memory_size;
+/*@ ghost 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 678a82b6e694e6fcd652dcc99f1c04476ef6021b..7258ddac41bf74445d8b0d57912d430c70f90095 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);
-extern size_t __memory_size;
+/*@ ghost 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 926d19e3528202503c0d3df18a55e7776e645ae9..4287e8ff2714275b64a6c3ba9de8f6dbeae8d01f 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);
-extern size_t __memory_size;
+/*@ ghost 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 926d19e3528202503c0d3df18a55e7776e645ae9..4287e8ff2714275b64a6c3ba9de8f6dbeae8d01f 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);
-extern size_t __memory_size;
+/*@ ghost 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 0e0116db4b098d32cc95293acb6e3e1ffb522fb5..aa39b2d317a82f1cf1b25bbcc01326f54a2ac159 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; */
-extern size_t __memory_size;
+/*@ ghost 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 4bf7eb61caba72a833cf94fe6cc373922d229a49..291d9b6fdc6db0e2bfeb1adcf8df77a4bf982024 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; */
-extern size_t __memory_size;
+/*@ ghost 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 cf0c7a9ac40009441703e54aeea96d99bb19f7b7..ceb5d2b3fa7d5e2b05376c4519a9e3336fad3520 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; */
-extern size_t __memory_size;
+/*@ ghost 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 8d740e38f9cf649f865cecacf65cb2eba4552641..5759207338083c55c108456a88bb4448b11e0aad 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; */
-extern size_t __memory_size;
+/*@ ghost 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 d58163f6eaef9efcfff1a05e4fab8675572d0655..0acbead3158b8a94b1fc1343d2800d3902c870c2 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; */
-extern size_t __memory_size;
+/*@ ghost 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 d58163f6eaef9efcfff1a05e4fab8675572d0655..0acbead3158b8a94b1fc1343d2800d3902c870c2 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; */
-extern size_t __memory_size;
+/*@ ghost 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 065fcd3a5af1f2d9f72ebe8c8b6af7dfd6eb640c..4ff593abac462a51cf0f7101c755c760df6b1fbf 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; */
-extern size_t __memory_size;
+/*@ ghost 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 856dc063c317c7a215dff83a2835ec723d5ed761..18ed30062a9047a7c040b1997af25ec767a75a13 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; */
-extern size_t __memory_size;
+/*@ ghost 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 239eee72fa6191ec25cf9d4b916c2c130bd2d944..c8f1be53be9640ee9d3877e1b9927cc4d6dd487d 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);
-extern size_t __memory_size;
+/*@ ghost 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 2deb07329805d87ae4a4b86445210e61d5a9eef8..d117e37824f81a1787743d3fcb9d9d4986aefbf7 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);
-extern size_t __memory_size;
+/*@ ghost 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 832651941592a06b88d4e09966f3ff82dee4b47e..596b7b58c76cbd7859636f3ab82d3b348314657d 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; */
-extern size_t __memory_size;
+/*@ ghost 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 06d19150607000d59921da84b59fa0cd1626a22c..24f06299028b9211179101a8f3bf4947f93cb32b 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; */
-extern size_t __memory_size;
+/*@ ghost 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 36bb23f2f4a61506806af9c0a0fbd7264c76ee55..9766e975635bafa886aa55e78e37a62ed0607d9a 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; */
-extern size_t __memory_size;
+/*@ ghost 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 576103c144095a8b2f1399f84c6fcbfe33bdf07c..13d42707706e11ac2d102ed1e9e75f5b8e469227 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; */
-extern size_t __memory_size;
+/*@ ghost 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 78eb643924895c3c0434662e3b46340fef134b3e..3f7d2a0d79c8925862fff3e0b6167d8f25ba90bb 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; */
-extern size_t __memory_size;
+/*@ ghost 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 6a0ecaa8d795915450edfe041e2937314557a926..36cffb7e59c81717cca1db5d380dd1940e68f000 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; */
-extern size_t __memory_size;
+/*@ ghost 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 0214f345a1a077e2c747c31ef3d4b907904b13a0..daf1108de6c05159db0d92ade68ec9b724aec005 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; */
-extern size_t __memory_size;
+/*@ ghost 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 038f318bd6530c2b895f95b62b77f405fde89fbf..7482fd27fd74c812d4f7c825fbfa40f08912ca22 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; */
-extern size_t __memory_size;
+/*@ ghost 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 339de2ad9a8276fed2ebc64a1246cdb5730d2c66..12112426a52f0e04e65be70ef0f6c6c1eb880f53 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; */
-extern size_t __memory_size;
+/*@ ghost 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 cf504ffbb74929a3b4174475bd4d220b7591b112..42e1ad147407904ec6b650760a3556f148b9db2b 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; */
-extern size_t __memory_size;
+/*@ ghost 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 36d2abc560bfc1f03781f1969b5e0bb648f12699..3223de6d50ba6fb17b9dcf5e6e16cbf98fb61ad2 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);
-extern size_t __memory_size;
+/*@ ghost 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 be124fbfe05c48f68fc4a852923055c7d4590e0c..9f6168dcc9a5e92b35164120addc3adeb4bb02f7 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);
-extern size_t __memory_size;
+/*@ ghost 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 c4682298ae89e5c9ce779e862b5d2d885b801e73..49b0543c428a69df2f67918a0a871d52c6f411b8 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);
-extern size_t __memory_size;
+/*@ ghost 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 c4682298ae89e5c9ce779e862b5d2d885b801e73..49b0543c428a69df2f67918a0a871d52c6f411b8 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);
-extern size_t __memory_size;
+/*@ ghost 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 1ef9196616e46ccc66aef93d27231aa9a929797e..c03705c4cf4c88fecb78112efa5f35308c6aa614 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; */
-extern size_t __memory_size;
+/*@ ghost 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 0ca615298b0d98d104cd1856578c0a2b2d5eb3a3..1adfb29a18108f461487273c013749d66cffb736 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; */
-extern size_t __memory_size;
+/*@ ghost 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 793907b521a858c8cf019cc6e858e097a4bf84b4..c8d331edc7c550479e6c5fbd1dbb892f9789bb94 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; */
-extern size_t __memory_size;
+/*@ ghost 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 d7b1519c37153277fe7fbf0c1cd44847defd0912..cad4c41a492a588be98576c86e287205451fb83c 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; */
-extern size_t __memory_size;
+/*@ ghost 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 533e4005411a8deb418910b12a45c9701b23a8e9..ef2552990a1491d903742077e94d975fb4519e07 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; */
-extern size_t __memory_size;
+/*@ ghost 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 f9c0b314106097063ae5e379b6e45dba9de37554..e44f41c1996a57d9e12e6f7c86becdec64587faf 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; */
-extern size_t __memory_size;
+/*@ ghost 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 ae8fc87a09c6fc9e603b28c7b0a19f7123bc3991..1c0d0332fa6028a385857033e928aa84ac84ee51 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; */
-extern size_t __memory_size;
+/*@ ghost 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 044e8f2bd342eee199b36916c50e21eb9c408a5b..9a26741265bbe2a4ff8713917c7430f6e12db4f1 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; */
-extern size_t __memory_size;
+/*@ ghost 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 622632d2f58aad883adedaf94cc757c2017c4121..32f5d86c99626cd7364507460b2d14078add2108 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; */
-extern size_t __memory_size;
+/*@ ghost 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 622632d2f58aad883adedaf94cc757c2017c4121..32f5d86c99626cd7364507460b2d14078add2108 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; */
-extern size_t __memory_size;
+/*@ ghost 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 82119838d461d91a924d3de5138725ebf6e105f9..afa63f7ba33e0979922bfdcfed8e37ce6e0e29a1 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; */
-extern size_t __memory_size;
+/*@ ghost 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 8b4876e0a963072053464b4ed25156665405ac38..3ad84cb6966ff8e0be24c1e57320cdc16f4a624d 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; */
-extern size_t __memory_size;
+/*@ ghost 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 e75b9fa3be85a0bc09caff337b77b42b6ad99091..f854d7b49be46cdf62b315b95428029093d74556 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);
-extern size_t __memory_size;
+/*@ ghost 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 7c955be14206bf6984ba595acf9e416fb5a87aca..44d9f3c173f4765c975913345a70f92504e91329 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);
-extern size_t __memory_size;
+/*@ ghost 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 2f8b23a278dd672358626d97290667a7e921b60f..c545933f565de0de097c0df20e399148c16990cc 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);
-extern size_t __memory_size;
+/*@ ghost 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 2f8b23a278dd672358626d97290667a7e921b60f..c545933f565de0de097c0df20e399148c16990cc 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);
-extern size_t __memory_size;
+/*@ ghost 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 9d5de4c61421c1911d8de8737c45cd36b64d4268..68298283100daf32b9d4a9b96b461ac88a80906e 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; */
-extern size_t __memory_size;
+/*@ ghost 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 e5cab98bdc5504e812ccd65cf2f31343e0c67ab9..ee2348c85abb33d831fea492d0ada74b81bf9d28 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; */
-extern size_t __memory_size;
+/*@ ghost 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 afc317085a47394fc7405e9b4f01c87b2750f7a5..fadefe1f3e4dd1b22887eb41dd864ead6f18f3bc 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; */
-extern size_t __memory_size;
+/*@ ghost 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 dbfac58a24a4dadb5d569c8cb4104ec3fcf87060..6ec0ed2c7c3b2513bc15bd5d47694adcc840bbba 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; */
-extern size_t __memory_size;
+/*@ ghost 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 af9745bdbbada3c32a265520f868db89d666e1f8..863e5ba0a29c55b08fbb8ffefa3a5a95f70f9d04 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; */
-extern size_t __memory_size;
+/*@ ghost 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 9c6acd338d564c44a0cf79b06c646f20b7c28183..9eb072c28e9e88766e62ba30e11221227be11cee 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; */
-extern size_t __memory_size;
+/*@ ghost 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 b5b19adb7d1f54d3ab5fd435bd2e722818bad3d6..6db54aa859e440e04b04ac9a53e236aa6b15b96d 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; */
-extern size_t __memory_size;
+/*@ ghost 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 1207af4bf99035c4d88c7adb7b10d979d5462659..b52f58679e5d7326aaba30891ae6cfb041a92c21 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; */
-extern size_t __memory_size;
+/*@ ghost 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 69b21a7190f39cd6c42277f11be16a3e69bac8fa..8e1101b3c274577c907db2076ca18e7e38f7b5a9 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; */
-extern size_t __memory_size;
+/*@ ghost 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 69b21a7190f39cd6c42277f11be16a3e69bac8fa..8e1101b3c274577c907db2076ca18e7e38f7b5a9 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; */
-extern size_t __memory_size;
+/*@ ghost 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 055b304e4d7ba89b3e100f196685ff5522a4d638..eecf507b2d7032218855b88f1b129b41d47ab47d 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; */
-extern size_t __memory_size;
+/*@ ghost 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 9642f673908e63ffc3d517f81649b7f80b5438a8..624b42cfe889dfe466c516ebfd8043e14d2f0843 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; */
-extern size_t __memory_size;
+/*@ ghost 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 f392e58ad62cd3a0381a22ebd5a9334f808e677a..6b7354a356dbad21526e2603c23c3dbc97711008 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);
-extern size_t __memory_size;
+/*@ ghost 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 f392e58ad62cd3a0381a22ebd5a9334f808e677a..6b7354a356dbad21526e2603c23c3dbc97711008 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);
-extern size_t __memory_size;
+/*@ ghost 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 478f0f72d199529fe706aa75b7393a3911bf64a9..6ac30ce1b033b4095f82841be1a55714702d13c9 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);
-extern size_t __memory_size;
+/*@ ghost 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 f526f6c0f4d402c1477c864a9a645e505b2ea0e8..1321097141898e1b21435751b8d4bca0d446aad1 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);
-extern size_t __memory_size;
+/*@ ghost 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 019bfa32a74d9524d0f5101a31f32b0d26bb1347..4cebebc641f25d981295e83f1bee48f31ec27b82 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);
-extern size_t __memory_size;
+/*@ ghost 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 019bfa32a74d9524d0f5101a31f32b0d26bb1347..4cebebc641f25d981295e83f1bee48f31ec27b82 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);
-extern size_t __memory_size;
+/*@ ghost 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 0d5a4de57612cb4457e6f5b39baa9f8775493cef..6a4bba4d5230101329af954584c32a06347ae2dd 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);
-extern size_t __memory_size;
+/*@ ghost 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 4c50717aab0841df638e3e3ba70746d6055f210b..e7645e29a7488e9c4f185cf8088f6504b80c3938 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);
-extern size_t __memory_size;
+/*@ ghost extern size_t __memory_size; */
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;