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 244db78f6a444a7ab97f607a5faa975eb6bbe0a4..e2ba13dd239ddaaf7ac934942622bf1eb1802d0c 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
@@ -23,7 +23,7 @@ model __mpz_struct { ℤ n };
*/
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 244db78f6a444a7ab97f607a5faa975eb6bbe0a4..e2ba13dd239ddaaf7ac934942622bf1eb1802d0c 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
@@ -23,7 +23,7 @@ model __mpz_struct { ℤ n };
*/
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 0b7777a5414407e4130ac56c947ba4ff0649c88a..831b7db83a050d3afb64fcacaa26e235afba72c2 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 0b7777a5414407e4130ac56c947ba4ff0649c88a..831b7db83a050d3afb64fcacaa26e235afba72c2 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 6470694a4c0ddbc603eced124b4ec0c2f292d792..32c909ea76865515beb81bdca414d0d655dc5c81 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 e0d7ca856510d03f3b449ce715e1ff6f154f5cbb..7951ab45651169fe71c19049cd1bfbec68ba1eb9 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
@@ -124,7 +124,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 eee3c5a3145c07b2364abc28e3a283658c05048f..2cb5a1becaa512185b09b1796753c69a8e8dc548 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 4cc5defb1af2b92187a24965aae0f521a80e5dd6..733f2aed30c37729b0c648286b53c1b210599ebf 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
@@ -40,7 +40,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 acbb22b8db2bd293b060def705c81576a49fbea0..ce28c3879ae3b373163092696b089f8b4f0a6adb 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 ef1d71ea6fbb5ce118364f7df6b1adc5fd56ed3b..b0106cd5bd48a6ceda613887ec5f68c35d7f9206 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
@@ -67,7 +67,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 e560fab40692bc4d41e3387c69bef65091f67689..2bc325e5acc0f02829bd98f31b9062295da00d0b 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
@@ -36,7 +36,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = 32767UL;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 e560fab40692bc4d41e3387c69bef65091f67689..2bc325e5acc0f02829bd98f31b9062295da00d0b 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
@@ -36,7 +36,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = 32767UL;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 52382e769de3fe104c4fc4f14c56e563bef7e492..596d7fb7326be30e7647bb9a9ff85c159a546dd1 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 f4cf0b14916eb858ae21f3e83270cc23df2ca758..715d4526919af4e139f1e9589b9423665f08b146 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
@@ -71,7 +71,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 8c6b3285703e3f320761d84c02677ae68de6145d..9023f38861c3cfd1c015699e0b76b5e2e7539056 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 8d62cc117b375b723a2d0e8a8c4961dac04bb5a5..e2be4ab6b6134f2b977d2f575c79bc43b39e2eeb 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
@@ -79,7 +79,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 1b897ce77a068c6cbdb57fcc656b48c4796c38dc..b51d0c4f89e9511f1018454f55563a4266c33cd0 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
@@ -21,7 +21,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 2a59198cae7e8f0e3648fc727955217af7fd7070..6039cd5eb1344fc422600526710f6f4d21c68577 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
@@ -68,7 +68,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 dd75426e2710d1c80972fc4fbf5e138c015e3fee..87f1dae575be7503b9266afb9905a79abc0520ca 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 a63bb3b6309790b40b10d5a0194fcab82cef7b23..4e63ae9b850f741187cf7c3322a6e63465ad8263 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
@@ -79,7 +79,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 d32886bffd7cd1f43be88efa79308a90e78c9ff2..0fb8963aa8e478632ddf7fd77c41e8e1ee5075aa 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
@@ -49,7 +49,7 @@ model __mpz_struct { ℤ n };
*/
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 d32886bffd7cd1f43be88efa79308a90e78c9ff2..0fb8963aa8e478632ddf7fd77c41e8e1ee5075aa 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
@@ -49,7 +49,7 @@ model __mpz_struct { ℤ n };
*/
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 6b1383de20e5c18e4a3b2e6ea647b8234839e958..79fb985f417216880059ee043fc11554ebf739f0 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
@@ -26,7 +26,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 41010eccee50a97cf2ade4e491786553b9c04ce2..266585cfac07de7ea24d3363fdaa039d97cdc39a 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
@@ -77,7 +77,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 a65d6a97bedc877d749a2d6d4931efd51670cfec..9904c081be8cf982bb1d1339ab214db4257e6d72 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 51021dead633d7a636fe5e3cde5c0e9efd31a9fa..c13552cebb9406f8844afd0b1d1affbe0a243c98 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
@@ -65,7 +65,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 5c70350399ca184f9d02397660e0f75bf63efde2..10a9ae302de368279f30a1cdc0df7477f9dd94c8 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 4d25d0bc0532d60298692381de94e5e67a1544cd..2dd28772e462e7e86dc3d9a84e3e3012b70742d0 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
@@ -55,7 +55,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 9c6c389c03d7535220a7f318002557ce8e3b5a27..e760f254d26c5dbd0b10468a1f5eb33f6441dce4 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 9c6c389c03d7535220a7f318002557ce8e3b5a27..e760f254d26c5dbd0b10468a1f5eb33f6441dce4 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 cb854fd6d81250f0298b433e2535186663313405..1fc792e0c37c8f1f047fbc86764aa5919b45c9b3 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 a0c5f1a214811543ea916bdba90a7dc98e0484d4..222e697f71e1994630c6a6844971ad1a87b04f94 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
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 9485978f1dfd10f0cd5b96a0f42d48ae189f66f7..33616d4464247c83656b680e99c2dea2c5a33b91 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 8e9fd8bc890509e766e0dedb384b422af15aa50a..edde55abd0eb8f204019f5f4cf435c17b503c4fe 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
@@ -40,7 +40,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 78871f79f328054d6147d5eb70f3fedc3c8df9b9..7a057561eb271177cecfaf17e1c0a69f1c4609f0 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
@@ -41,7 +41,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 a48f33cde5081d84ff7ae9e10a29909ff47be95c..2df187c7929c93a437ad8e1866d59f0c116d19bb 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
@@ -51,7 +51,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 eac173765f5496d058d894917c5cf3674c1ed888..51a00d96d814bff451a415e7747c493d108b0d95 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 e0ff8ad93c3e46ca37a4be186a4ecf13af5a46d1..ab0778af061bf2ee4ce7ad2a8d7282174dcea9a1 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
@@ -40,7 +40,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 fcf7e8db56a905e9c449f561705cddaf6d5878dc..ccac293a0dc47e6f0bc70afbd98bef75d8a8e02a 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 fabf71ed53911a2f7943aedb8ba8f89538cb1cac..a00b658612eacc8581827bca4f383db0020af7db 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
@@ -40,7 +40,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 d9c5f42a2c2f6474fa58de3c29803bf77358d4f1..f52c93260c1341f94fc5d0ec2a5c86de83ccd4f1 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 1d677e65b0f5d12d4504bf3be4f203ae530330f8..fce174c34d5142622fab78c115d4e1e7d62865ff 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
@@ -67,7 +67,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 7d84da1d84893277efb696346b8d56a8acf841da..1d8f35b075e1222b3fd916ebb56fa1a6b2e47d83 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 a7a500dfeaedc8106ffd7c435bb51a0d3f748ce5..9b70bcfdd6ce2547c6bc487aa30a89f806ceb919 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
@@ -69,7 +69,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 670a2b1bcf78ae7a51a51d6a00c0967ac3604607..802ff2fbc3123a57cd3f60d2dadf9caa9d6c9799 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 d3685f1e927a41f57711da2311ca2b54d20505f0..5acab45413030dcb038ac8a8df7aa959edb6cb17 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
@@ -40,7 +40,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 d861adcd1f81db381fff27d586e4872a235d5882..3e5483cb4c39477492724ab3b23d5ecdbd323031 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
@@ -24,7 +24,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 d861adcd1f81db381fff27d586e4872a235d5882..3e5483cb4c39477492724ab3b23d5ecdbd323031 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
@@ -24,7 +24,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 17ef97e00fa8b99e8d72ac51fd547963a0478246..dc3e01f74048ba51e7569931a159417234846562 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 e68ac2e4c62089b81c4a12530889676dbd2676ea..edad0b3115fe94327cd3817c09fe8460422cc21b 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
@@ -40,7 +40,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 0a62a47992c8e630fd9b85d6a1304a0c09c2f7e0..fec032c38393a1123c3b4be9d5c7076c4ef9339e 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 7919b6cfc4b07be02b759ce7a7babd7d772fef1c..fc3adb9948c4f198b3e83a0a485b2ceb8a20dc80 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
@@ -40,7 +40,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 ff3c44d096cbfe24e68f4b57e7f5d2bb5fb46b2b..dcf4e8ae8ac1ddfd750b9bdb9e59da9c07dc47c0 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 ff3c44d096cbfe24e68f4b57e7f5d2bb5fb46b2b..dcf4e8ae8ac1ddfd750b9bdb9e59da9c07dc47c0 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 8155dc69c1ffd97bc29b86e75a84678e0d4ecfbb..e9fbeb377ccc8f13edcc0bc991c4ba0249bd6c7e 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
@@ -24,7 +24,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 8f7baba029b2d536bf319ecfe6b04d7156e7d78d..0e05c2ad2e78ed5dfa0639adf7c122a0a9add293 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
@@ -44,7 +44,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 14d0032ad8fe4a1d2c4b6cb7510510e29d97eabc..176208d82adc4f988ed76479862336a3fe711d8b 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 3049d4771b1769b92271863760d316767e54e5cc..c97a4938d6777950f172d40a8cfab22d35100ac7 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
@@ -91,7 +91,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 14648a95ec46a915185e1bd4fc65d1819f890536..62ca52a6be56eafebc7d28b098df1d4c008cb98d 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 14648a95ec46a915185e1bd4fc65d1819f890536..62ca52a6be56eafebc7d28b098df1d4c008cb98d 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 2b271fc2fa2adf48645427bfd643d961c5800120..efffa80fa16c04784d1f4ac4c5e358047d0482d0 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 096d13f3e920f8408a57528a3cbda76a48e502d6..433da33e2ada84ae52782e98ab86f80bffd7d0f0 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
@@ -95,7 +95,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 8e7e6c3975ef3731b92dbe0f3e08c055d3a752ca..395b9ad9031405f6d98125e8f94153a3185ced73 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 e1e53d35bef73f5702e4488ad687849718466cf8..e927b04f98f5532459f433cfe89b768a3c1ce265 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
@@ -61,7 +61,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 f8550559d28bd5feca51424a15567bb892c9be51..c20896ea2a1c8dcdb0f543a035e170d366a2a641 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 9978b8662751de29646903bd1be5288b348b89d8..5ab7bfcda082aefa694ec97d7c0aaf51e912b94d 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
@@ -40,7 +40,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 4cb6a1fc840c43eb0503fedfa180acc958111684..e9e6ac009e7ebc1880631519ea95c39da21bba51 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 87f439da9fb0ebbdb60e3378149d23b3ce3e1729..f5fefb3fd3eb62a1698528376135f018f08a0c0c 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
@@ -57,7 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 9f9127ee517df374f8e6dc8d764dba95dc1e1590..50ecf913687bd02d765b2f6f666b6160b877d0b5 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 9f9127ee517df374f8e6dc8d764dba95dc1e1590..50ecf913687bd02d765b2f6f666b6160b877d0b5 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 53aa6bddc1f61d86ab08947bac4da202d087e5e3..351227afff088e6237d029c636e0737c81cc405c 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
@@ -21,7 +21,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 3541cbd70ad7dca89bc82301a714e1759fe55db3..fcdc81e2bb1492a492d76ba319617026fff95007 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
@@ -51,7 +51,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 7280c80ad88ae623ee86cb1818fcd6e02d1cab43..15466f0fab0069cec33e774295e87a682720a50d 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 7280c80ad88ae623ee86cb1818fcd6e02d1cab43..15466f0fab0069cec33e774295e87a682720a50d 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 39bfc7e30e1b573b90baa6948ae335d9f9c17abd..198b72cf5f4b0ca927dbc7841eed3df83209ea8f 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 5c79ab7a56794d4e4751a1357951ec09cbf6a4d3..1e83be551d2072f78ee15bfba28b32a7dc366a5a 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
@@ -40,7 +40,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 1837354a1ca9cdda46c2836b04abdc6d15514e99..8f8f9b184575eba44940065f40d67f499d0f0acb 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
@@ -24,7 +24,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 1837354a1ca9cdda46c2836b04abdc6d15514e99..8f8f9b184575eba44940065f40d67f499d0f0acb 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
@@ -24,7 +24,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 7c4d9feda33f606ed1f721fa26a87bb4ab301a84..05bf89ae9bdefb7e31004c7badf9e5787c9edb70 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
@@ -20,7 +20,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
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 3756d1802cf72398ac90c143f79d678defd0baf3..c33187cacbb60609d0dde69454b5e145dc9f084a 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
@@ -40,7 +40,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
-extern int __fc_heap_status;
+/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index fafff849b61d30319fffc019b6449327b058a70c..929c08ae3454bf2b9305fcba3f54bf343d6b334a 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -284,7 +284,10 @@ you must call function `%s' by yourself"
if vi.vorig_name = Kernel.MainFunction.get ()
&& not (Options.Check.get ())
then main_fct <- Some fundec
- | GVarDecl(_, vi, _) -> vi.vghost <- false
+ | GVarDecl(_, vi, _) ->
+ (* do not convert extern ghost variables, because they can't be linked,
+ see bts #1392 *)
+ if vi.vstorage <> Extern then vi.vghost <- false
| _ ->
()
in