diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index af4b444dc68eeba4a641ca3419b8479564d941de..bba0ff9f0201266a531fc199f1ddb0cf9b04326e 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,7 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2015/04/28] Fix bug when using fopen.
 o  E-ACSL       [2014/12/17] Export a minimal API for other plug-ins.
 -* E-ACSL       [2014/10/27] Add a missing cast when translating an integral
 	        type used in a floating point/real context in an annotation.
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index 6f14f3ff9c81e04ee148e211b600863c6f6407ac..a584ede0c19008a5d4b798b6b4648fcfae237464 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -218,11 +218,12 @@ let change_printer =
       let pp () = object
         inherit (Printer.extensible_printer ()) as super
         method !varinfo fmt vi =
-          if not vi.Cil_types.vghost then
+          if vi.Cil_types.vghost || vi.Cil_types.vstorage <> Cil_types.Extern
+          then
+            super#varinfo fmt vi
+          else
             let s = Str.replace_first r "" vi.Cil_types.vname in
             Format.fprintf fmt "%s" s
-          else
-            super#varinfo fmt vi
       end in
       Printer.change_printer pp
     end
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
index f4cf8ba21c74dd2533c6cb899f740f73630c374b..6c989f972cd533e02fe7e0e4334f946cfc0a5988 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
index f4cf8ba21c74dd2533c6cb899f740f73630c374b..6c989f972cd533e02fe7e0e4334f946cfc0a5988 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
index f4cf8ba21c74dd2533c6cb899f740f73630c374b..6c989f972cd533e02fe7e0e4334f946cfc0a5988 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
index 2a6424a798ceeaacc82c3fee110c0734bd1243ae..ec68e5b94427a8453af3ec577bbf1d2523f73114 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
@@ -8,8 +8,8 @@ tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
index df325fe187bb0020b6fa18e39161af1e1871c68e..6291429ab43848435ab895b87db17f8fd383b214 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
@@ -8,8 +8,8 @@ tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
index 2a6424a798ceeaacc82c3fee110c0734bd1243ae..ec68e5b94427a8453af3ec577bbf1d2523f73114 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
@@ -8,8 +8,8 @@ tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
index 36fc1092d18368c622a6f08793670231c7a92de4..77eafde3d46c7f39fded2b11bc8d66fb33437c99 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
index c797620543782ca8438712053e9743f34fbbbd4f..9d10a4d5f852636ce9beafcdaf0c3449ed604ec7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
index 36fc1092d18368c622a6f08793670231c7a92de4..77eafde3d46c7f39fded2b11bc8d66fb33437c99 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
index 7583cbd29fde586a13012f6a653d05780fb3c8e1..ec79b9e70c9f6b090b0ef42b676bb35eb3bc6414 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
index 0a2e472a6f02b50dc7c78ddda66a2976b788310f..7b216576b832623406d9095114d1fb4affb822b6 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
index 7583cbd29fde586a13012f6a653d05780fb3c8e1..ec79b9e70c9f6b090b0ef42b676bb35eb3bc6414 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
index c98c0cb1cddef9e7b2a720bc1bddfc602e613f5c..617549275c19e82c32f93f4f0b6dcec43adcb14c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
index 59bc686a665398a1c9675aaee0c0986524c0e280..6cff74587032dd7b35045111aab68dcf9374058d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
index c98c0cb1cddef9e7b2a720bc1bddfc602e613f5c..617549275c19e82c32f93f4f0b6dcec43adcb14c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
index 1b7e2835fd507fc263bd5ee3d24808d9f38adbe9..e8aef1cfbc24fb5af26b9f9ba7a71658d9b5d475 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
@@ -4,15 +4,15 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
   stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
-  fopen[0..511] ∈ {0}
-  _p__fc_fopen ∈ {{ &fopen[0] }}
+  __fc_fopen[0..511] ∈ {0}
+  _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
   S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
                [--..--]
                [0].[bits 80 to 95] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
index 1b7e2835fd507fc263bd5ee3d24808d9f38adbe9..e8aef1cfbc24fb5af26b9f9ba7a71658d9b5d475 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
@@ -4,15 +4,15 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
   stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
-  fopen[0..511] ∈ {0}
-  _p__fc_fopen ∈ {{ &fopen[0] }}
+  __fc_fopen[0..511] ∈ {0}
+  _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
   S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
                [--..--]
                [0].[bits 80 to 95] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
index 1b7e2835fd507fc263bd5ee3d24808d9f38adbe9..e8aef1cfbc24fb5af26b9f9ba7a71658d9b5d475 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
@@ -4,15 +4,15 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
   stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
-  fopen[0..511] ∈ {0}
-  _p__fc_fopen ∈ {{ &fopen[0] }}
+  __fc_fopen[0..511] ∈ {0}
+  _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
   S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
                [--..--]
                [0].[bits 80 to 95] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
