From 2490ce6d168b2528fcd581987ee28f14be257dc6 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 7 May 2013 12:43:33 +0000
Subject: [PATCH] [E-ACSL] fixed issue with extern ghost variable (definitively
(?) fixed issue #1392
---
.../e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_function_contract.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_function_contract2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_integer_constant.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_integer_constant2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_nested_code_annot.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_other_constants2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_valid_in_contract.c | 2 +-
.../tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c | 2 +-
src/plugins/e-acsl/visit.ml | 5 ++++-
81 files changed, 84 insertions(+), 81 deletions(-)
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 244db78f6a4..e2ba13dd239 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 244db78f6a4..e2ba13dd239 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 0b7777a5414..831b7db83a0 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 0b7777a5414..831b7db83a0 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 6470694a4c0..32c909ea768 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 e0d7ca85651..7951ab45651 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 eee3c5a3145..2cb5a1becaa 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 4cc5defb1af..733f2aed30c 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 acbb22b8db2..ce28c3879ae 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 ef1d71ea6fb..b0106cd5bd4 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 e560fab4069..2bc325e5acc 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 e560fab4069..2bc325e5acc 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 52382e769de..596d7fb7326 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 f4cf0b14916..715d4526919 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 8c6b3285703..9023f38861c 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 8d62cc117b3..e2be4ab6b61 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 1b897ce77a0..b51d0c4f89e 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 2a59198cae7..6039cd5eb13 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 dd75426e271..87f1dae575b 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 a63bb3b6309..4e63ae9b850 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 d32886bffd7..0fb8963aa8e 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 d32886bffd7..0fb8963aa8e 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 6b1383de20e..79fb985f417 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 41010eccee5..266585cfac0 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 a65d6a97bed..9904c081be8 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 51021dead63..c13552cebb9 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 5c70350399c..10a9ae302de 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 4d25d0bc053..2dd28772e46 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 9c6c389c03d..e760f254d26 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 9c6c389c03d..e760f254d26 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 cb854fd6d81..1fc792e0c37 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 a0c5f1a2148..222e697f71e 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 9485978f1df..33616d44642 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 8e9fd8bc890..edde55abd0e 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 78871f79f32..7a057561eb2 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 a48f33cde50..2df187c7929 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 eac173765f5..51a00d96d81 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 e0ff8ad93c3..ab0778af061 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 fcf7e8db56a..ccac293a0dc 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 fabf71ed539..a00b658612e 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 d9c5f42a2c2..f52c93260c1 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 1d677e65b0f..fce174c34d5 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 7d84da1d848..1d8f35b075e 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 a7a500dfeae..9b70bcfdd6c 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 670a2b1bcf7..802ff2fbc31 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 d3685f1e927..5acab454130 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 d861adcd1f8..3e5483cb4c3 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 d861adcd1f8..3e5483cb4c3 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 17ef97e00fa..dc3e01f7404 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 e68ac2e4c62..edad0b3115f 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 0a62a47992c..fec032c3839 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 7919b6cfc4b..fc3adb9948c 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 ff3c44d096c..dcf4e8ae8ac 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 ff3c44d096c..dcf4e8ae8ac 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 8155dc69c1f..e9fbeb377cc 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 8f7baba029b..0e05c2ad2e7 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 14d0032ad8f..176208d82ad 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 3049d4771b1..c97a4938d67 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 14648a95ec4..62ca52a6be5 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 14648a95ec4..62ca52a6be5 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 2b271fc2fa2..efffa80fa16 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 096d13f3e92..433da33e2ad 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 8e7e6c3975e..395b9ad9031 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 e1e53d35bef..e927b04f98f 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 f8550559d28..c20896ea2a1 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 9978b866275..5ab7bfcda08 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 4cb6a1fc840..e9e6ac009e7 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 87f439da9fb..f5fefb3fd3e 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 9f9127ee517..50ecf913687 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 9f9127ee517..50ecf913687 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 53aa6bddc1f..351227afff0 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 3541cbd70ad..fcdc81e2bb1 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 7280c80ad88..15466f0fab0 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 7280c80ad88..15466f0fab0 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 39bfc7e30e1..198b72cf5f4 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 5c79ab7a567..1e83be551d2 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 1837354a1ca..8f8f9b18457 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 1837354a1ca..8f8f9b18457 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 7c4d9feda33..05bf89ae9bd 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 3756d1802cf..c33187cacbb 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 fafff849b61..929c08ae345 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
--
GitLab