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 dba81f3c6d31e6b024a975c5e8defc6736abd3f0..305100476ad94877e70917a4f623838fa05048a3 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
@@ -22,9 +22,9 @@ typedef unsigned int size_t;
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 dba81f3c6d31e6b024a975c5e8defc6736abd3f0..305100476ad94877e70917a4f623838fa05048a3 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
@@ -22,9 +22,9 @@ typedef unsigned int size_t;
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 52c77c6446b44a0c646e3cda55d270f3441eb772..d09d7c3c54b3320c48c8b81ab501135f0d75c5a8 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 52c77c6446b44a0c646e3cda55d270f3441eb772..d09d7c3c54b3320c48c8b81ab501135f0d75c5a8 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
index 2f7e31a5459289093b4e2640a005421f35a50250..f38509d6a426c6745fbb399cddb97187e73cfe60 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
index 2f7e31a5459289093b4e2640a005421f35a50250..f38509d6a426c6745fbb399cddb97187e73cfe60 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 8dbf4057d2dd64420a2257deb51c7e6889c8474f..8a8625abd82ae9f3c5af14f0a755a40cda4323a3 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 761c1f2cb402c3a0d351b4c2a525b6877286b74f..6c3acc4d9ec5cae1fff3a90ba0c375f80379763b 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 12e1e5ea0e62ff4fe0e45f869fd30ceee0a8bc9e..1615b6ef37741237930590c4da83cfa0f1774a4a 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 ac2df812f0e30164041625aef91efd46b7dfe43d..0ac93b33fe09356f110703f3d698ff373861dfaa 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 a64f6de670d780b2a9d64bd5c3da5e20d83b0f4f..60038ef2900abd6855980509323119cbf850e9c1 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 69882bd06dc66ad4b6d0e5eadf805ee936712cf3..e1d38eb53a07215124f9b9ff1025af5cd7038f18 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 e7b3047cb044ddbb6fe267e3327835807c3bd329..603392116eb8f6ca83d400644a8175abfbe4f473 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
@@ -34,9 +34,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = 32767UL;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 e7b3047cb044ddbb6fe267e3327835807c3bd329..603392116eb8f6ca83d400644a8175abfbe4f473 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
@@ -34,9 +34,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = 32767UL;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 49ba96ec713e3ea4a68c00a7c88f4b981ca90f03..6db200ab0af3a8af4caa31ea14badd54b116f284 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 5a1adaa340953d768a5477f64521366e1517c445..ba08554994b2e234c87467e50c2d897c56f65f01 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 db57354983aa0b912bc56473efde6e90cca53610..2a8d7cab33d18c4c4e28cc3ded8a8fe441607787 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 52dc9e946e4dffecb1ce1c1b53565338a758de16..800ef64be2b889387e090ff5dff2d49eef7346f3 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 580e2170a31e4ef1048f84f495ca008f6a422f8a..e89a9bbab037e5deda963fa93ebc1e0b427ae428 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
@@ -19,9 +19,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 727dbcac769fd69ac26a8311ab01a3557d1aa539..ed44677b2fd98bb8ba9af6e9a786d4fd8c721677 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
@@ -19,9 +19,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 7a2cb429cb64485d4c019aece867b156f3d188f2..9db9f987df08da1ece8008626e6108aeb0805430 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 f19443e1e4e0fc6b6724ad2edece10a69ffbbd22..05478205fdb1a9ee38407978a28a35c425926cc4 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 5d7ef9cd6cd3411c39b54adc239c9d625fc35d68..828a0e2f6c7bae23082f9fb380c0feee9e3e0cca 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
@@ -50,9 +50,9 @@ typedef struct __fc_FILE FILE;
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 5d7ef9cd6cd3411c39b54adc239c9d625fc35d68..828a0e2f6c7bae23082f9fb380c0feee9e3e0cca 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
@@ -50,9 +50,9 @@ typedef struct __fc_FILE FILE;
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 ecd647e68b5c98ece7a780604f600d81e9eeb907..21f61f904cc4a03efba674677a5e119051d4ec29 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
@@ -24,9 +24,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 37d0b6d845728ef138b4de57776fcdf079350d4d..3c686df28e312acc8eaa56e4cc0b22aea02d0897 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
@@ -24,9 +24,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
index 1af8751dd51f9760cb8039b01141539f42961079..ce1a2038dc845eba24da525c20adb6625d02331b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
index b0fc6e014d1298110aa720dbd57bb8eb0410f290..ef98386277da8542f8df7e3e143ecf4399d7e671 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
index fcc8fdea9b571a4be297544a1115ba4f0ac63068..a1f40a83d098cc9b6bca93f24f1b68860f44d001 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
@@ -21,9 +21,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
index 28cafc31d717c3a63eed1d522cfb7ef3cc0c3f9e..b4d554830bac8e1438d6528a2b537aaa30b58cca 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
index 28cafc31d717c3a63eed1d522cfb7ef3cc0c3f9e..b4d554830bac8e1438d6528a2b537aaa30b58cca 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
index eea9d82ef209429b3bc8df8d299628b1ad8d1fb0..cf51d7d52488f18bd6c9bcdb3bb8cf07aa9a7f8f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
index eea9d82ef209429b3bc8df8d299628b1ad8d1fb0..cf51d7d52488f18bd6c9bcdb3bb8cf07aa9a7f8f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 ea3e50ec1f005b0b215c4c3a0f76f1c3f555e724..6f92774bd2d62b405cfd02d1eae48cfd62c9254a 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 2f1c08454324d94b6a3f1d827c854f29588260cb..7ec45739b59eefead54c26bfa2e504349db83a11 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 4e4625a02394b4aef0fc2dbd27577a1fe0a11282..6c7cb59e21ec4f424fb612117cdce3ca1666a356 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 9eb4b43ba1ca7628e12243d3ddbf3277589298d5..b8e9076ac30ba366f5f678c1b65a9ca2aaa2c84c 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 1fd7d396a109d5e04ef064805ad0f1e10825526d..3ed665699cc1dd29a757b9d6d73642609c6ea16e 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 1fd7d396a109d5e04ef064805ad0f1e10825526d..3ed665699cc1dd29a757b9d6d73642609c6ea16e 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 b8c5132e0a8a1c358834fb2c0d805191d7201d67..253d3d4adcaf597e650b92243e7f40b7683577e4 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 bcbe97f2f00c3c64ba361a5ead6669c601acef13..b91ecab66e449878ad5a6ec41e887736dcfbfe64 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 764d3802ca85918046da77820e1c9fb73c802af8..f91e395aa1fdffea54cfa859160c3635fb3b7816 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 818ce62654dcf88fdc6e93621abded71c5039d33..7e4312e3b45eb45f9a9755862c73871d570f1a8a 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
index fb34f5a8339c0ffdd15f654599332527eb96001f..2ad63c456df558dd0fd5d12c6f2b5f6e3eff2e03 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c
index fb34f5a8339c0ffdd15f654599332527eb96001f..2ad63c456df558dd0fd5d12c6f2b5f6e3eff2e03 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 1a264fd98cb70f4f331d0f88f5d9d9b52c1f937e..4e4655bb33ab84a12ae4ca6853e2bd4320959ab8 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 6090e411fa3386be496546f27360c2c9ee778e53..357c3ba8ae9d05b68d336aedbb8a53c6dc334b39 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 b0a2b92651dc6b174239f9f70c2e843f38152b95..ca95f8bc50fde57d7c30b0c2e4b0853b61730c57 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 e8ec0e172adf088dcede15fbc3a66c708e6bae7a..4c27d12cf492b3766d436486f31f45eb80586eda 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 c32c7597ebde261bc37f76e6a87265e2b6ee21cd..f54bb89c336436b839eff2bb5f279a3f4242fea9 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 cab66fd38db18f12a14e50426ccdb509e941e445..e0769e4505e7a90b9e40eb30eace8d8228ebe5a9 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 4796453831b4bf4db97d8430982cd83a429e5357..cf4ce4f86ef08b51b345a17365114ffc69de40af 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 05e53ad7a8889abaffa0418022aece5b09518421..1112e66a66547f88590707f403d8dd7978c16c06 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 26138bff93637067183a3721824424010a9cffbd..313b731f630932758b161cea1817f46311a3471f 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 40a119bcad3ae7b920e508666a92da3f88ac275b..3877084d38efa9d2a3308ed54f0e5b9302700cf5 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 6d0b1e9d48c392c949b7b676ca5dfd10a7f9a17d..ce2452867a9278c39c8205b6d358314e55003c1b 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 d508166dd141edde5be93ab955fa8de8e56ec875..6dbaf12b8f1a5a490e88ee166102d552a310def7 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 194a9c901c0188670eeff6c39a0d2c12fe60d01a..780abf1d50ccca31ce2102876b6f080e0bf3cd0c 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
@@ -22,9 +22,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 194a9c901c0188670eeff6c39a0d2c12fe60d01a..780abf1d50ccca31ce2102876b6f080e0bf3cd0c 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
@@ -22,9 +22,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
index d21977c4a78798590be5ea94b97ab0609bba7d8b..1ec68a1de687fde8e23a9e64cd18671e48625333 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
index cd99b29cdd1c0dcab88b142bd356ed6c0a4951ef..268ad6c1bafcc1834fcfdda0cc4a50a6c3b2aebf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
index 81bb83295524bd3c7c25dea639041b4a2ad3a493..0c2cf126e6e51f9b1003ab72fa5cb44dc8fd9b7e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
index b7d6f87b2a0b777a7fb7e4d6c2a4dc8763a8abe2..8a78fcd3c388a091e2f5f4718381134d55ead504 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
index 699eb92ac7c99a67f4577792835016ad811219bf..b8a8828aa6eb968b528230e09d3ff9ad9f165e2e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
@@ -19,9 +19,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
index 3a7ab9a029bbfa5a120889c0cd2bb2189f4bd0d8..359147001c45c626ac1fdcf5aeceb43da5c8b67f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
@@ -19,9 +19,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 29f33c58a5c1ebfb2b5c6dc66850c271b8d53b2c..d12f78a04b9ed97f3e804268554215d22a6be4f6 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 014a582591cb37944a4ea124d8b0b96de38fe4dc..e3f8fbe0b6c47c8210cbae9bbebe0025c1b6ed8a 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 1ad91c4c4e620c6240f5fb9daf5ae033214ffaf8..80dce51c3a6d7d6d9ea5a71c1f14e6f16694ec17 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 d35adbe8f2353ceade47e9a95b872d5dff356188..72532dc387cae31cf3cfcddb24db202e60d57a81 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 66a1651f0dbd75b9c340e2ead6c8c60782c54788..216bb084e2be5bc1ba41f24c7166da6eeef0aa90 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 66a1651f0dbd75b9c340e2ead6c8c60782c54788..216bb084e2be5bc1ba41f24c7166da6eeef0aa90 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 bf043e2dcf50809afad93157c033732b363d3d5e..4c13b1477b9f315fd70bb977d75f4ec830456e90 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
@@ -22,9 +22,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 00614bc4ff76d9acb8a4be97ed75df5a41922612..d9cc1e203307d327f4345ad90eca85519e185c53 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
@@ -22,9 +22,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 f06b99fbaa0a6fbea345c1a23ec27deefa39f62e..878b9a3407a9d9e70e2a7f9d99b728e32d48a69c 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 c800a42f9b525d2b7279a0420b6fb9dd2010cd3f..1e3430db81471e24729d131e2f3d05ad398f9365 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 97fc8320410c6e601512b58c73b737c680f01bd2..a79f65348bfe2ed77ffc77a5159a946ef15b90eb 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 97fc8320410c6e601512b58c73b737c680f01bd2..a79f65348bfe2ed77ffc77a5159a946ef15b90eb 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 a8639591951e239fae5bfe39b03ce81910bf5464..b882f493333ad5ecd74ed506f963ee0935c3d85f 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 68735a67eb6e5f8ffacb39312ac10faf7219f453..4adb08a08f2aa032322c282efc2ff4670d6ae5de 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 b0ddb3a41129aa254ea2fbb8060b7c14b653b808..2792dcf8aaf932c3cfa90a0a1f5890efee3c87cb 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 a022ac08c5e198e54987392eb3445fcabc454033..90cdc6aeae07ca3a4f768617ea199aa65e09216b 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 7f848e4a0fceacbe1368208e6c266dbd61b74f4e..77e7a73136decfc978c21c240a4121babf139640 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 46af40a2731d915596fa1cdd3170cb95996f1a74..f6c96b33c089c8383945c0a474486b97d4cfc767 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
index 7c79595298b17981123c7ed784264edd4e1a3713..7531b683c53aa238c55c5c97d130967d91c6eea7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
@@ -58,9 +58,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
index 7c79595298b17981123c7ed784264edd4e1a3713..7531b683c53aa238c55c5c97d130967d91c6eea7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
@@ -58,9 +58,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 ab74b73951bc2a30b0b94b528b9e44625479fd0c..b7927180ad1a31bd753b6c269ae003ad728e57dd 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 f037df664b6507d1a911998c4cd7ba2de27aac70..e0cdb70d6eac1a6c0f58bd15b31fb553557d7da2 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 b14f5695b20a74ed6e0589be9fa2938afb711f50..720929a8f71b9186e8683973f5aee01ddd39c7be 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 b14f5695b20a74ed6e0589be9fa2938afb711f50..720929a8f71b9186e8683973f5aee01ddd39c7be 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 600c610aac752546811aa85f25b43e075ad3febb..8149e2edc106d318433b5d835609eabb12d54d48 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
@@ -19,9 +19,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 841c1c3743684ad669453378d3785ece4fe15126..e69481cbedece490202df66be6e3a16193d1b822 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
@@ -19,9 +19,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 7e1f35cc0a739e560e6742d6c1db6af48f341de2..93df89f36dffc5b8ac8d92d5ab75aa890ded93f6 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 7e1f35cc0a739e560e6742d6c1db6af48f341de2..93df89f36dffc5b8ac8d92d5ab75aa890ded93f6 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 b8a2d83d8d02137cd73bc8d1a63a8e55cc286bae..ddde059e9211f2441731373cd29f2f330bdc3acd 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 f56c24eed56b7a70a498047adcccf153db5f6368..9702b5b68b4781b10bb4e91893c86ae13f5c6de5 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 ef0708553790bec0ea91f65918a2b8b7ab48d3ce..5964f59070216d8c0b715aeb6191c42f2acc0006 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
@@ -22,9 +22,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 ef0708553790bec0ea91f65918a2b8b7ab48d3ce..5964f59070216d8c0b715aeb6191c42f2acc0006 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
@@ -22,9 +22,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 ee38254834023ddb11f5c4cc292fe3ce977a83bf..3f50777239b1cf27f792555407328b2780f3c82c 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {
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 8ed2ae4c95eafa7e1f59eb890c27bc8112f0f191..e4f0303aa767b4e8e4cfe004f35be81299bb93c9 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
@@ -18,9 +18,9 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__));
+int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
 axiomatic dynamic_allocation {