index b07e6a38955df67553b624f292d51ec7e7614a8e..03deca8538462c23d094a70ef4a5468661841577 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
@@ -19,8 +19,8 @@ FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
index 4d1df873684a7ad1d905e77eecb6ce258c75c0fe..ca19d80fd5e1d2cc8f6702a91db8ee236cfd2dd3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
@@ -27,8 +27,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
index 45341f00fdce9f3ff60dfdfda2f7a1eaff2a82c4..98e36f797bf76c4368c6ed1fed39c0bfcf247f89 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
@@ -19,8 +19,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
index aa1818323b885df4bef5089b233f1d6ee3323ecc..615a1182b1808b5ab22594d8869d317a555ec50c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
index c71bbdb36d409eb10dcd9effa81057c73e0d3200..ca69d07a0e98b05b362eda09c8298067a242d337 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
index aa1818323b885df4bef5089b233f1d6ee3323ecc..615a1182b1808b5ab22594d8869d317a555ec50c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
index 282bf108a6571145fd47e12a50b5b6f3908414dc..36ad7b7e87f2d5d621b502a5c97588c6ad2e5dcd 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
index 282bf108a6571145fd47e12a50b5b6f3908414dc..36ad7b7e87f2d5d621b502a5c97588c6ad2e5dcd 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
index 282bf108a6571145fd47e12a50b5b6f3908414dc..36ad7b7e87f2d5d621b502a5c97588c6ad2e5dcd 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
index 91778b7edbeff4e3bc5fb224e877922d4069b8ff..eb2f883c0869d46c4a4b83af223996c299bf1249 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
index 91778b7edbeff4e3bc5fb224e877922d4069b8ff..eb2f883c0869d46c4a4b83af223996c299bf1249 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
index 91778b7edbeff4e3bc5fb224e877922d4069b8ff..eb2f883c0869d46c4a4b83af223996c299bf1249 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
index 603392116eb8f6ca83d400644a8175abfbe4f473..b2f7f38d1805dfa9a01003c60bec70fd9a9259f5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
@@ -34,8 +34,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = 32767UL;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = 32767UL;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c
index 603392116eb8f6ca83d400644a8175abfbe4f473..b2f7f38d1805dfa9a01003c60bec70fd9a9259f5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c
@@ -34,8 +34,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = 32767UL;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = 32767UL;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index 6db200ab0af3a8af4caa31ea14badd54b116f284..bf2eb65234bd4cf6a74e74b410097516d5ddcc27 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -18,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c
index ba08554994b2e234c87467e50c2d897c56f65f01..b0fc85c485edb633748505648101eecec9c3b163 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c
@@ -18,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index 2a8d7cab33d18c4c4e28cc3ded8a8fe441607787..f1e6def71d2d3e7f6ce2dc22c9b6be41aeb023ac 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -18,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c
index 800ef64be2b889387e090ff5dff2d49eef7346f3..aab5a6b122816b329918cab015120a46b869dc0f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c
@@ -18,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index e89a9bbab037e5deda963fa93ebc1e0b427ae428..a5bf59395c9f283c9de2e158dd06991205359b47 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -19,8 +19,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c
index ed44677b2fd98bb8ba9af6e9a786d4fd8c721677..c5e1dc20355e66da9357905a35084b5bab8597be 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c
@@ -19,8 +19,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index 9db9f987df08da1ece8008626e6108aeb0805430..2686494f29706f019c72c8fb7946f09071527315 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -18,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
index 05478205fdb1a9ee38407978a28a35c425926cc4..ff382f5a14f89af73feda08538c1729a982c7ab5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
@@ -18,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
index 828a0e2f6c7bae23082f9fb380c0feee9e3e0cca..9de11fd683b8376bc597fba726142e190435fbdc 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
@@ -50,8 +50,8 @@ typedef struct __fc_FILE FILE;
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
@@ -84,8 +84,8 @@ predicate diffSize{L1, L2}(ℤ i) =
  */
 extern FILE *stdout;
 
-FILE fopen[512];
-FILE const *_p__fc_fopen = (FILE const *)(fopen);
+FILE __fc_fopen[512];
+FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
 /*@ assigns *__fc_stdout;
     assigns *__fc_stdout \from *(format+(..)); */
 extern int printf(char const *format , ...);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
index 828a0e2f6c7bae23082f9fb380c0feee9e3e0cca..9de11fd683b8376bc597fba726142e190435fbdc 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
@@ -50,8 +50,8 @@ typedef struct __fc_FILE FILE;
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
@@ -84,8 +84,8 @@ predicate diffSize{L1, L2}(ℤ i) =
  */
 extern FILE *stdout;
 
-FILE fopen[512];
-FILE const *_p__fc_fopen = (FILE const *)(fopen);
+FILE __fc_fopen[512];
+FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
 /*@ assigns *__fc_stdout;
     assigns *__fc_stdout \from *(format+(..)); */
 extern int printf(char const *format , ...);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
