diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 628dd97bbb5ce9ebbaccffe449828435f9469580..7210380aca5660baf0847e8a02bf366ea6f963da 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2014/07/08] Fix bug about using some part of the
+ (Frama-C) libc which prevents linking of the generated C code.
-* E-ACSL [2014/05/21] Fix bug #1782 about incorrect URL in the
documentation.
- E-ACSL [2014/03/27] Remove spurious warnings when using type `real`.
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index 3b41b48dd89c31bbbb4637362a7936a53147e08d..a798b1ccb13ed2a598fb8713420057412177a4f0 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -197,10 +197,39 @@ let add_e_acsl_library _files =
- locations are better (indicate an existing file, and not a temp file) *)
let () = Cmdline.run_after_configuring_stage add_e_acsl_library
+(* The Frama-C standard library contains specific built-in variables prefixed by
+ "__fc_" and declared as extern: they prevent the generated code to be
+ linked. This modification of the default printer replaces them by their
+ original version from the stdlib. For instance, [__fc_stdout] is replaced by
+ [stdout]. That is very hackish since it modifies the default Frama-C
+ printer.
+
+ TODO: should be done by the Frama-C default printer at some points. *)
+let change_printer =
+ (* not projectified on purpose: this printer change is common to each
+ project. *)
+ let first = ref true in
+ fun () ->
+ if !first then begin
+ first := false;
+ let r = Str.regexp "^__fc_" in
+ let pp () = object
+ inherit (Printer.extensible_printer ()) as super
+ method !varinfo fmt vi =
+ if not vi.Cil_types.vghost then
+ 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
+
let main () =
- if Options.Run.get () then
+ if Options.Run.get () then begin
+ change_printer ();
ignore (generate_code (Options.Project_name.get ()))
- else
+ end else
if Options.Check.get () then
apply_on_e_acsl_ast
(fun () ->
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 6eeca12deeedcbea748a4f78897a6c450b968a5e..3d10cb740c7e5c0f310edbcc0b8d7d5007ea29df 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 6eeca12deeedcbea748a4f78897a6c450b968a5e..3d10cb740c7e5c0f310edbcc0b8d7d5007ea29df 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 ebbeaef53da6c8aa133903e0681dedb2cb79fe3e..beb597a013456946bcffe1d646477ca664b86284 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 ebbeaef53da6c8aa133903e0681dedb2cb79fe3e..beb597a013456946bcffe1d646477ca664b86284 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 8d0c810c62254083fe456a4a64b090e43862012a..78ee7781191a9edcbb9d98e2b486c453b28bd3d4 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 9d33b17f15c80b5d11a490afe61a39ec975c897c..0cdf4bac1916c72f0555794875a6b369b5ea8598 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 c4cd42d3ae35fc9d4cfce2c56dce80914ccd9f5a..454b7b14a1c3d5fd10c6b6269d52d0ad07dc4783 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 4c3f47d2031b3a2de94fe8ad06176bc8fb513e03..34280485ca06b815472122fddf462b92a5f01437 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 d4a2472d1c5c63be517f7e40955e6ae42a4caa87..5294f75d2b31f987fb90155f06e88dfb632fcddf 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 4f19c71c8d4c49842479f53f5430087968c0a8ec..132bc9553b5c14d1f1cda8661c9568de0002788f 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
index 0b17e914e6e4eff8910cfeff8019e7d24f64fb67..a461761af127100cbae97591ed95712a0ec66d8a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1304.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
index 0b17e914e6e4eff8910cfeff8019e7d24f64fb67..a461761af127100cbae97591ed95712a0ec66d8a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
index 29bb832ec0d55d3ae59a7ec86a8d2ea20ea1ce4f..9da17af23eb05c0c00e1b4e824a4b3559f32d6e3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
@@ -14,8 +14,8 @@ tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1307.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
index 464bfd42cf62f5f946cac1add1099c61f8f31d85..49e77bc016918215299eccfad9aa0ad5c0b4773b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
@@ -14,8 +14,8 @@ tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
index a4c946ba598074f8f45d19e8268149c7234c5e5f..843698257a811b1961815fe5c86fb1321986609b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1324.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
index 488866b8fa5f350308669318620a2d6c662f4a34..447c838d1e56fead38215f98e7985e2903c01670 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1326.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
index b81f489bed1e9a4b2e597558cd042002a73118d1..ac2e364690f2e617be11ab4ca8135e1fccf4ade9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1326.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.res.oracle
index 856636dcb07759c5e51e0bbbffa5f93da58a7f49..eb9277270dd3ae119a41a516be9f8b782e3710b8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.res.oracle
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
index bd257da45dfa67eb590865df46480d18725d33fa..f8ad3751c31f0b3c347c869465da40c78e2a718b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
@@ -11,8 +11,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1390.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
index ef41ce840583d56292487611f3dc3b1b9f0ae540..45b009a504716b7e792d9b08d89608ee58cde6c9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
@@ -11,8 +11,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1398.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
index 877d15f251ecc37cde876cc196034793d12306f1..af5dc40fc73e85fe7d25b39e77fbae734353e968 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
@@ -11,15 +11,15 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
- __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
- __fc_fopen[0..1] ∈ {0}
- _p__fc_fopen ∈ {{ &__fc_fopen }}
+ stdout ∈ {{ NULL ; &S___fc_stdout }}
+ fopen[0..1] ∈ {0}
+ _p__fc_fopen ∈ {{ &fopen }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
[--..--]
[0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
index 877d15f251ecc37cde876cc196034793d12306f1..af5dc40fc73e85fe7d25b39e77fbae734353e968 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
@@ -11,15 +11,15 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
- __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
- __fc_fopen[0..1] ∈ {0}
- _p__fc_fopen ∈ {{ &__fc_fopen }}
+ stdout ∈ {{ NULL ; &S___fc_stdout }}
+ fopen[0..1] ∈ {0}
+ _p__fc_fopen ∈ {{ &fopen }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
[--..--]
[0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
index b072fd282085811b9c36b0d7365932af76cd7c48..b634bce49662c13c9de1ae742568d439afe39e42 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
@@ -34,8 +34,8 @@ FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1399.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
index 21a68ed15107334ea2e67558e9b03fd6de4a1dff..8cfdc8dc491ace729ef0059ab53854c20d0070b7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
@@ -26,8 +26,8 @@ FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
index 5d373286f97733088b0f8e3a59448c9212ff2665..44f5c5647e533e34a56c2c4b04532469f429e81c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
@@ -11,8 +11,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1478.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
index 0d9154cd481948b92d014d02a1bcd5532d394204..76d0e9b7e0a3933965f5588a5277d0e5b8be81a3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
@@ -11,8 +11,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1700.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.res.oracle
index 74bbf857adb7b54faca5fa445c26eaf4a1ec3fbe..71cc1729670588514e9090b9303e990a8ea57fd8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.res.oracle
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1700.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.oracle
index 74bbf857adb7b54faca5fa445c26eaf4a1ec3fbe..71cc1729670588514e9090b9303e990a8ea57fd8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.oracle
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1717.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.1.res.oracle
index b04cc71f53280031fedba4cdf4a5ab6fadaeb0af..f0036c5d7704dbd3aeb9272839501ae987a83c02 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.1.res.oracle
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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/bts1717.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.res.oracle
index b04cc71f53280031fedba4cdf4a5ab6fadaeb0af..f0036c5d7704dbd3aeb9272839501ae987a83c02 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.res.oracle
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 5abe18e21315f9b5d629e91228e2bc57e6d64083..2922e483dde28df30836385aece9938a3ab4544c 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
@@ -24,8 +24,8 @@ FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `logic functio
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 a2a8d96b0bde0c35cea035cef2ee38a3e0dec79d..a873c96d7ec971d28a44a870fcbb39f64d214c6b 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
@@ -20,8 +20,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
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 20ae38c9e7f26eb512d3e58d83ffcd8842fb3095..8a954fea71f67d3e70059448c229ba4d8da6b1a3 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 cfb947c60f7bbf02778739e54c9c86531e7c51f4..b8abbec8223a4a367108379067dd76137b3f22e8 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 f86e56173dfebcf63c0788c2aa4a83dc6ed8a4cb..fce50ae2277057ac7ac568745d9666de8a16741b 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 e77b42acb2e36d03b62fdca99f3e90a29a6bf80f..c5a32de22067e928d9a201609d20605b04cae545 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 38ce731e0a0e0ea119f9f13d3f0249b83b91ec1c..a64cb6809462cc1c4a9e0bab175ca2c94b28242f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
@@ -22,8 +22,8 @@ typedef unsigned int size_t;
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 38ce731e0a0e0ea119f9f13d3f0249b83b91ec1c..a64cb6809462cc1c4a9e0bab175ca2c94b28242f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
@@ -22,8 +22,8 @@ typedef unsigned int size_t;
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 dbb2932fc8d63a050db25d1a57fa1f68a9df7a5c..7610e778e933bd0ba0dd1cfa131ba23572e0294e 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 dbb2932fc8d63a050db25d1a57fa1f68a9df7a5c..7610e778e933bd0ba0dd1cfa131ba23572e0294e 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 e09ec22fd91f296819b0863778328fc6af78bf55..a2ff92e8e24edffb005fcc19d5f5623e7c889e0f 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 874df546bf09e6439d1a878e1ac445b14f860cd8..eb34979bf181dce2fad004c735aa35d408745ab2 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 78d13f82b67c368ee3a63855fa688aa47c86a5b2..fab581fe35d6c970a4edd9b84be778aaaad4e771 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 78d13f82b67c368ee3a63855fa688aa47c86a5b2..fab581fe35d6c970a4edd9b84be778aaaad4e771 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 21d3dee0e0f030f66ac342a53dc280c04406bcb0..3595848a6626dbd2bd6f667e492ea4ab78cb9a34 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 21d3dee0e0f030f66ac342a53dc280c04406bcb0..3595848a6626dbd2bd6f667e492ea4ab78cb9a34 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 8247aa4992b277a595fe1a382605022369903f86..474a027f30510cfa6ec4ea95bb875c90d360df1c 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 820086317114462508624a70a06064a4945a2433..8e826c199676e88eb18b7b2dbbbfe63d88522718 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 c765bd1a860143148c2b182ed6978dee10a24bf9..426291f1f93f1d02fab0a94816170dd86bea504f 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 bf258eef4aa8b408b9f9f6614ed08ae1140ea16b..3465af736a5a03ae431c3c76eafad3eba0938d9b 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 a325b76062211a5ed436c20d38fe24a87c00d72a..a86d2c65f524c49a2207992c212900c731020c67 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 c69173bbeae7168a53b9f1c88f132b95e8bda473..fbad827ab0661a99eb57e5a6fa500878cd8c4a08 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
index efdb482b820a7b5c40527c92f786aac9dcdd94c6..45945925656d360d54ef320de566038fcca6ea91 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
@@ -34,8 +34,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = 32767UL;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = 32767UL;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
index efdb482b820a7b5c40527c92f786aac9dcdd94c6..45945925656d360d54ef320de566038fcca6ea91 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
@@ -34,8 +34,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = 32767UL;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = 32767UL;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
index 31a9781a1007907da2d0e67b2dda838bd09e2074..a3882707f84331eddbef3f9cb447f072b0700735 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
index 3b4af93775d4e858061c87f93a503a03dc7ff2ab..f2953f325152d085c11ff40ea971aec9b4ed1515 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
index 560261c0f557090fc2db80dc6af50b238e3b0580..97c05e9203abbf57efd919e8103eb3b7f2ca84bb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
index 89edfb78504c7af7a6753a678d3f93c8c27952e0..669dbe87e7bf522a236ea4566ec8742d9a3a9b71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
index eb2080fc217d181bed7ae86727654bba84fd810b..d0e407c5451f821e53dfef8a35d799afe52b4225 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
@@ -19,8 +19,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
index 8c3ebbe99700f48e7476ffde0cfdbf6f473e803d..50e0edfc00c9ab4a48b49e3c5be747c6554b91a8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
@@ -19,8 +19,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
index 2b98891e4a70b7f4f3c062cb2785dbf22e4b3c07..17b721b9dd2600087cd3a2a9abab40dcc6254d1a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
index b4ea1d9be57be3006931d9da16780fea4f06541e..27a2a4a4de8765444722501162302424c9dee96b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
index f09bf2f1116c0f70e52d9f3e87d324ccc6b27974..7cb3e53d8fe96574acdc9e24e5b94311ff909df3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
@@ -47,8 +47,8 @@ typedef struct __fc_FILE FILE;
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
@@ -80,10 +80,10 @@ extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
-extern FILE *__fc_stdout;
+extern FILE *stdout;
-FILE __fc_fopen[2];
-FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
+FILE fopen[2];
+FILE const *_p__fc_fopen = (FILE const *)(fopen);
/*@ assigns *__fc_stdout;
assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
index f09bf2f1116c0f70e52d9f3e87d324ccc6b27974..7cb3e53d8fe96574acdc9e24e5b94311ff909df3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
@@ -47,8 +47,8 @@ typedef struct __fc_FILE FILE;
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
@@ -80,10 +80,10 @@ extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
-extern FILE *__fc_stdout;
+extern FILE *stdout;
-FILE __fc_fopen[2];
-FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
+FILE fopen[2];
+FILE const *_p__fc_fopen = (FILE const *)(fopen);
/*@ assigns *__fc_stdout;
assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
index 45a8c5865d8ec62066579026e41ee9a880ad12fe..d4a592d8a9f2a3bab78bc0fa50a05c4102b64d75 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
@@ -24,8 +24,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
index 9b75f0ffe84564c135e12bad95eabd3e811ef524..3074489280dc5c55d8842a30f4a6a092a1651128 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
@@ -24,8 +24,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
index d9defb9f39085df3a61f9f88a36b6afd350f806e..356c8305d69aceb78e20d5c4a62fe79ee13eb7f3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
index 2f5253714910fda4ff031c1058dcd8c4d0e1a4db..0e3f2d02f3d7b54f593d9675d113fddb11cffcbc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
index 7258ddac41bf74445d8b0d57912d430c70f90095..bd982bc4f57866c66a1a1f2745b62d97ed33527f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
@@ -21,8 +21,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
index 87cc310d9afb045bd4e425ed2b6179d0b6fcfd06..58a1bbf0c1a589b4e5e64d373f722c0467e25ab4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
index 87cc310d9afb045bd4e425ed2b6179d0b6fcfd06..58a1bbf0c1a589b4e5e64d373f722c0467e25ab4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 4287e8ff2714275b64a6c3ba9de8f6dbeae8d01f..c16bdde76b03311c1253d51390f509f7dbab7023 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
index 4287e8ff2714275b64a6c3ba9de8f6dbeae8d01f..c16bdde76b03311c1253d51390f509f7dbab7023 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
index aa39b2d317a82f1cf1b25bbcc01326f54a2ac159..d802950c13eacce1febb790c3a38b576b2ce9104 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 291d9b6fdc6db0e2bfeb1adcf8df77a4bf982024..ef9d9264b5f76853b0c05785d38c7af8c6253008 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 ceb5d2b3fa7d5e2b05376c4519a9e3336fad3520..dc712b9c16daa6b91e17d2b42e8621f8b2c06062 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 5759207338083c55c108456a88bb4448b11e0aad..d7ab417d961d662cb451096b1860659f8cc9d98f 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 0acbead3158b8a94b1fc1343d2800d3902c870c2..5c50649668fcb976874d7c2abf64feba0ae0a246 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 0acbead3158b8a94b1fc1343d2800d3902c870c2..5c50649668fcb976874d7c2abf64feba0ae0a246 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 4ff593abac462a51cf0f7101c755c760df6b1fbf..78ffa12f7d100dac49fbc0fd9fd3e3c461399190 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 18ed30062a9047a7c040b1997af25ec767a75a13..9a70717d35144abbcc4c203e5a21be1058260dad 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 c8f1be53be9640ee9d3877e1b9927cc4d6dd487d..8ab2658f325d1f8326f115d39bdb81f41af42f75 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 d117e37824f81a1787743d3fcb9d9d4986aefbf7..0b1470d48fdf997b3ddfa52204aa20b803cebf40 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 596b7b58c76cbd7859636f3ab82d3b348314657d..5b40837b51635f32daf9bcab776b7ab36e4587af 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 24f06299028b9211179101a8f3bf4947f93cb32b..0b51e70cba21930f4fbe82ed3a168b540f4e7ad6 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 9766e975635bafa886aa55e78e37a62ed0607d9a..de35de137c1e2c6f8d349e76d9f1b603cc3f8a71 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 13d42707706e11ac2d102ed1e9e75f5b8e469227..80bb06d09f8f1ee2921b55e68cfb544467fa06c6 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 3f7d2a0d79c8925862fff3e0b6167d8f25ba90bb..16a26a9cadde5ee72311ce946dca188584144e6f 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 36cffb7e59c81717cca1db5d380dd1940e68f000..ec4b8be154f74b3519a43922e834eb9cb693726b 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 daf1108de6c05159db0d92ade68ec9b724aec005..8a626071746007de80708a65a4867ae5bcd76c0d 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 7482fd27fd74c812d4f7c825fbfa40f08912ca22..59a282d47a3d21d810c15a22f6a41625ea979ce6 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 12112426a52f0e04e65be70ef0f6c6c1eb880f53..973a2e326c50444f4fc3ba5663c410a3b7a64c83 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 42e1ad147407904ec6b650760a3556f148b9db2b..ef1ee65866d97788d9b896400c9213a233b0b95e 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 3223de6d50ba6fb17b9dcf5e6e16cbf98fb61ad2..7838fe636920b059ed92e7067486cefe59f45eda 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 9f6168dcc9a5e92b35164120addc3adeb4bb02f7..53ce9fc3add0bb04ad3209b22c116e41e7f13093 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 49b0543c428a69df2f67918a0a871d52c6f411b8..03b15f9c862c59b38a55eaa33eb056710ff516c6 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
index 49b0543c428a69df2f67918a0a871d52c6f411b8..03b15f9c862c59b38a55eaa33eb056710ff516c6 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
index c03705c4cf4c88fecb78112efa5f35308c6aa614..97898f346f9ff2fe0826f7c78a7b5e2325d664ff 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 1adfb29a18108f461487273c013749d66cffb736..bc7a9170e298896d213109dabb696cb723ef22b5 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 c8d331edc7c550479e6c5fbd1dbb892f9789bb94..de414ac3045e2727df12b26b3cad26346c5c5d2e 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 cad4c41a492a588be98576c86e287205451fb83c..af979f21b344db5d5cd318119a04b6ec5c1c461e 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 ef2552990a1491d903742077e94d975fb4519e07..3dc445f2d177ba6fe95ee69e22490df538513c9f 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 e44f41c1996a57d9e12e6f7c86becdec64587faf..ef5acd7d55fefc8230e4299c9d43fb1cbc3e8f33 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 1c0d0332fa6028a385857033e928aa84ac84ee51..16d7ced41ac37da8405b3cbf1d1c9299b681ca19 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 9a26741265bbe2a4ff8713917c7430f6e12db4f1..5ccb318714b6fa3cb0d27345e822f3f4776db55c 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 32f5d86c99626cd7364507460b2d14078add2108..89bd9045ef4e175df909978a8c3e0526d1c5afbb 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 32f5d86c99626cd7364507460b2d14078add2108..89bd9045ef4e175df909978a8c3e0526d1c5afbb 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 afa63f7ba33e0979922bfdcfed8e37ce6e0e29a1..0d46e1f187d1cfeebf079af1068b1aae8052f8ec 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 3ad84cb6966ff8e0be24c1e57320cdc16f4a624d..6f5faa3091bb02cb1a94a2e6dd8ba4140925dc84 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 f854d7b49be46cdf62b315b95428029093d74556..dd216a8bc8dcc1b3341fcf0166aabe1a873a1f15 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 44d9f3c173f4765c975913345a70f92504e91329..066c297a322d95ae895cf9db57c62c5e0fc37b23 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 c545933f565de0de097c0df20e399148c16990cc..908867a4633686a97eca5e028daf39e799ad669c 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
index c545933f565de0de097c0df20e399148c16990cc..908867a4633686a97eca5e028daf39e799ad669c 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
index 68298283100daf32b9d4a9b96b461ac88a80906e..8779cbdeabdb30d88396e02d521f67a75371d43b 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 ee2348c85abb33d831fea492d0ada74b81bf9d28..7eba41bee98b9691c0772c621bf52ac8c4df5d6e 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 fadefe1f3e4dd1b22887eb41dd864ead6f18f3bc..cc0712eb47748ccb87924209327eb9fe6d566384 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 6ec0ed2c7c3b2513bc15bd5d47694adcc840bbba..40ddcec7016e605443a0431c71466a9d9eb1c189 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 863e5ba0a29c55b08fbb8ffefa3a5a95f70f9d04..403b4169c17c2a3f9477105a60fc523956d4ff16 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 9eb072c28e9e88766e62ba30e11221227be11cee..6930a9c474117bfbafdcf40a358677295068bc4a 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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
new file mode 100644
index 0000000000000000000000000000000000000000..758997853d3fa797090a6bc224280838b860190f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
@@ -0,0 +1,124 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+typedef unsigned int ino_t;
+typedef unsigned int gid_t;
+typedef unsigned int uid_t;
+typedef long time_t;
+typedef unsigned int blkcnt_t;
+typedef unsigned int blksize_t;
+typedef unsigned int dev_t;
+typedef unsigned int mode_t;
+typedef unsigned int nlink_t;
+typedef long off_t;
+struct stat {
+ dev_t st_dev ;
+ ino_t st_ino ;
+ mode_t st_mode ;
+ nlink_t st_nlink ;
+ uid_t st_uid ;
+ gid_t st_gid ;
+ dev_t st_rdev ;
+ off_t st_size ;
+ time_t st_atime ;
+ time_t st_mtime ;
+ time_t st_ctime ;
+ blksize_t st_blksize ;
+ blkcnt_t st_blocks ;
+ char *__fc_real_data ;
+ int __fc_real_data_max_size ;
+};
+struct __fc_FILE {
+ unsigned int __fc_stdio_id ;
+ unsigned int __fc_maxsz ;
+ unsigned int __fc_writepos ;
+ unsigned int __fc_readpos ;
+ int __fc_is_a_socket ;
+ int mode ;
+ struct stat *__fc_inode ;
+};
+typedef struct __fc_FILE FILE;
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+/*@ ghost extern size_t __memory_size; */
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+extern FILE *stdout;
+
+FILE fopen[2];
+FILE const *_p__fc_fopen = (FILE const *)(fopen);
+void __e_acsl_memory_init(void)
+{
+ __store_block((void *)(& stdout),8U);
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ FILE *f;
+ __e_acsl_memory_init();
+ __store_block((void *)(& f),8U);
+ __full_init((void *)(& f));
+ f = stdout;
+ /*@ assert f ≡ __fc_stdout; */
+ e_acsl_assert(f == stdout,(char *)"Assertion",(char *)"main",
+ (char *)"f == __fc_stdout",12);
+ __retres = 0;
+ __delete_block((void *)(& stdout));
+ __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
new file mode 100644
index 0000000000000000000000000000000000000000..758997853d3fa797090a6bc224280838b860190f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
@@ -0,0 +1,124 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+typedef unsigned int ino_t;
+typedef unsigned int gid_t;
+typedef unsigned int uid_t;
+typedef long time_t;
+typedef unsigned int blkcnt_t;
+typedef unsigned int blksize_t;
+typedef unsigned int dev_t;
+typedef unsigned int mode_t;
+typedef unsigned int nlink_t;
+typedef long off_t;
+struct stat {
+ dev_t st_dev ;
+ ino_t st_ino ;
+ mode_t st_mode ;
+ nlink_t st_nlink ;
+ uid_t st_uid ;
+ gid_t st_gid ;
+ dev_t st_rdev ;
+ off_t st_size ;
+ time_t st_atime ;
+ time_t st_mtime ;
+ time_t st_ctime ;
+ blksize_t st_blksize ;
+ blkcnt_t st_blocks ;
+ char *__fc_real_data ;
+ int __fc_real_data_max_size ;
+};
+struct __fc_FILE {
+ unsigned int __fc_stdio_id ;
+ unsigned int __fc_maxsz ;
+ unsigned int __fc_writepos ;
+ unsigned int __fc_readpos ;
+ int __fc_is_a_socket ;
+ int mode ;
+ struct stat *__fc_inode ;
+};
+typedef struct __fc_FILE FILE;
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+/*@ ghost extern size_t __memory_size; */
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+extern FILE *stdout;
+
+FILE fopen[2];
+FILE const *_p__fc_fopen = (FILE const *)(fopen);
+void __e_acsl_memory_init(void)
+{
+ __store_block((void *)(& stdout),8U);
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ FILE *f;
+ __e_acsl_memory_init();
+ __store_block((void *)(& f),8U);
+ __full_init((void *)(& f));
+ f = stdout;
+ /*@ assert f ≡ __fc_stdout; */
+ e_acsl_assert(f == stdout,(char *)"Assertion",(char *)"main",
+ (char *)"f == __fc_stdout",12);
+ __retres = 0;
+ __delete_block((void *)(& stdout));
+ __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 6db54aa859e440e04b04ac9a53e236aa6b15b96d..e0bcf266375e61b45e0761d8057e620fece9d0cc 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 b52f58679e5d7326aaba30891ae6cfb041a92c21..63a290eedce70a643c78c3c7477170ca0ec263da 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 8e1101b3c274577c907db2076ca18e7e38f7b5a9..16f0e40ddaa2cb38d46d33e745e1151000cca6ab 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 8e1101b3c274577c907db2076ca18e7e38f7b5a9..16f0e40ddaa2cb38d46d33e745e1151000cca6ab 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 eecf507b2d7032218855b88f1b129b41d47ab47d..b09462117d47200e66d5f4b9bdc3d4bf246d78fb 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 624b42cfe889dfe466c516ebfd8043e14d2f0843..7d7245dcaef0aa43deb5a2b12df07e0a9139b7a4 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 6b7354a356dbad21526e2603c23c3dbc97711008..d43659faf504d642b77700977e78bdccd06b3fa8 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index 6b7354a356dbad21526e2603c23c3dbc97711008..d43659faf504d642b77700977e78bdccd06b3fa8 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
index 6ac30ce1b033b4095f82841be1a55714702d13c9..8187bd9b1d2f9fbd39fecd5029acce36e6255f0f 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
index 1321097141898e1b21435751b8d4bca0d446aad1..563cb72ec73a08b103263ae86e737db215e36c01 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index 4cebebc641f25d981295e83f1bee48f31ec27b82..dc069fd655e5152e874bf9b44cd7f002dfa88959 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 4cebebc641f25d981295e83f1bee48f31ec27b82..dc069fd655e5152e874bf9b44cd7f002dfa88959 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 6a4bba4d5230101329af954584c32a06347ae2dd..94f13e139d47763a7d18af90405ad462d1e168c5 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
index e7645e29a7488e9c4f185cf8088f6504b80c3938..5db867a9f768aec03c2a9d22a31c86ac8da34cf1 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 __fc_random_counter __attribute__((__unused__));
-unsigned long const __fc_rand_max = (unsigned long)32767;
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
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 68a3330749b00729a88372ea06a7dc26012379c5..d6281b63bea04dff9df5524a9ee78d99a8c61e48 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 23b4644573992c31cf5f4f12380360143771e128..fbea9e275c7c34bae03029acb5e154d952c80538 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 16212ce0bec648565abd76c33808760baf0c2f57..af4ebcce6827413073520995f5fcc4d40e1db9ef 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 e4b40084976d99596f202dda111d53e286e3b062..4d516552be268606d3d61f2688e4c3c510f1907b 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 21a8c8b0bb9f199c9d303e4bf5ac5b0bb278baa1..1f4ffe1bebb65a79a479d24ffbe2e6242c3dda17 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 248c8af9cc25e4e62f67acc9d499ca1fa27da417..4980d9600744c14bbee8e0db5024b578cd23ec53 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 1b0901c56609ef43399ba5ad7cb93f72f922a39e..66f81f4d6bd3786c877dcdaa5582ff2d55d1d7c6 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 2d59ce2eeda28b2688a5c477da19e00cd86beccc..46bacb15a6b8c6be1b87352e59994a0ba543794f 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 4f06836f4be2a9ef0457600c05a969874d05cf8f..8f9966c9c1e6adef8ffeb800fa9f3b050307c8bb 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 c1ab49ed8ffb0793fa524787176f4d5bf15b5fad..96541df2fae63dbb503c77e829cbe01303350fd5 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
@@ -13,8 +13,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
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 f5797a4e813bd0fd187dcceaac5e20379be9bb7d..acfabfbe6620bb9181920007600468918e1590c1 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 4fe509716ad4246e86b14c301e30660601419e0e..85256158819af01d42b662c61ec40a85f7146bab 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 ef3bee7f9acc88ee19e645dfe2e3cfb4ca1f005c..bb7f7e8f18c8bbbf3dcee5bf2785b2de4e87ab4b 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 303b4b0c0e5fcf15a3902b284975d02567891527..2fb1e73b1fe2639ed1cc741af4bf3b96cc698f79 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 99fcc322383457f34bf3adee78ca56947d7d93e5..505188204524b3c7dbdb7f32b4eaba19ad80624e 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
@@ -24,8 +24,8 @@ FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `logic functio
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 621041c743d95e0a8a598a6e148f17b6df6c8785..9ce9941b7a43253e99e9ebd14d040f0ad2a47761 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
@@ -20,8 +20,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
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 0bb3ff7fee2ed8ac69778643a7157d86dbe60f27..4bfb1336228fb11437033f3215b04a9a2371aa3d 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 bd910bdf9b8fd1e09ee6ff04ea257c5469093a5f..eeebc509279c543216726456fd5d2bf445dbeeb0 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 2a29c1cd0354dd569bcb1a9da578856913c60b74..d49790719a93844e353234871036dedeee740b74 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 24c9085a67a4fc88d2a77ec050da9719d71324a9..222fcd185325e0c4c2c2715d7510eccabe6bd8de 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 b62c74b7930ff3a1b597d50dddc7f3d454617949..a1629852a0598bc60de3f30a72a4557c6d75a5f9 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 e5c231612712bc11898fb226864c4ad6769989f8..3dd3d4c464229d642ccdf4d018e7c601954922a4 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 75d68e3a4aefcd82ea5d87475710c7dbbe36ed6e..c252659bc4c22b3456ba99a57354b7aaf59a3a6e 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 40316cdce210326a7e449a7cff78d172479c8bb1..a16eedd64425d25b048d951aedbdd8f0a53676d3 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 f166bba7846f0c090951a4f278f7b03169aa5ac7..ede072768943a102d923d81524744bb382843d72 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 f166bba7846f0c090951a4f278f7b03169aa5ac7..ede072768943a102d923d81524744bb382843d72 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 938fb1d7d7f85f44486a7982f6b496736c945daf..02930c8750c9cac273e36941031ceac564253b87 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 2042277c0a8f2050732e392876722383565c2091..faaa5173ff1d114fa35954d14571500a471e2a34 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 570841204e644f448415a83ddbc8340a9b9241be..7723a2ff42a843ef11e82e649bfb7cbf19dfc68d 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 d26ad81d9108493fb59c530f9dd7f96f189538f7..0579223fec6caa5eb40693d5e055fa53cce48b1d 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 dddad854902f5146264a1b493a0df256bf9a8b93..68e6ea08da09356a4048325150f90a92f6961872 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
@@ -24,8 +24,8 @@ FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `logic functio
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 e561d2dc01d8723837c2e86ba0860c574a3eee96..c7d1ad4854cd2b1f1389a515319e58139fb6e2d4 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
@@ -20,8 +20,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
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 a8899867a2d03c6015292a3b4ed5c1556dae17f2..7e58babf3c65623ea4b18785696c358e8a9e21f9 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 330bd859fb7f8cf3ce923f84646cfa6fc1efbfd5..a4fb1b9c644f38c681160f46ab54d1bf1194fcf7 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 0c215a823fdec5dee5016e7a2aeb43f740ed223d..b2a6b735ac1d37a72109c401619f7e2b691ef55d 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 013d4c42c5cef6285f71387f469fa20d3f1875ce..f467ad1814ae6780dcec2934f6717339ca4907e7 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 84272cb7240f9c96659296ac178275838b399759..ff5150c54ab5fd2cea9682757917f0d5bab8470b 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 f4b58164d5ef75c5651ee8ea7ceb7309d514f8c2..454c8a8c574692be497473a00a8665e35c9b17b6 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
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
new file mode 100644
index 0000000000000000000000000000000000000000..1bd7d9fc259b6444e9d607dcfeba1847d721814a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
@@ -0,0 +1,63 @@
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD tests/e-acsl-runtime/stdout.c"
+[e-acsl] beginning translation.
+[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_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+ stdout ∈ {{ NULL ; &S___fc_stdout }}
+ fopen[0..1] ∈ {0}
+ _p__fc_fopen ∈ {{ &fopen }}
+ S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
+ [--..--]
+ [0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
+ [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
+ [--..--]
+ [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
+ S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks} ∈
+ [--..--]
+ [0].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_0_S___fc_inode_0_S___fc_stdout }}
+ {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈
+ [--..--]
+ [1].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_1_S___fc_inode_0_S___fc_stdout }}
+ [1].__fc_real_data_max_size ∈ [--..--]
+ S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_inode_1_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks} ∈
+ [--..--]
+ [0].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_0_S___fc_inode_1_S___fc_stdout }}
+ {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈
+ [--..--]
+ [1].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_1_S___fc_inode_1_S___fc_stdout }}
+ [1].__fc_real_data_max_size ∈ [--..--]
+ S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_real_data_1_S___fc_inode_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 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
+[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
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
new file mode 100644
index 0000000000000000000000000000000000000000..1bd7d9fc259b6444e9d607dcfeba1847d721814a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
@@ -0,0 +1,63 @@
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -dD tests/e-acsl-runtime/stdout.c"
+[e-acsl] beginning translation.
+[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_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+ stdout ∈ {{ NULL ; &S___fc_stdout }}
+ fopen[0..1] ∈ {0}
+ _p__fc_fopen ∈ {{ &fopen }}
+ S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
+ [--..--]
+ [0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
+ [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
+ [--..--]
+ [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
+ S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks} ∈
+ [--..--]
+ [0].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_0_S___fc_inode_0_S___fc_stdout }}
+ {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈
+ [--..--]
+ [1].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_1_S___fc_inode_0_S___fc_stdout }}
+ [1].__fc_real_data_max_size ∈ [--..--]
+ S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_inode_1_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks} ∈
+ [--..--]
+ [0].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_0_S___fc_inode_1_S___fc_stdout }}
+ {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈
+ [--..--]
+ [1].__fc_real_data ∈
+ {{ NULL ;
+ &S___fc_real_data_1_S___fc_inode_1_S___fc_stdout }}
+ [1].__fc_real_data_max_size ∈ [--..--]
+ S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_real_data_1_S___fc_inode_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 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
+[value] ====== VALUES COMPUTED ======
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 ca3b93ba6a8d9084a045a60cb7479bbab0ac9cc8..ef38527a9d36508d8d3d2437a691a18e1d99f4a7 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 525695a8f824d26a67473e76d81e0b438f9c0454..52a40dc10ac92369ebdd6e84ec51558075cae2b8 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 27bf58526758d8c8854d9eae97a5493e17af681b..ef1e58080e4724279bc1ddc51a1e081068e1372d 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 27bf58526758d8c8854d9eae97a5493e17af681b..ef1e58080e4724279bc1ddc51a1e081068e1372d 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 decf200de851cb36b927f3e11acd0c03045f79e8..9b2187cb4ff019880f69e83564c50bafa6c7301b 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 7d4f021a945a485ac35581c92638f1117cc43513..ba4417a3682a3e527e82368261fb92aa67ce3dc3 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
@@ -10,8 +10,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 310a54b035b39782c4aca0d5b3f732ddff693d1d..c0b07db75bbe02f5d88f9d2339b149c0844a5c33 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
@@ -34,8 +34,8 @@ FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 6636c868d96a0e6a477594c08c71e5be32d7b67e..c5011899f7ea1956df5c88631da821864348817c 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
@@ -26,8 +26,8 @@ FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 a04137bd4fb48ebb20d7345d766ae34b9fa2c3aa..6aa84685b5108e5ff01f82bb5babfb1c87718786 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
@@ -34,8 +34,8 @@ FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 9a2feea64ed8a6887c23a5ba89e5c54a231a42ff..0dd840891cea6f06eb66f8d9192a2e4ef8e37d9d 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
@@ -26,8 +26,8 @@ FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 041424bba5380c5114d59f4eb169e26498901a2c..db2c30fd5958e3be88defd9282d575a8685a3657 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
@@ -11,8 +11,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 041424bba5380c5114d59f4eb169e26498901a2c..db2c30fd5958e3be88defd9282d575a8685a3657 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
@@ -11,8 +11,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 d4f48f1b4511f6838d22865a895e80de781e5cb1..eeb367bf19d92c01c028cfb6b5f0110255d0e8e9 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
@@ -34,8 +34,8 @@ FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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 1e433e7dfcad4ede8881f89a3c17dd44130d00fb..2ca60b8b32bd6d26628d34c5064deea17511d310 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
@@ -26,8 +26,8 @@ FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- __fc_random_counter ∈ {0}
- __fc_rand_max ∈ {32767}
+ random_counter ∈ {0}
+ 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
new file mode 100644
index 0000000000000000000000000000000000000000..7078d0e56a746f0c6476dca4c76c612dfd7d82fe
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c
@@ -0,0 +1,13 @@
+/* run.config
+ COMMENT: __fc_stdout
+ 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_test.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_test.sh stdout2
+*/
+
+#include<stdio.h>
+
+int main(){
+ FILE *f = stdout;
+ //@ assert f == stdout;
+}