diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index a02b796d2f0e0c783a5d7bb3dbedac33133028dc..07864bf4047d9d9aab541a8e342d3f2685f0bec7 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 3b3ca403e8a0df5a9149812118ecc8ae8f001393..a0318bfaab9dbdf48780f5256984944a2253e01f 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 38ce731e0a0e0ea119f9f13d3f0249b83b91ec1c..bd18e36abde7a0fee4c31bbcae789a2774719349 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 38ce731e0a0e0ea119f9f13d3f0249b83b91ec1c..bd18e36abde7a0fee4c31bbcae789a2774719349 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 b5dc0547cc2270bcd7ff5b0b131f31cf671003e4..1e6222005104d76c9f01c61cf3ad794999e20ae2 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 b5dc0547cc2270bcd7ff5b0b131f31cf671003e4..1e6222005104d76c9f01c61cf3ad794999e20ae2 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 8247aa4992b277a595fe1a382605022369903f86..36ab63332e1ebc015ae646538a516e13639d74a6 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 fcee7f175df00f75de5e67b904699e0d92aeeb7a..89fa5f21b5b6608d4e8e2d49923f311c80959954 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 c765bd1a860143148c2b182ed6978dee10a24bf9..015b35c243ae8db3efe12eabd530086ac8aeecff 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 f71079b2b5672c6c1b46bf6f23f60c5b79c327fa..87fb64c5b7a25fa3817243d03f56eb6af13592f4 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 adb8d3f3949fe93e7a729d3a7b686e6aac6dba5f..4c602ab97f6e850e171308b85bb2d9dc75de043b 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 1873c61ab0c559c85ae2071edfe4c105fe6d9ef3..00e3ebcd6097ca40468aabf5b89291d66e120538 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 84d80fddce8f8061fa5d31c71bc04d4ff6c15cdc..3f26caf2671710847f5159aa0939bc130f76d787 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 84d80fddce8f8061fa5d31c71bc04d4ff6c15cdc..3f26caf2671710847f5159aa0939bc130f76d787 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 fd29f6f50aa43cffbd70229b1e883bba9a2382ca..0160cac5eaa4e411fb63a45e98959a8b0a348268 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 6d5eca108d242f969ef7b342f3f568459898518d..b872ad3acc42453d09f70c26cbc551c90d60d886 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 45db6aa2ea30754a463caa9f42c03458755a3a46..f44557de11f21bb2d59b009fb6cde6b555f3a301 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 30baaf36a7ca6d1ea0e25981368564bab247fe84..5911ab58328e30d2b271693caa8b86989a18c934 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 baf3324a7a303cd8b52fbe8cffe3888d727ea794..1b88864c5e3a4fa42eda0c3ed152d3c70709a87d 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 7458a7b014177423d2bfde6648ea6dfa1123f58b..2fda90e2b44eea76ad5e4d822ed3679f6ee810df 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 15f35cd5da0d3118f781614cebcd2e4905d7f4fe..4c531e569225ba2ab31193b9ab4a5ffd6be9521c 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 374f6e4e8c9313879619d80ce061b86b79b73575..e56b1063601b04e5f015e52304b65bb579cf5222 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 ece5f59861545ecf0cd2e727153300fd4cf88038..8a8c27d00a5a50d1ce3c0b950ecee8b5e0409294 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 ece5f59861545ecf0cd2e727153300fd4cf88038..8a8c27d00a5a50d1ce3c0b950ecee8b5e0409294 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 cc50b25167e9af84ef05b9067982b9ff5b1108c2..ad98bcaa03554f74820b69253d18dc1f2943cf43 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 adf78f451ccfffa529e5333bb4d4ea7589cefb81..a822b5d1d225e6d115a6cb63da0f94d10d6200f0 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 06a3fc11150c6e82ed7f0e3b3cf4e6f8276e4a5d..8c31c2be641c86133c8efd6e1fbc119dfc775411 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 45b976cd0c2a51f02c80f487a0244573cb8b5697..45e2779238a804e2e638dc76c69b94894445452a 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 5be9e13a3155a9d5d6d2159c86a470b51d64136a..22cc9127f745bab244f9aa9328f58ab4ab7ed53a 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 5be9e13a3155a9d5d6d2159c86a470b51d64136a..22cc9127f745bab244f9aa9328f58ab4ab7ed53a 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 aa39b2d317a82f1cf1b25bbcc01326f54a2ac159..0e0116db4b098d32cc95293acb6e3e1ffb522fb5 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 843262da152ec16b1d8db2d3ae8c12f20bfbc610..f0380484b9a44f6774b3f90aa33acd7c754d5425 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 fc83ac463e5b9910891f2d4c423abedb6b51af05..9f6b718deff187a13ec22db5cd10c7ce7ca7cd83 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 7c04b61e3aa1bffe0f90a6a6a1e4e91f6f3af1c0..242e3ed9de19c8e64d77f473e7260fe59a9c3924 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 0acbead3158b8a94b1fc1343d2800d3902c870c2..d58163f6eaef9efcfff1a05e4fab8675572d0655 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 0acbead3158b8a94b1fc1343d2800d3902c870c2..d58163f6eaef9efcfff1a05e4fab8675572d0655 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 4ff593abac462a51cf0f7101c755c760df6b1fbf..065fcd3a5af1f2d9f72ebe8c8b6af7dfd6eb640c 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 4b38a411b4f17f5ccd6e7c64d02576943b389aff..439d27cdee290cbe92a98c2e0913104fe87c37f3 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 7fc2a37b8b0ea326cd4fb5c28fd6747ab173f3fa..2639706e849b8b43af713d7f12afab325532c7f0 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 f285d9af85dd3c2deddc935230c4acbda2ee21cd..86886d6ea0fd5f08064b44dd84a2e4cb4a52c845 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 d9b773df2af25ed851c6fdf3a772b75ab649e7b8..c402d80e4b06e75565f602a97c92dba04d9512f5 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 4bf8fa7ca42590608afc984401c97a5e0b260ab1..db41d63ff1bba4cb3b8fe8183c81862e358f0a06 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 9766e975635bafa886aa55e78e37a62ed0607d9a..36bb23f2f4a61506806af9c0a0fbd7264c76ee55 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 cac4f9f5601c5a283f2c518531c384b3b7bb6988..99b21692ac63e95ec306aa765f9f6f0392dfed81 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 3f7d2a0d79c8925862fff3e0b6167d8f25ba90bb..78eb643924895c3c0434662e3b46340fef134b3e 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 665a2ba7ccab3eaada1fdc38c55df744a54f5b1e..49e3d41cd17a27fe5f181fad9a27e2fbe49d30be 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 daf1108de6c05159db0d92ade68ec9b724aec005..0214f345a1a077e2c747c31ef3d4b907904b13a0 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 0ad85db3985dace5fa2f82f1d9bf85481c75153a..20f32dc1f19dd3a015e370d0f2737acccd82665a 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 12112426a52f0e04e65be70ef0f6c6c1eb880f53..339de2ad9a8276fed2ebc64a1246cdb5730d2c66 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 9ff25d12ee2a6839d45235d930d6fbb6021334ce..90634371c74f520013ea6349cf3f2e06a4ce4f15 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 38f5fc307d28975e2fc4ecca0d098bcdc2f93092..60cd8c741c20cbd3d7b1397bfcf53180272e3783 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 34412b95e2544fb8f3e35bb129eba1bb2b0b711f..1a56981dacf06ec89a5e1dbf4babcb6892457a1a 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 9575a1af7e8bff67c13af651014997716b84b5f0..a747e0f120eec68572cc29619096144c9d24dabe 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 9575a1af7e8bff67c13af651014997716b84b5f0..a747e0f120eec68572cc29619096144c9d24dabe 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 92f224da6a17f38660d7ebd6b398c498d0b071ae..ac20ccb0b858fa54bc8d32be7790db1f7b8b79d7 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 ffa38aecaff37e843cf3ecec7550679a0dbafc4a..d43da1139780302eb1022debb3f201e652f38b85 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 c8d331edc7c550479e6c5fbd1dbb892f9789bb94..793907b521a858c8cf019cc6e858e097a4bf84b4 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 fae1d6072a7360c0a2799a6bb1b1a9cd4f70ad14..658a5be7b19f5bc8220f5581e4298b1dd5750c5c 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 ef2552990a1491d903742077e94d975fb4519e07..533e4005411a8deb418910b12a45c9701b23a8e9 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 04594103a97d13b8e476b64833db50a8747f9d04..0ced9c9df1141e6468068460f46cf82e7cb65a14 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 1c0d0332fa6028a385857033e928aa84ac84ee51..ae8fc87a09c6fc9e603b28c7b0a19f7123bc3991 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 26339cbef18a66d5da7c5a78006e90980973be8e..07ed6a8b54a678073282183fb5937deac9547146 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 32f5d86c99626cd7364507460b2d14078add2108..622632d2f58aad883adedaf94cc757c2017c4121 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 32f5d86c99626cd7364507460b2d14078add2108..622632d2f58aad883adedaf94cc757c2017c4121 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 afa63f7ba33e0979922bfdcfed8e37ce6e0e29a1..82119838d461d91a924d3de5138725ebf6e105f9 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 a58807aaba4e7e5d81ac9a00a7b25058649ce121..cbf8fc10b2cc9098354686b7cc75a6fed3e38d03 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 f53a0ce559e4a80f607d14695d6eefc775b53ee6..74807c6ded65c5ff331480ea30efc247a31b416c 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 f412c98ea2165b2e19f5073ded05b3cf4e0f74b2..8badf9bff2fe0435b24554dc83de8cd272c19a57 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 60c19368ccfb846ea10c36969f9242e3f3ebef0e..1b69d5b87f97bddb52c7b5a18bdf4bd0ba7434ef 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 60c19368ccfb846ea10c36969f9242e3f3ebef0e..1b69d5b87f97bddb52c7b5a18bdf4bd0ba7434ef 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 68298283100daf32b9d4a9b96b461ac88a80906e..9d5de4c61421c1911d8de8737c45cd36b64d4268 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 cc5e68a6ace6245ce8c426f7a0cbd1659fc59f1e..f22fcce7a0ea34224f77d42d19fd7b980666d501 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 fadefe1f3e4dd1b22887eb41dd864ead6f18f3bc..afc317085a47394fc7405e9b4f01c87b2750f7a5 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 598dfd0630287ef6927db8fe3cd7cf307df13c1f..af96189d5f55802f66cd4efd36c61f7338057b51 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 863e5ba0a29c55b08fbb8ffefa3a5a95f70f9d04..af9745bdbbada3c32a265520f868db89d666e1f8 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 1cfac9428e118d359a554e7c45ad4e9a12ca6600..cb3a469567bf26d09b52250c9ba65406a0e1ee6c 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 6db54aa859e440e04b04ac9a53e236aa6b15b96d..b5b19adb7d1f54d3ab5fd435bd2e722818bad3d6 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 d65ca485419cbf8c38cea5c84a7371df210c54fb..958c110111f8b638ad1133235c34695716f20e66 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 8e1101b3c274577c907db2076ca18e7e38f7b5a9..69b21a7190f39cd6c42277f11be16a3e69bac8fa 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 8e1101b3c274577c907db2076ca18e7e38f7b5a9..69b21a7190f39cd6c42277f11be16a3e69bac8fa 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 eecf507b2d7032218855b88f1b129b41d47ab47d..055b304e4d7ba89b3e100f196685ff5522a4d638 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 46f9f4d87175b5f910843887a5a45390d88f6960..18406e17f1101dd1c19ce41bcf8d920e42fe3a06 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 f515828c7de62eeada75c2f8dfdb6521214d9b63..650bf234c545135411436f2afd5beb86a4d50013 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 f515828c7de62eeada75c2f8dfdb6521214d9b63..650bf234c545135411436f2afd5beb86a4d50013 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 feeade9ce0e205d0a507d5042ae23b9d845b0431..8be2b64352b79c88b0007defcbaf975d6b1d2505 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 553033f26ca89298a91f9a57e4e54caaf481d638..206cdf6b927ca0dc762144973016a78661d3774f 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 2f82ee663838b22927a733bb0c85aa368682f4ab..376bde687ed0032dc17b793baaa1341e2a86eb6c 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 2f82ee663838b22927a733bb0c85aa368682f4ab..376bde687ed0032dc17b793baaa1341e2a86eb6c 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 939790becc10a26e0152fa70698ebf13ad1812f4..a58e7d1888904be5cc9fcf8fada67bc84bbbf34a 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 a77d7b0fd86e8f92080d03da9b9dd9db8a943242..bb49efe02e3bf955e6214b8d5c9c1baac30491d2 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;