index 21f61f904cc4a03efba674677a5e119051d4ec29..1b1a391506d5596cc35477a5cb9de301c250ea98 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
@@ -24,8 +24,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
index 3c686df28e312acc8eaa56e4cc0b22aea02d0897..84b12d496e0a8cfe716211c0b95df80c4427ee8d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
@@ -24,8 +24,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
index 291c1d24a8272a564dd7f3d43866773611073709..de9f0a6c8650efc82f34727701c81f9418787def 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -18,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c
index 5bfa785f3bf44761c346e8bec1dcc3926ae61453..3be5246cfb3f3f6e7d3d20a7debc1a17dc60abb3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c
@@ -18,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
index a1f40a83d098cc9b6bca93f24f1b68860f44d001..487a65e7f23cd3ef46b18d985612ff10757f8ba3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
@@ -21,8 +21,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
index b4d554830bac8e1438d6528a2b537aaa30b58cca..bfd83983a86a46b25cb49bae40eb908e42a9d0cb 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -18,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c
index b4d554830bac8e1438d6528a2b537aaa30b58cca..bfd83983a86a46b25cb49bae40eb908e42a9d0cb 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c
@@ -18,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
index 70b672564a3d8183673fa7a02045731ecb228b64..4bcd25d2c380870a245aad302ba475907b30314c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
index 70b672564a3d8183673fa7a02045731ecb228b64..4bcd25d2c380870a245aad302ba475907b30314c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle
index fddcb52a99b8c2570fed7d1971b5fafd29a92fec..e16771bba8f47172248978e9528949591c473921 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.res.oracle
index fddcb52a99b8c2570fed7d1971b5fafd29a92fec..e16771bba8f47172248978e9528949591c473921 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
index c0f02d51b0fc6dc306e6fe093ea83ac271550fbc..1f09cb63b6eb0eb44fdf71cc73742301516be8ed 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index 11e9eec074fc9eb2c52caf358b75a493352e2c41..9e13e05e51dd2fa26998055d289d6af06e884bdf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
index 654ef2d58ed95ed155a80e9ea19b387bb5445fa2..ee1253b86e554319d71a05658c1c4858f926e07c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
index c2858d8543547cbf663450701310e6d0e80eacc0..f776ff5e9498ffaaf3c60e9a53355c6f61bea139 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
index b6325ad939dd17d487108ca8d85a1131776f01d6..6ba9bf6d9e72bc6e64cd61688f8cdcc5fdf226c7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
index ded5a71b828519a2afd55ceba70de25ee37769c3..96720f05fdbbdbb8623457e4ca5767f54f99ab5f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
index 11a917359cf6309e8a681cdcdf9020660b1dccfd..b0025ffba8ebc2642babca6f9fcd851f216bd704 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
@@ -17,8 +17,8 @@ FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `logic functio
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
index 86e479dd88bd3192d086e870c8e84c1a8ef6b46f..7ad062afafc8d8bad4709c61f468587851284ded 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
@@ -13,8 +13,8 @@ tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `logic functio
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
index 5ee27b10d16a494958cc6f2c4dc95b0b58bf6003..61fa2dd0ad737859c8c17bf3114aa8a6233b21c0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
index 72b8370d3d6581331ba93a4fe3764179f4334ef2..ec9a37710689a807271a4b7d015cf756100ae640 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
index 2908d36305ddb9b69532b8785bd73a4cff39ef3c..c3e6e6d19c5b2ad98f4064e02fa7e9839d277c3b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index ebab496bdc6bb5d55a6f52c373b8326374ef5f67..b75bd5d40869bf43313c8374d3d8f2f62aec17d1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
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 e1cd531afcbedc9290d092deeed97cf196feb2bf..c96be87ab712aed7a4c980d6ac2e95c6d4b19287 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
@@ -24,8 +24,8 @@ typedef unsigned int size_t;
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 e1cd531afcbedc9290d092deeed97cf196feb2bf..c96be87ab712aed7a4c980d6ac2e95c6d4b19287 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
@@ -24,8 +24,8 @@ typedef unsigned int size_t;
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
index b77ed944f6377f39d8948c1efe0fb739e4b9e42e..6d6583f6638659ea52612540c3655184360bf209 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
index b77ed944f6377f39d8948c1efe0fb739e4b9e42e..6d6583f6638659ea52612540c3655184360bf209 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
index cd1aa87a38f426969e732d9ecf3e7772e51485f2..2cc6f18177e38838932c94c70ad4d9f6ec49da31 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
index f594a2e752392012ac4cf38648d8547fe9e6f5b7..1bbc0c9654d741b860380ee0c7d2bb622777b7fb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
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 d09d7c3c54b3320c48c8b81ab501135f0d75c5a8..af4f3a3fd81e6a12e44cc40821871b136e2071d0 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 d09d7c3c54b3320c48c8b81ab501135f0d75c5a8..af4f3a3fd81e6a12e44cc40821871b136e2071d0 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 f38509d6a426c6745fbb399cddb97187e73cfe60..2fde55817581fc8c604cb479e9dd71e9ee66fcb7 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 f38509d6a426c6745fbb399cddb97187e73cfe60..2fde55817581fc8c604cb479e9dd71e9ee66fcb7 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 8a8625abd82ae9f3c5af14f0a755a40cda4323a3..5514e19c20ca70b21b61efa166a1da16452842e4 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 6c3acc4d9ec5cae1fff3a90ba0c375f80379763b..e9448e971bb55c45575cee1360a00d0bef9edf64 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 1615b6ef37741237930590c4da83cfa0f1774a4a..35a2e76b508a8b21d03bd4bea1672e66d7dbb609 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 0ac93b33fe09356f110703f3d698ff373861dfaa..37e6324859786f9fade1c3805d4ce9655391d462 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 60038ef2900abd6855980509323119cbf850e9c1..1d784f2cdacd7b24f031d181da7b793b91d7223c 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 e1d38eb53a07215124f9b9ff1025af5cd7038f18..715a1a811964f92b89b9784b605c465b96fbab07 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 cf51d7d52488f18bd6c9bcdb3bb8cf07aa9a7f8f..d8e01ffbb5d49b1671cfb6ccb5b22e510d764449 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 cf51d7d52488f18bd6c9bcdb3bb8cf07aa9a7f8f..d8e01ffbb5d49b1671cfb6ccb5b22e510d764449 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 6f92774bd2d62b405cfd02d1eae48cfd62c9254a..7ec7966af9338cf83a608049790b593c869f8dc4 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 7ec45739b59eefead54c26bfa2e504349db83a11..c45b13af2193bc8b0176187aa3e20aa03d214bfa 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 6c7cb59e21ec4f424fb612117cdce3ca1666a356..df1b5c1fbf752594c8ea204dbf0dc81d97e0f7a4 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 b8e9076ac30ba366f5f678c1b65a9ca2aaa2c84c..4c2fe7776ae8f71446e07cfd52e5bf514e7ec213 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 3ed665699cc1dd29a757b9d6d73642609c6ea16e..f5f1034d24985c3bc201e90dc70fce0b443b0396 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 3ed665699cc1dd29a757b9d6d73642609c6ea16e..f5f1034d24985c3bc201e90dc70fce0b443b0396 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 253d3d4adcaf597e650b92243e7f40b7683577e4..02887746306ca35fc5d113bf4058dd65d33bcc52 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 b91ecab66e449878ad5a6ec41e887736dcfbfe64..329843c1b49ed25ad473048f7581ca044351cf0b 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 f91e395aa1fdffea54cfa859160c3635fb3b7816..7f0e671807c13441f13ca02fe5467a8326202627 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 7e4312e3b45eb45f9a9755862c73871d570f1a8a..2b76c7ef6826fbf0900f0a4135c74fdb0c3e0b6f 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 2ad63c456df558dd0fd5d12c6f2b5f6e3eff2e03..862762c900984c1f591c44269a91a779e5d18a5f 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 2ad63c456df558dd0fd5d12c6f2b5f6e3eff2e03..862762c900984c1f591c44269a91a779e5d18a5f 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 4e4655bb33ab84a12ae4ca6853e2bd4320959ab8..e817129f94b57a869ba8ddb422a7ff1911cb369e 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 357c3ba8ae9d05b68d336aedbb8a53c6dc334b39..c6747b03d2826605d21acdd19657886c4c22ceeb 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 ca95f8bc50fde57d7c30b0c2e4b0853b61730c57..17edc7547d30849fc7fef2f5e0ab3023b91e59cd 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 4c27d12cf492b3766d436486f31f45eb80586eda..43521357a7b6ac017a0ec271432f495632c65406 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 f54bb89c336436b839eff2bb5f279a3f4242fea9..f9514e7699f98b9668297940f078ea39bbd6c5be 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 e0769e4505e7a90b9e40eb30eace8d8228ebe5a9..65543717ad65ecdd60dd4c1778acb0a4960cf86d 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 cf4ce4f86ef08b51b345a17365114ffc69de40af..d3ce4ce6b8b7fa706b49dfb59460cc5c265a0fa0 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 1112e66a66547f88590707f403d8dd7978c16c06..56c8f4f7969849e946c34848c4371681d52d9e79 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 313b731f630932758b161cea1817f46311a3471f..50947884763a4351ee0d1210b054de77acbe3179 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 3877084d38efa9d2a3308ed54f0e5b9302700cf5..6f087c5d81dcd74aa58f9a173f639ce047b1f4f5 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 ce2452867a9278c39c8205b6d358314e55003c1b..e4a52463a66355440094dc0540fc05117291d2e2 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 6dbaf12b8f1a5a490e88ee166102d552a310def7..7e106b402afe1fc682e93052854600de084f244b 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 780abf1d50ccca31ce2102876b6f080e0bf3cd0c..a6fe60a1e2799417dc36066e84c61de4f50a4a81 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,8 +22,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 780abf1d50ccca31ce2102876b6f080e0bf3cd0c..a6fe60a1e2799417dc36066e84c61de4f50a4a81 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,8 +22,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 1ec68a1de687fde8e23a9e64cd18671e48625333..a4bb6efa875c8b9e6f4dce4c8d1b3e5d06cf9a66 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 268ad6c1bafcc1834fcfdda0cc4a50a6c3b2aebf..983c49f3da40b18fff7a063a321ed8ffb7d92e71 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 0c2cf126e6e51f9b1003ab72fa5cb44dc8fd9b7e..017d65d08d5ca775270cf50198ba6e46e306687e 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 8a78fcd3c388a091e2f5f4718381134d55ead504..789eeed6d95e0b685bb1d007b18b5755f6f1e4ff 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 b8a8828aa6eb968b528230e09d3ff9ad9f165e2e..2dffc64ca52c9d92ecebf5280aeccf4b6103bc8a 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,8 +19,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 359147001c45c626ac1fdcf5aeceb43da5c8b67f..fcb3ad3ac0b25636428d9f23e17dba3fbe73b74d 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,8 +19,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 d12f78a04b9ed97f3e804268554215d22a6be4f6..f3bdecf27041c1435e609df8e25c86dda6a0eb81 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 e3f8fbe0b6c47c8210cbae9bbebe0025c1b6ed8a..d9b8a0192ccdb250b328cec2f6c9131a51cecfe8 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 80dce51c3a6d7d6d9ea5a71c1f14e6f16694ec17..4fe3c73b67c674ba40d01151765379894d692504 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 72532dc387cae31cf3cfcddb24db202e60d57a81..676e7c3a328d60fe271ff5bc966d0862fd2be980 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 216bb084e2be5bc1ba41f24c7166da6eeef0aa90..a09b2333e5245328a47e607b26fad3b34f7ae9e2 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 216bb084e2be5bc1ba41f24c7166da6eeef0aa90..a09b2333e5245328a47e607b26fad3b34f7ae9e2 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 4c13b1477b9f315fd70bb977d75f4ec830456e90..3cfb1dca11d84e641a0036ec3fcb0a9b4798bbe0 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,8 +22,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 d9cc1e203307d327f4345ad90eca85519e185c53..20eb9f1b21fb95fe23807f3b629228cd348da651 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,8 +22,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 878b9a3407a9d9e70e2a7f9d99b728e32d48a69c..3cd0ce6d69f1d0429eaf4da85fa20e90eee33e02 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 1e3430db81471e24729d131e2f3d05ad398f9365..b58a645ffe756bac21f4d5fb5fbedc6fd85c0f0b 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 a79f65348bfe2ed77ffc77a5159a946ef15b90eb..7eba374f37b83e18e221e1675afa3a6442d0732a 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 a79f65348bfe2ed77ffc77a5159a946ef15b90eb..7eba374f37b83e18e221e1675afa3a6442d0732a 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 b882f493333ad5ecd74ed506f963ee0935c3d85f..b3e10d11118ae131a3f74767740287d909bb70db 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 4adb08a08f2aa032322c282efc2ff4670d6ae5de..b026674235d0f9833ea4317c2935bdae90101cc2 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 2792dcf8aaf932c3cfa90a0a1f5890efee3c87cb..e2992629f11b5c954e9c0b134993096a447fdd7e 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 90cdc6aeae07ca3a4f768617ea199aa65e09216b..c8306f004fe026b866e5b75d76866f3715e5c540 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 77e7a73136decfc978c21c240a4121babf139640..7c3daa2acdceb95c1bbdddc0d17711abdfdd685e 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 f6c96b33c089c8383945c0a474486b97d4cfc767..e6821c6545f986b0225e6c62a576de27cb0e429c 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 7531b683c53aa238c55c5c97d130967d91c6eea7..f4eedb8b927580579e693e6e9967be45e9f84632 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,8 +58,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
@@ -82,6 +82,9 @@ extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
 
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
+
 /*@ ghost extern int __e_acsl_internal_heap; */
 
 /*@ assigns __e_acsl_internal_heap;
@@ -97,8 +100,31 @@ predicate diffSize{L1, L2}(ℤ i) =
  */
 extern FILE *stdout;
 
