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 7454e06c2c1399233454b94b554563a11eb80129..1910afc7b8a96888d46a5e019e14f96d374dd0e2 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 a64cb6809462cc1c4a9e0bab175ca2c94b28242f..6ef9c7669611d1f39559957f9b9a4b79e59cf32b 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 a64cb6809462cc1c4a9e0bab175ca2c94b28242f..6ef9c7669611d1f39559957f9b9a4b79e59cf32b 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 fab581fe35d6c970a4edd9b84be778aaaad4e771..5309e60cd67bb4b4352b86e4bd6ce340a9e14a63 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
@@ -59,7 +59,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
index fab581fe35d6c970a4edd9b84be778aaaad4e771..5309e60cd67bb4b4352b86e4bd6ce340a9e14a63 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
@@ -59,7 +59,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
index 3595848a6626dbd2bd6f667e492ea4ab78cb9a34..000d6dc934b62fad202de203849c7908d08df339 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
@@ -63,7 +63,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
index 3595848a6626dbd2bd6f667e492ea4ab78cb9a34..000d6dc934b62fad202de203849c7908d08df339 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
@@ -63,7 +63,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
index 474a027f30510cfa6ec4ea95bb875c90d360df1c..42f1d9bddef5612feae367dff84b506d42b94058 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 8e826c199676e88eb18b7b2dbbbfe63d88522718..bc971c55db2cf6931b0ba132037b76b90379654c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
@@ -144,7 +144,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_com(__mpz_struct * /*[1]*/ z1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
index 426291f1f93f1d02fab0a94816170dd86bea504f..550860b8b8acd4c5f03aeb85e5444f62d758cb81 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 3465af736a5a03ae431c3c76eafad3eba0938d9b..287d37fe27cbf50184dd75ce16c3efc7e0d0c9c0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
index a86d2c65f524c49a2207992c212900c731020c67..b737ff9a321e4d5a8c5a6ca1f27cbcc464470c29 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
@@ -63,7 +63,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
index fbad827ab0661a99eb57e5a6fa500878cd8c4a08..8274bfc731cb8aa688469d4acae3215d5a7e1adc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
@@ -114,7 +114,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
index 45945925656d360d54ef320de566038fcca6ea91..ced75079abe3e4fe64db32f1114dd46a55e3b24c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
@@ -76,7 +76,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
index 45945925656d360d54ef320de566038fcca6ea91..ced75079abe3e4fe64db32f1114dd46a55e3b24c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
@@ -76,7 +76,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
index a3882707f84331eddbef3f9cb447f072b0700735..e83ffad6da682a06b7902da04cea50379b4c108f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
@@ -70,7 +70,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
index f2953f325152d085c11ff40ea971aec9b4ed1515..3e5432daf5de6180c8bcf65ddeaf52387206e2c7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
@@ -126,7 +126,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
index 97c05e9203abbf57efd919e8103eb3b7f2ca84bb..96e7fb5af5796a5caaab803c34d7d2ba7a638fcf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
@@ -60,7 +60,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
index 669dbe87e7bf522a236ea4566ec8742d9a3a9b71..7187305f794b5a5fb66464d887eaf1c10800ce3e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
@@ -115,7 +115,7 @@ extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
index d0e407c5451f821e53dfef8a35d799afe52b4225..8f9343ee1e814de0136a50788db9b85fe65b8632 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
@@ -61,7 +61,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
index 50e0edfc00c9ab4a48b49e3c5be747c6554b91a8..abcc1e5f2da4681acc281ef594a6c7d42ef10849 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
@@ -103,7 +103,7 @@ extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
index 17b721b9dd2600087cd3a2a9abab40dcc6254d1a..6e7b2c4e8e7fa2b850e97426808306cf212c7aa7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
@@ -68,7 +68,7 @@ extern __attribute__((__FC_BUILTIN__)) int __offset(void *ptr);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
index 27a2a4a4de8765444722501162302424c9dee96b..94d119f763ab388903f39056bace7245da6ade34 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
@@ -123,7 +123,7 @@ extern __attribute__((__FC_BUILTIN__)) int __offset(void *ptr);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
index 7cb3e53d8fe96574acdc9e24e5b94311ff909df3..5e7a4dda72577c933f2d195b69eb3ce388cf4cbe 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
@@ -74,7 +74,7 @@ extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
index 7cb3e53d8fe96574acdc9e24e5b94311ff909df3..5e7a4dda72577c933f2d195b69eb3ce388cf4cbe 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
@@ -74,7 +74,7 @@ extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
index d4a592d8a9f2a3bab78bc0fa50a05c4102b64d75..0d1435a2cb8bfda82e042d6a957e4c48dafaa244 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
@@ -123,7 +123,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
index 3074489280dc5c55d8842a30f4a6a092a1651128..d53e74c8f753a7f177f9d4dfb58fb920b6b08cf1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
@@ -170,7 +170,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
index 356c8305d69aceb78e20d5c4a62fe79ee13eb7f3..e521c474f045bbb05d1bf32a688c291e612b26fb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
@@ -54,7 +54,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
index 0e3f2d02f3d7b54f593d9675d113fddb11cffcbc..45acef9f359afba5f9ed8a24a4a76e0254dc1b81 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
@@ -77,7 +77,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
index bd982bc4f57866c66a1a1f2745b62d97ed33527f..b6de2bea6c5d75199d9fadce244f1d9298ad53f5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
@@ -69,7 +69,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
index 58a1bbf0c1a589b4e5e64d373f722c0467e25ab4..2ceb18f29490c3c07f12991a2fc6609b01a90b77 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
@@ -66,7 +66,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
index 58a1bbf0c1a589b4e5e64d373f722c0467e25ab4..2ceb18f29490c3c07f12991a2fc6609b01a90b77 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
@@ -66,7 +66,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
index c16bdde76b03311c1253d51390f509f7dbab7023..6c0ac16ffade7b79209ef24aa8249786265722ca 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
@@ -85,7 +85,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
index c16bdde76b03311c1253d51390f509f7dbab7023..6c0ac16ffade7b79209ef24aa8249786265722ca 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
@@ -85,7 +85,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
index d802950c13eacce1febb790c3a38b576b2ce9104..f60a4466aa789998afdc9b446f52f870914a1554 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 ef9d9264b5f76853b0c05785d38c7af8c6253008..ec6d146ae29df6ef59b8c8590899afb87a4ea958 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
@@ -84,7 +84,7 @@ extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index dc712b9c16daa6b91e17d2b42e8621f8b2c06062..75a781208911e4da6be23b1b3afc75c0e1b5029c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -45,7 +45,7 @@ extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
index d7ab417d961d662cb451096b1860659f8cc9d98f..3fb2085702ddfe8547007bbdb0b01cf9b216dbab 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
@@ -84,7 +84,7 @@ extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
index 5c50649668fcb976874d7c2abf64feba0ae0a246..f868895c131db7e7df7f4fd911b7154d7ef0957f 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 5c50649668fcb976874d7c2abf64feba0ae0a246..f868895c131db7e7df7f4fd911b7154d7ef0957f 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 78ffa12f7d100dac49fbc0fd9fd3e3c461399190..e1ce7c11b9fbd82cfad25c944df851e3adca4761 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 9a70717d35144abbcc4c203e5a21be1058260dad..85c5fc2ed81053a6b01cf9a55f90bf740665ddd0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
@@ -75,7 +75,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
index 8ab2658f325d1f8326f115d39bdb81f41af42f75..f5d1e8efd05f34b9dc2cc34b5953032fb920afb2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
@@ -79,7 +79,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
index 0b1470d48fdf997b3ddfa52204aa20b803cebf40..37bdf66318a43aceb6cf49194c6974f83f98d1eb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
@@ -93,7 +93,7 @@ extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index 5b40837b51635f32daf9bcab776b7ab36e4587af..e96fd92f5354211e85c89d033d1985b62196de41 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -59,7 +59,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
index 0b51e70cba21930f4fbe82ed3a168b540f4e7ad6..8eed7fb940fbd36392d6523e2964f5d51b1036d7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
@@ -69,7 +69,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
index de35de137c1e2c6f8d349e76d9f1b603cc3f8a71..a3086e7756abf6ab3033c346110afca32dfc8d83 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 80bb06d09f8f1ee2921b55e68cfb544467fa06c6..96805b2246a83862ff90366991192502fda9dda0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
index 16a26a9cadde5ee72311ce946dca188584144e6f..710d5a14fdb19e9e000b39160ccc1166945bd376 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 ec4b8be154f74b3519a43922e834eb9cb693726b..58d35baf16fe8b77b536432918bf162f05f6c06c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
index 8a626071746007de80708a65a4867ae5bcd76c0d..0dcf8afc82ff390b23a27808bd40f61e9087d380 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 59a282d47a3d21d810c15a22f6a41625ea979ce6..a0b007954e3f75991b174763ab11c74dd0f4fecb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
@@ -85,7 +85,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index 973a2e326c50444f4fc3ba5663c410a3b7a64c83..78b44f28a9d2599d1f10d2868fe4c7eaf7138221 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 ef1ee65866d97788d9b896400c9213a233b0b95e..9c512a286510d337d0d082ec1a9ffc0ca44696bb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
@@ -88,7 +88,7 @@ extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
index 7838fe636920b059ed92e7067486cefe59f45eda..ef102f88c41ee31a1162fe4fb88d3eadd756a265 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
@@ -78,7 +78,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
index 53ce9fc3add0bb04ad3209b22c116e41e7f13093..e5d0a0280dd302297f7a22269e5ce7bea7dace4c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
@@ -101,7 +101,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
index 03b15f9c862c59b38a55eaa33eb056710ff516c6..2b8ed53573594fcd6598c5a65d60202730202766 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
@@ -98,7 +98,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
index 03b15f9c862c59b38a55eaa33eb056710ff516c6..2b8ed53573594fcd6598c5a65d60202730202766 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
@@ -98,7 +98,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
index 97898f346f9ff2fe0826f7c78a7b5e2325d664ff..c51118701e805a1c18bcd9476e170f7892ebcecf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
@@ -113,7 +113,7 @@ extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
index bc7a9170e298896d213109dabb696cb723ef22b5..a355b7d0367df861a895b9cd3a16991bbeb62e09 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
@@ -108,7 +108,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_r(__mpz_struct * /*[1]*
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
index de414ac3045e2727df12b26b3cad26346c5c5d2e..5358205e357ff3f89bfb4315bff7befe850b2d52 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 af979f21b344db5d5cd318119a04b6ec5c1c461e..3b4567d368a0a4fda0f1fad9a100367f0f587ba8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
@@ -98,7 +98,7 @@ extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
index 3dc445f2d177ba6fe95ee69e22490df538513c9f..2828fd2c7d889ad7527e843e540f05f075801d07 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 ef5acd7d55fefc8230e4299c9d43fb1cbc3e8f33..a37818a8a038ea38dc4d1b7e857bfab3fbfae5da 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
index 16d7ced41ac37da8405b3cbf1d1c9299b681ca19..fb650ced87168fa3d858b1d07968e01649037218 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 5ccb318714b6fa3cb0d27345e822f3f4776db55c..4a7daa2481d84112c0cb721981aff123a7fc59a1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
index 89bd9045ef4e175df909978a8c3e0526d1c5afbb..f1cfe20bdc8ca293a7258c3eedbb01070197e54e 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 89bd9045ef4e175df909978a8c3e0526d1c5afbb..f1cfe20bdc8ca293a7258c3eedbb01070197e54e 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 0d46e1f187d1cfeebf079af1068b1aae8052f8ec..d4e78da1104b305ba8d476ac8033f6f48feb299b 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 6f5faa3091bb02cb1a94a2e6dd8ba4140925dc84..82431c97c2cc2af77f7ad95e03975d9782d847cf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
@@ -61,7 +61,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
index dd216a8bc8dcc1b3341fcf0166aabe1a873a1f15..da9e0f50eb99da6b2583ef2517dc11e0ec773d73 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
@@ -72,7 +72,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
index 066c297a322d95ae895cf9db57c62c5e0fc37b23..97ed477275ece4052084373ce99edc08452e4959 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
@@ -130,7 +130,7 @@ extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
index 908867a4633686a97eca5e028daf39e799ad669c..ff3b77ce0e1bdbef73c382205ff83c582c051b86 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
@@ -83,7 +83,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
index 908867a4633686a97eca5e028daf39e799ad669c..ff3b77ce0e1bdbef73c382205ff83c582c051b86 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
@@ -83,7 +83,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
index 8779cbdeabdb30d88396e02d521f67a75371d43b..a808779ab9edd09d15e151e46c605850cf64a8bf 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 7eba41bee98b9691c0772c621bf52ac8c4df5d6e..da34c241b4ad6226ddfcd475021c3f14f76a3c11 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
@@ -113,7 +113,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_r(__mpz_struct * /*[1]*
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
index cc0712eb47748ccb87924209327eb9fe6d566384..3feb1351016baa3263efd1bc793f7fcc991b49eb 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 40ddcec7016e605443a0431c71466a9d9eb1c189..83e2e2cb511e899c3598639f9ba754b937db05d1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
@@ -80,7 +80,7 @@ extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
index 403b4169c17c2a3f9477105a60fc523956d4ff16..eef7334720d7a787d23de16b737ab45fbe9f9a99 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 6930a9c474117bfbafdcf40a358677295068bc4a..cad3806eb156f1328250d44d8787812071841267 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
index 758997853d3fa797090a6bc224280838b860190f..bfb8ca6d0bb11a79f5f0ecbbca70170bb64accb6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
@@ -87,7 +87,7 @@ extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
index 758997853d3fa797090a6bc224280838b860190f..bfb8ca6d0bb11a79f5f0ecbbca70170bb64accb6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
@@ -87,7 +87,7 @@ extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
index e0bcf266375e61b45e0761d8057e620fece9d0cc..24887d7d7f9bc3dcef0429dd86f3d12a6ed2a2f9 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 63a290eedce70a643c78c3c7477170ca0ec263da..981fd6bc7640f868f703f2bfd7977d21e789533f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
@@ -75,7 +75,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
index 16f0e40ddaa2cb38d46d33e745e1151000cca6ab..7c58c054a3bb4b793bbb19748d55a0cdee1d1744 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 16f0e40ddaa2cb38d46d33e745e1151000cca6ab..7c58c054a3bb4b793bbb19748d55a0cdee1d1744 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 b09462117d47200e66d5f4b9bdc3d4bf246d78fb..a66c8e145198145c928e8f5c2cc1d2bb2ffb38a9 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 7d7245dcaef0aa43deb5a2b12df07e0a9139b7a4..fc9a529ebc99189ece43c22adbe88ef352d41efa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
@@ -68,7 +68,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
/*@ ghost extern int __e_acsl_internal_heap; */
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index d43659faf504d642b77700977e78bdccd06b3fa8..2bdff3991572445376fb4341be4072e5171da21f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -120,7 +120,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index d43659faf504d642b77700977e78bdccd06b3fa8..2bdff3991572445376fb4341be4072e5171da21f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
@@ -120,7 +120,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
index 8187bd9b1d2f9fbd39fecd5029acce36e6255f0f..5444decbe4be3275a5c09466d5ab039163cef462 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
@@ -124,7 +124,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
index 563cb72ec73a08b103263ae86e737db215e36c01..0d609bc8857571784081b1017b619aabbc87cb86 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
@@ -138,7 +138,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index dc069fd655e5152e874bf9b44cd7f002dfa88959..133d0d4c7c4f625adfd51b5656473cb6ae330a19 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -79,7 +79,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
index dc069fd655e5152e874bf9b44cd7f002dfa88959..133d0d4c7c4f625adfd51b5656473cb6ae330a19 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
@@ -79,7 +79,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@
predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
index 94f13e139d47763a7d18af90405ad462d1e168c5..84460b287a8f0247740b3c1551f329f6d15f5b64 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
@@ -108,7 +108,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
index 5db867a9f768aec03c2a9d22a31c86ac8da34cf1..95005ee9287d652740889d461dd71ba2fd230f84 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
@@ -131,7 +131,7 @@ extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
/*@ assigns __fc_heap_status, \result;
assigns __fc_heap_status \from size, __fc_heap_status;
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 5af377d2bf8484231e8e6de63643b8087b27b2e7..a7dd86cb6c08b2b3a47e05c2518f47ab434b6dae 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -472,13 +472,14 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
| ret :: l ->
let loc = Stmt.loc stmt in
let delete_stmts =
- Globals.Vars.fold_in_file_order
- (fun vi _ acc ->
- if Pre_analysis.must_model_vi vi then
- let vi = Cil.get_varinfo self#behavior vi in
- Misc.mk_delete_stmt vi :: acc
+ Varinfo.Hashtbl.fold_sorted
+ (fun old_vi _ acc ->
+ if Pre_analysis.must_model_vi old_vi then
+ let new_vi = Cil.get_varinfo self#behavior old_vi in
+ Misc.mk_delete_stmt new_vi :: acc
else
acc)
+ global_vars
[ Misc.mk_call ~loc "__e_acsl_memory_clean" []; ret ]
in
b.bstmts <- List.rev l @ delete_stmts