-FILE fopen[512];
-FILE const *_p__fc_fopen = (FILE const *)(fopen);
+FILE __fc_fopen[512];
+FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
+/*@ ensures
+      \result ≡ \null ∨
+      (\valid(\result) ∧ \subset(\result, &__fc_fopen[0 ..]));
+    assigns \result;
+    assigns \result \from *(filename+(..)), *(mode+(..)), _p__fc_fopen;
+ */
+extern FILE *fopen(char const *filename, char const *mode);
+
+/*@ ensures
+      \result ≡ \null ∨
+      (\valid(\result) ∧ \subset(\result, &__fc_fopen[0 ..]));
+    assigns \result;
+    assigns \result \from *(filename+(..)), *(mode+(..)), _p__fc_fopen;
+ */
+FILE *__e_acsl_fopen(char const *filename, char const *mode)
+{
+  FILE *__retres;
+  __store_block((void *)(& __retres),8UL);
+  __retres = fopen(filename,mode);
+  __delete_block((void *)(& __retres));
+  return __retres;
+}
+
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& stdout),8UL);
@@ -108,17 +134,32 @@ void __e_acsl_memory_init(void)
 
 int main(void)
 {
+  char *__e_acsl_literal_string_2;
+  char *__e_acsl_literal_string;
   int __retres;
   FILE *f;
+  FILE *f2;
   __e_acsl_memory_init();
+  __store_block((void *)(& f2),8UL);
   __store_block((void *)(& f),8UL);
   __full_init((void *)(& f));
   f = stdout;
+  __e_acsl_literal_string = "foo";
+  __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
+  __full_init((void *)__e_acsl_literal_string);
+  __literal_string((void *)__e_acsl_literal_string);
+  __e_acsl_literal_string_2 = "wb";
+  __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
+  __full_init((void *)__e_acsl_literal_string_2);
+  __literal_string((void *)__e_acsl_literal_string_2);
+  __full_init((void *)(& f2));
+  f2 = __e_acsl_fopen(__e_acsl_literal_string,__e_acsl_literal_string_2);
   /*@ assert f ≡ __fc_stdout; */
   e_acsl_assert(f == stdout,(char *)"Assertion",(char *)"main",
-                (char *)"f == __fc_stdout",12);
+                (char *)"f == __fc_stdout",13);
   __retres = 0;
   __delete_block((void *)(& stdout));
+  __delete_block((void *)(& f2));
   __delete_block((void *)(& f));
   __e_acsl_memory_clean();
   return __retres;
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 7531b683c53aa238c55c5c97d130967d91c6eea7..13b9fa9cf18134adad785b59484613d3bc98d365 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,8 +58,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
@@ -82,6 +82,16 @@ extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
 
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+    ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
+    assigns \result;
+    assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern  __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
 /*@ ghost extern int __e_acsl_internal_heap; */
 
 /*@ assigns __e_acsl_internal_heap;
@@ -97,8 +107,31 @@ predicate diffSize{L1, L2}(ℤ i) =
  */
 extern FILE *stdout;
 
-FILE fopen[512];
-FILE const *_p__fc_fopen = (FILE const *)(fopen);
+FILE __fc_fopen[512];
+FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
+/*@ ensures
+      \result ≡ \null ∨
+      (\valid(\result) ∧ \subset(\result, &__fc_fopen[0 ..]));
+    assigns \result;
+    assigns \result \from *(filename+(..)), *(mode+(..)), _p__fc_fopen;
+ */
+extern FILE *fopen(char const *filename, char const *mode);
+
+/*@ ensures
+      \result ≡ \null ∨
+      (\valid(\result) ∧ \subset(\result, &__fc_fopen[0 ..]));
+    assigns \result;
+    assigns \result \from *(filename+(..)), *(mode+(..)), _p__fc_fopen;
+ */
+FILE *__e_acsl_fopen(char const *filename, char const *mode)
+{
+  FILE *__retres;
+  __store_block((void *)(& __retres),8UL);
+  __retres = fopen(filename,mode);
+  __delete_block((void *)(& __retres));
+  return __retres;
+}
+
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& stdout),8UL);
@@ -108,17 +141,32 @@ void __e_acsl_memory_init(void)
 
 int main(void)
 {
+  char *__e_acsl_literal_string_2;
+  char *__e_acsl_literal_string;
   int __retres;
   FILE *f;
+  FILE *f2;
   __e_acsl_memory_init();
+  __store_block((void *)(& f2),8UL);
   __store_block((void *)(& f),8UL);
   __full_init((void *)(& f));
   f = stdout;
+  __e_acsl_literal_string = "foo";
+  __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
+  __full_init((void *)__e_acsl_literal_string);
+  __literal_string((void *)__e_acsl_literal_string);
+  __e_acsl_literal_string_2 = "wb";
+  __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
+  __full_init((void *)__e_acsl_literal_string_2);
+  __literal_string((void *)__e_acsl_literal_string_2);
+  __full_init((void *)(& f2));
+  f2 = __e_acsl_fopen(__e_acsl_literal_string,__e_acsl_literal_string_2);
   /*@ assert f ≡ __fc_stdout; */
   e_acsl_assert(f == stdout,(char *)"Assertion",(char *)"main",
-                (char *)"f == __fc_stdout",12);
+                (char *)"f == __fc_stdout",13);
   __retres = 0;
   __delete_block((void *)(& stdout));
+  __delete_block((void *)(& f2));
   __delete_block((void *)(& f));
   __e_acsl_memory_clean();
   return __retres;
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 b7927180ad1a31bd753b6c269ae003ad728e57dd..dbada0dda058055449e510f927e7765e00b196fa 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 e0cdb70d6eac1a6c0f58bd15b31fb553557d7da2..ac6f0177bbb32b082aaa78486d555bcbdba4e47a 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 720929a8f71b9186e8683973f5aee01ddd39c7be..c7f61875787758513755bd9b4326dfd98efc3e98 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 720929a8f71b9186e8683973f5aee01ddd39c7be..c7f61875787758513755bd9b4326dfd98efc3e98 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 8149e2edc106d318433b5d835609eabb12d54d48..146b775b2f6bf29a8c7b7ccd6441a77c5e4f41d3 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,8 +19,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 e69481cbedece490202df66be6e3a16193d1b822..09cb51fe38a3edcc4963c0386f163914229ba686 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,8 +19,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 93df89f36dffc5b8ac8d92d5ab75aa890ded93f6..e63da0d3e7f1bc518389643fe8979d952ffa35f4 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 93df89f36dffc5b8ac8d92d5ab75aa890ded93f6..e63da0d3e7f1bc518389643fe8979d952ffa35f4 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 ddde059e9211f2441731373cd29f2f330bdc3acd..db243d2e0634cc22715f601251b5ff36a36cc0ec 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 9702b5b68b4781b10bb4e91893c86ae13f5c6de5..9379b88d9eadade5907f91250963b1720d5419d7 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 5964f59070216d8c0b715aeb6191c42f2acc0006..45a24b77ddd2a9497c732e87c4c2a77d92f49865 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,8 +22,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 5964f59070216d8c0b715aeb6191c42f2acc0006..45a24b77ddd2a9497c732e87c4c2a77d92f49865 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,8 +22,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 3f50777239b1cf27f792555407328b2780f3c82c..15e875caf18ba38d5a720d286d23772f65b28510 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
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 e4f0303aa767b4e8e4cfe004f35be81299bb93c9..497c9c7411765223c95d5484dc65bd4446844f4a 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,8 +18,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
index c61173356b53c2af890d7759127c3fe5cb61c76a..97bb0712a0349c42d8143936a53e0225a1de5860 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle
index fdfc7990ec2c29f1d1410789c00a8ed9772ca0a5..2cee1d69b38777ad323fcae841388704d3f43b10 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
index 6f95e59543baf65560038f994955f6ed088a38c7..d0c22cc84bc5858e31c82c35029cd68e9bb80876 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle
index 6f95e59543baf65560038f994955f6ed088a38c7..d0c22cc84bc5858e31c82c35029cd68e9bb80876 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
index 6f64ff4256ae554831a4e2008431f1e8c761e8b7..db4cb25cd186a33fd8b4a9edb4f398e8ab9929fa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index 75e76b3c1fad68b08eabf579639765e1acfd0c3f..f7340321cd0498bee0597b1d17fac485ffeb73f1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
index b5d994b3a4c6b3482b6019c76acda278f2e9ca1a..adb93500ead6803a182070f51da5d55da0c60890 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
index 1b3bf80d4f4b0d183b8cc6e9f50d664d8040c03a..ada600909030a9236134c45221480e4010d7d1a9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
index 570ea6d0d060ae8611aad2332c1ede8e90da2f12..34d08a38a829e7832700cdf01e9aa249e21bbbfa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
index 3f92625eb67b27aa223e4320614011e8ac28d3d0..ea82cb27ffb5ea7f7466582b93de03784f651004 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
index a3babb0b4f12994a5e28abdddee8b8d1dcf1e6a1..55a6dc8a5ed9f671198fde6e06e7452b308c7d30 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
index 32af23aefb16f26c8c847df16f18d4e6adff764e..c79ae4bf45f2df4c73d7e2f298441875adb66737 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
@@ -7,8 +7,8 @@ tests/e-acsl-runtime/lazy.i:16:[rte] warning: divisor assert broken: 0 ≢ 0
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index 9d1b1436f98006fa264c1adeee2d8bc20f37e75e..ed5739d6aa150d63e00ac048663cba8e03ba4464 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
index 2de1029abd063b5d79109082fda2653f30414b24..6000f8fb4f899bf620bb4f89242728132df66cf9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
index af73885cc561db30b0b81da3b9a04abd8f158bb9..89839e8fac30b0b0fb8a4b2ea3eb891346fe16b2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
index 5109ba1df0f63edd018be6214a91e3e670639a2e..cbfef42b8bf3b4235ec9009a1379adaf840049e1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
index 1cca0a2e3ed3dd9b249021d56b33da60a4f18818..b3b06850962d2ba9d57d64bfc60d54d3d0ef4241 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
@@ -17,8 +17,8 @@ FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `logic functio
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
index c1caa33286b7a63c5f8c31157ffbb0fc05755b90..823d6aabb3181ff7d9987efbbc2830e9baa75df6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
@@ -13,8 +13,8 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
index 15598c2640853180be93caf7d27aa3ec27a2a1ab..ff68f25afa04fe2a52efd90ac633aad35b691674 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle
index e8925e28b35588811198edde478ecc1d13b54165..2877bdc22a3f46acda0bfc2864b22ab396dce3e9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
index 087bfb0829d57a0829a94fa9d66e7742b942790b..8f017d69ecda578fedd10674fa0e54f7ff3e4575 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
index 96db9cc42a3344bfd8d0f6af3b7b9fc56943bc91..71aa24d07a4ebe77322512e04d60d25e1922a645 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
index 02eb94e3703ddf0d13f85beccef082ffc836868a..0edcfe44db52d5b9bb2baea7f7d1bd052f0ce766 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
@@ -13,8 +13,8 @@ FRAMAC_SHARE/libc/string.h:88:[e-acsl] warning: E-ACSL construct `applying logic
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
index 53f26299b4a71fbd9955ea10f2edbea9a1311db0..a4c8eb909d1c8691fdb252f0233ac1b7010500d6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
@@ -13,8 +13,8 @@ FRAMAC_SHARE/libc/string.h:88:[e-acsl] warning: E-ACSL construct `applying logic
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
index e0b1cb0c3d979bfd9e515314fc32bfbe59d11a8c..8a8222523676e72bcfd05feaffb8090b026f21e5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
index f6cf15e6ea1c7b4479a60dbfd8ced6af0df5dce2..151f864ecdd500fa488537b7a014ce8494bd6cc5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
index dda4be5ebd969520fdf5548b48a91c6f4a9a4fb8..57e6831e42f440dc422074515b54e430423919e0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
index 16bde583746558b5d2fb1feadc6915032879540a..c4513a0cf3efae76f1bcf98037fd67ee37f3150e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
index bf8c4859320b966a8267fa0c7b444b7267756253..6d317b9c751dc5b6bcf67ac364b320f0d6fda1d1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
index bf8c4859320b966a8267fa0c7b444b7267756253..6d317b9c751dc5b6bcf67ac364b320f0d6fda1d1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
index 966bbf3f9ede1b14574857d777a280fbab21e190..4c6b098dd0854b40e73fc6e248f2297b735c794b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
index d59dceb58ead491807f9d207af5d81a6ecef9dbe..dec8067549f0bf1957e11931a1fba51ccf39a0ef 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
index d8345c4eed8bfbd56ea5f53ecd969d459bcb153b..d044420359cf20d697297fb0d92bf8ebd5635913 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
index 67d6935766eff32842a60a21c08444a53148a9a6..3815dcb62e094b9f98b97808c5d4ec59262bacf3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
index 1cc53371d79554e4e23f4dcfff86a43af46fa20b..40d70b4af825e9c074c0c616323a7e82e428e10e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
@@ -17,8 +17,8 @@ FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `logic functio
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
index 2879d0ab923611951267632dec7ffd95582651a0..554ca48e7182f60e812b9f3714185bc6795eac51 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
@@ -13,8 +13,8 @@ tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `logic fun
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
index 67316f6bcda689d4a9304f11de44536963e62f39..f57dd54e53ffebbcbf3011c4e11fc11e343db5d8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
index 539678d62e9bdea354b819317b142e0bb0c85150..953488ee27e808fe594665de5b13b3a3315402c7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
index 02df4c9a03f3860d0050d6241af9c8ed94887ce1..768f090efb61438ee48bc21e95b83a5cdeb085a6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
index 40f2b194ea5f02e790c4ab461078014c246e936e..7ffb06bab752ca3b2195b77a6562e7de54169ede 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
index 32e1ef3c35a77e3a2acef18a1f1a914e61a7a6db..505160e67de12c2668dc9cfc95a4ccbb67ef106b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
index 77557d4b4f5b64e48b2edea40bfd49459315d7f0..3d936884430f4315dda3561e2fd36797eceaba98 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
index b61a91ef3ae8450bcbf594b02f95d8535b935cb6..c99d74f71f1ced6c5b1f5e0db6edaa19c73c07c9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
@@ -1,18 +1,25 @@
 [e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `fopen':
+                  the generated program may miss memory instrumentation
+                  if there are memory-related annotations.
+tests/e-acsl-runtime/stdout.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdio.h:95:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
   stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
-  fopen[0..511] ∈ {0}
-  _p__fc_fopen ∈ {{ &fopen[0] }}
+  __fc_fopen[0..511] ∈ {0}
+  _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
   S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
                [--..--]
                [0].[bits 80 to 95] ∈ UNINITIALIZED
@@ -36,9 +43,12 @@
   S___fc_real_data_1_S___fc_stdout[0..1] ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
-tests/e-acsl-runtime/stdout.c:12:[value] Assertion got status unknown.
+[value] using specification for function __literal_string
+[value] using specification for function fopen
+[value] using specification for function __delete_block
+FRAMAC_SHARE/libc/stdio.h:94:[value] Function __e_acsl_fopen: postcondition got status unknown.
+tests/e-acsl-runtime/stdout.c:13:[value] Assertion got status unknown.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-[value] using specification for function __delete_block
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
index b61a91ef3ae8450bcbf594b02f95d8535b935cb6..c99d74f71f1ced6c5b1f5e0db6edaa19c73c07c9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
@@ -1,18 +1,25 @@
 [e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `fopen':
+                  the generated program may miss memory instrumentation
+                  if there are memory-related annotations.
+tests/e-acsl-runtime/stdout.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdio.h:95:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
   stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
-  fopen[0..511] ∈ {0}
-  _p__fc_fopen ∈ {{ &fopen[0] }}
+  __fc_fopen[0..511] ∈ {0}
+  _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
   S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
                [--..--]
                [0].[bits 80 to 95] ∈ UNINITIALIZED
@@ -36,9 +43,12 @@
   S___fc_real_data_1_S___fc_stdout[0..1] ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
-tests/e-acsl-runtime/stdout.c:12:[value] Assertion got status unknown.
+[value] using specification for function __literal_string
+[value] using specification for function fopen
+[value] using specification for function __delete_block
+FRAMAC_SHARE/libc/stdio.h:94:[value] Function __e_acsl_fopen: postcondition got status unknown.
+tests/e-acsl-runtime/stdout.c:13:[value] Assertion got status unknown.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-[value] using specification for function __delete_block
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
index 3c8da283445f6deecd64f0a3afbe99750315b449..c59e20f10fd17a74290d278d7ea5b649cf70a7d0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
index 1d4b3e002271135150b1d91d5891bfd94ea47cd4..7e1ef6d4aa6f36be6b2098a8fc8ada9ada27fb83 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
index d93c1ec36037a6fc7fef761c51815ab6bb606ec9..549d5a145b57a3cf106beb3e8cf8f10f6b8d921c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
index d93c1ec36037a6fc7fef761c51815ab6bb606ec9..549d5a145b57a3cf106beb3e8cf8f10f6b8d921c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
index 07e51862ce1728e38198487834e6c1d17525ee9a..eff640e073cf9b125066b2b65c845ede4420e963 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
index 21d29301271576ef42e82f4787f9b943d75f2eee..3e13beeb9f8206ad7c14d7a9d634b55e59cac7fc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index 9b93e8c95bdda327e19112e4406707f7a924d65a..c3ae2925bf66404400ca61ec2ad1022913b0f420 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -27,8 +27,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index 5044ab4e589609a8920410830befdc531c2a8e0c..4a818423ac9b74967a108c77eade101b009c80b8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -19,8 +19,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index 7682f1615baa79623ff7b256397065225785d08d..2da3ea9dfb651306b992df2918507b1df5bf83d1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
@@ -27,8 +27,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index 060731ee943a1998d09e3bf82af3f20c68acb83e..fcddec8a4b8ac3654748d38a2c02de2cf0f28eef 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
@@ -19,8 +19,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
index f4761bf8c34473bcedbeef7add7ffa8c65e0d121..3d3bab60483259699c068dc6bb03f87b62b51533 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
index f4761bf8c34473bcedbeef7add7ffa8c65e0d121..3d3bab60483259699c068dc6bb03f87b62b51533 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
index 86b2fcec9e28a41832e6465f690092bdf57a85f7..3eea9bdbc1b63e7a7b5b51de74128965213daacb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
@@ -27,8 +27,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
index 233c8f7660a8f4f41504876ea449ccca44c923e9..4eb0ff3fad7ca205c259b7d273f5b85443e36682 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
@@ -19,8 +19,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c b/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c
index 21c3e08bf613048ca416e089855c99d7988ab969..10cb12f2c52462001bd53d9e01c9e54c6b511d8b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c
@@ -1,5 +1,5 @@
 /* run.config
-   COMMENT: __fc_stdout
+   COMMENT: __fc_stdout et __fc_fopen
    STDOPT: #"-pp-annot"
    EXECNOW: LOG gen_stdout.c BIN gen_stdout.out @frama-c@ -machdep x86_64 -pp-annot -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/stdout.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_stdout.c > /dev/null && ./gcc_runtime.sh stdout
    EXECNOW: LOG gen_stdout2.c BIN gen_stdout2.out @frama-c@ -machdep x86_64 -pp-annot -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/stdout.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_stdout2.c > /dev/null && ./gcc_runtime.sh stdout2
@@ -9,5 +9,6 @@
 
 int main(){
   FILE *f = stdout;
+  FILE *f2 = fopen("foo","wb");
   //@ assert f == stdout;  
 }