From 361a4fa8bea76e9397d0b50fb08674ca2c4ae236 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 8 Jul 2014 02:27:11 +0200
Subject: [PATCH] fix bug when using Frama-C-specific names of the libc which
prevent linking the generated code
---
src/plugins/e-acsl/doc/Changelog | 2 +
src/plugins/e-acsl/main.ml | 33 ++++-
.../e-acsl-runtime/oracle/addrOf.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/addrOf.res.oracle | 4 +-
.../e-acsl-runtime/oracle/alias.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/alias.res.oracle | 4 +-
.../e-acsl-runtime/oracle/arith.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/arith.res.oracle | 4 +-
.../e-acsl-runtime/oracle/array.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/array.res.oracle | 4 +-
.../e-acsl-runtime/oracle/at.1.res.oracle | 4 +-
.../tests/e-acsl-runtime/oracle/at.res.oracle | 4 +-
.../oracle/bts1304.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/bts1304.res.oracle | 4 +-
.../oracle/bts1307.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/bts1307.res.oracle | 4 +-
.../oracle/bts1324.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/bts1324.res.oracle | 4 +-
.../oracle/bts1326.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/bts1326.res.oracle | 4 +-
.../oracle/bts1390.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/bts1390.res.oracle | 4 +-
.../oracle/bts1398.1.res.oracle | 10 +-
.../e-acsl-runtime/oracle/bts1398.res.oracle | 10 +-
.../oracle/bts1399.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/bts1399.res.oracle | 4 +-
.../oracle/bts1478.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/bts1478.res.oracle | 4 +-
.../oracle/bts1700.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/bts1700.res.oracle | 4 +-
.../oracle/bts1717.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/bts1717.res.oracle | 4 +-
.../e-acsl-runtime/oracle/call.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/call.res.oracle | 4 +-
.../e-acsl-runtime/oracle/cast.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/cast.res.oracle | 4 +-
.../oracle/comparison.1.res.oracle | 4 +-
.../oracle/comparison.res.oracle | 4 +-
.../e-acsl-runtime/oracle/empty.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/empty.res.oracle | 4 +-
.../e-acsl-runtime/oracle/false.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/false.res.oracle | 4 +-
.../oracle/function_contract.1.res.oracle | 4 +-
.../oracle/function_contract.res.oracle | 4 +-
.../tests/e-acsl-runtime/oracle/gen_addrOf.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_addrOf2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_alias.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_alias2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_arith.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_arith2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_array.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_array2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_at.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_at2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_bts1304.c | 4 +-
.../e-acsl-runtime/oracle/gen_bts13042.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_bts1307.c | 4 +-
.../e-acsl-runtime/oracle/gen_bts13072.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_bts1324.c | 4 +-
.../e-acsl-runtime/oracle/gen_bts13242.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_bts1326.c | 4 +-
.../e-acsl-runtime/oracle/gen_bts13262.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_bts1390.c | 4 +-
.../e-acsl-runtime/oracle/gen_bts13902.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_bts1398.c | 10 +-
.../e-acsl-runtime/oracle/gen_bts13982.c | 10 +-
.../tests/e-acsl-runtime/oracle/gen_bts1399.c | 4 +-
.../e-acsl-runtime/oracle/gen_bts13992.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_bts1478.c | 4 +-
.../e-acsl-runtime/oracle/gen_bts14782.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_bts1700.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_bts1717.c | 4 +-
.../e-acsl-runtime/oracle/gen_bts17172.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_call.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_call2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_cast.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_cast2.c | 4 +-
.../e-acsl-runtime/oracle/gen_comparison.c | 4 +-
.../e-acsl-runtime/oracle/gen_comparison2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_false.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_false2.c | 4 +-
.../oracle/gen_function_contract.c | 4 +-
.../oracle/gen_function_contract2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_ghost.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_ghost2.c | 4 +-
.../oracle/gen_integer_constant.c | 4 +-
.../oracle/gen_integer_constant2.c | 4 +-
.../e-acsl-runtime/oracle/gen_invariant.c | 4 +-
.../e-acsl-runtime/oracle/gen_invariant2.c | 4 +-
.../e-acsl-runtime/oracle/gen_labeled_stmt.c | 4 +-
.../e-acsl-runtime/oracle/gen_labeled_stmt2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_lazy.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_lazy2.c | 4 +-
.../e-acsl-runtime/oracle/gen_linear_search.c | 4 +-
.../oracle/gen_linear_search2.c | 4 +-
.../oracle/gen_literal_string.c | 4 +-
.../oracle/gen_literal_string2.c | 4 +-
.../e-acsl-runtime/oracle/gen_localvar.c | 4 +-
.../e-acsl-runtime/oracle/gen_localvar2.c | 4 +-
.../e-acsl-runtime/oracle/gen_longlong.c | 4 +-
.../e-acsl-runtime/oracle/gen_longlong2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_loop.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_loop2.c | 4 +-
.../oracle/gen_nested_code_annot.c | 4 +-
.../oracle/gen_nested_code_annot2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_not.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_not2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_null.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_null2.c | 4 +-
.../oracle/gen_other_constants.c | 4 +-
.../oracle/gen_other_constants2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_ptr.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_ptr2.c | 4 +-
.../e-acsl-runtime/oracle/gen_ptr_init.c | 4 +-
.../e-acsl-runtime/oracle/gen_ptr_init2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_quantif.c | 4 +-
.../e-acsl-runtime/oracle/gen_quantif2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_result.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_result2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_sizeof.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_sizeof2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_stdout.c | 124 ++++++++++++++++++
.../tests/e-acsl-runtime/oracle/gen_stdout2.c | 124 ++++++++++++++++++
.../e-acsl-runtime/oracle/gen_stmt_contract.c | 4 +-
.../oracle/gen_stmt_contract2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_true.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_true2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_typedef.c | 4 +-
.../e-acsl-runtime/oracle/gen_typedef2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_valid.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_valid2.c | 4 +-
.../e-acsl-runtime/oracle/gen_valid_alias.c | 4 +-
.../e-acsl-runtime/oracle/gen_valid_alias2.c | 4 +-
.../oracle/gen_valid_in_contract.c | 4 +-
.../oracle/gen_valid_in_contract2.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_vector.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_vector2.c | 4 +-
.../e-acsl-runtime/oracle/ghost.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/ghost.res.oracle | 4 +-
.../oracle/integer_constant.1.res.oracle | 4 +-
.../oracle/integer_constant.res.oracle | 4 +-
.../oracle/invariant.1.res.oracle | 4 +-
.../oracle/invariant.res.oracle | 4 +-
.../oracle/labeled_stmt.1.res.oracle | 4 +-
.../oracle/labeled_stmt.res.oracle | 4 +-
.../e-acsl-runtime/oracle/lazy.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/lazy.res.oracle | 4 +-
.../oracle/linear_search.1.res.oracle | 4 +-
.../oracle/linear_search.res.oracle | 4 +-
.../oracle/literal_string.1.res.oracle | 4 +-
.../oracle/literal_string.res.oracle | 4 +-
.../oracle/localvar.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/localvar.res.oracle | 4 +-
.../oracle/longlong.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/longlong.res.oracle | 4 +-
.../e-acsl-runtime/oracle/loop.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/loop.res.oracle | 4 +-
.../oracle/nested_code_annot.1.res.oracle | 4 +-
.../oracle/nested_code_annot.res.oracle | 4 +-
.../e-acsl-runtime/oracle/not.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/not.res.oracle | 4 +-
.../e-acsl-runtime/oracle/null.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/null.res.oracle | 4 +-
.../oracle/other_constants.1.res.oracle | 4 +-
.../oracle/other_constants.res.oracle | 4 +-
.../e-acsl-runtime/oracle/ptr.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/ptr.res.oracle | 4 +-
.../oracle/ptr_init.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/ptr_init.res.oracle | 4 +-
.../oracle/quantif.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/quantif.res.oracle | 4 +-
.../e-acsl-runtime/oracle/result.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/result.res.oracle | 4 +-
.../e-acsl-runtime/oracle/sizeof.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/sizeof.res.oracle | 4 +-
.../e-acsl-runtime/oracle/stdout.1.err.oracle | 0
.../e-acsl-runtime/oracle/stdout.1.res.oracle | 63 +++++++++
.../e-acsl-runtime/oracle/stdout.err.oracle | 0
.../e-acsl-runtime/oracle/stdout.res.oracle | 63 +++++++++
.../oracle/stmt_contract.1.res.oracle | 4 +-
.../oracle/stmt_contract.res.oracle | 4 +-
.../e-acsl-runtime/oracle/true.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/true.res.oracle | 4 +-
.../oracle/typedef.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/typedef.res.oracle | 4 +-
.../e-acsl-runtime/oracle/valid.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/valid.res.oracle | 4 +-
.../oracle/valid_alias.1.res.oracle | 4 +-
.../oracle/valid_alias.res.oracle | 4 +-
.../oracle/valid_in_contract.1.res.oracle | 4 +-
.../oracle/valid_in_contract.res.oracle | 4 +-
.../e-acsl-runtime/oracle/vector.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/vector.res.oracle | 4 +-
.../e-acsl/tests/e-acsl-runtime/stdout.c | 13 ++
194 files changed, 802 insertions(+), 384 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 628dd97bbb5..7210380aca5 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 3b41b48dd89..a798b1ccb13 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 6eeca12deee..3d10cb740c7 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 6eeca12deee..3d10cb740c7 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 ebbeaef53da..beb597a0134 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 ebbeaef53da..beb597a0134 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 8d0c810c622..78ee7781191 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 9d33b17f15c..0cdf4bac191 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 c4cd42d3ae3..454b7b14a1c 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 4c3f47d2031..34280485ca0 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 d4a2472d1c5..5294f75d2b3 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 4f19c71c8d4..132bc9553b5 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 0b17e914e6e..a461761af12 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 0b17e914e6e..a461761af12 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 29bb832ec0d..9da17af23eb 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 464bfd42cf6..49e77bc0169 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 a4c946ba598..843698257a8 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 488866b8fa5..447c838d1e5 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 b81f489bed1..ac2e364690f 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 856636dcb07..eb9277270dd 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 bd257da45df..f8ad3751c31 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 ef41ce84058..45b009a5047 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 877d15f251e..af5dc40fc73 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 877d15f251e..af5dc40fc73 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 b072fd28208..b634bce4966 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 21a68ed1510..8cfdc8dc491 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 5d373286f97..44f5c5647e5 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 0d9154cd481..76d0e9b7e0a 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 74bbf857adb..71cc1729670 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 74bbf857adb..71cc1729670 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 b04cc71f532..f0036c5d770 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 b04cc71f532..f0036c5d770 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 5abe18e2131..2922e483dde 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 a2a8d96b0bd..a873c96d7ec 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 20ae38c9e7f..8a954fea71f 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 cfb947c60f7..b8abbec8223 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 f86e56173df..fce50ae2277 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 e77b42acb2e..c5a32de2206 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 38ce731e0a0..a64cb680946 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 38ce731e0a0..a64cb680946 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 dbb2932fc8d..7610e778e93 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 dbb2932fc8d..7610e778e93 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 e09ec22fd91..a2ff92e8e24 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 874df546bf0..eb34979bf18 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 78d13f82b67..fab581fe35d 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 78d13f82b67..fab581fe35d 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 21d3dee0e0f..3595848a662 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 21d3dee0e0f..3595848a662 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 8247aa4992b..474a027f305 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 82008631711..8e826c19967 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 c765bd1a860..426291f1f93 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 bf258eef4aa..3465af736a5 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 a325b760622..a86d2c65f52 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 c69173bbeae..fbad827ab06 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 efdb482b820..45945925656 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 efdb482b820..45945925656 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 31a9781a100..a3882707f84 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 3b4af93775d..f2953f32515 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 560261c0f55..97c05e9203a 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 89edfb78504..669dbe87e7b 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 eb2080fc217..d0e407c5451 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 8c3ebbe9970..50e0edfc00c 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 2b98891e4a7..17b721b9dd2 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 b4ea1d9be57..27a2a4a4de8 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 f09bf2f1116..7cb3e53d8fe 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 f09bf2f1116..7cb3e53d8fe 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 45a8c5865d8..d4a592d8a9f 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 9b75f0ffe84..3074489280d 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 d9defb9f390..356c8305d69 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 2f525371491..0e3f2d02f3d 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 7258ddac41b..bd982bc4f57 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 87cc310d9af..58a1bbf0c1a 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 87cc310d9af..58a1bbf0c1a 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 4287e8ff271..c16bdde76b0 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 4287e8ff271..c16bdde76b0 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 aa39b2d317a..d802950c13e 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 291d9b6fdc6..ef9d9264b5f 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 ceb5d2b3fa7..dc712b9c16d 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 57592073380..d7ab417d961 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 0acbead3158..5c50649668f 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 0acbead3158..5c50649668f 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 4ff593abac4..78ffa12f7d1 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 18ed30062a9..9a70717d351 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 c8f1be53be9..8ab2658f325 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 d117e37824f..0b1470d48fd 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 596b7b58c76..5b40837b516 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 24f06299028..0b51e70cba2 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 9766e975635..de35de137c1 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 13d42707706..80bb06d09f8 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 3f7d2a0d79c..16a26a9cadd 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 36cffb7e59c..ec4b8be154f 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 daf1108de6c..8a626071746 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 7482fd27fd7..59a282d47a3 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 12112426a52..973a2e326c5 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 42e1ad14740..ef1ee65866d 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 3223de6d50b..7838fe63692 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 9f6168dcc9a..53ce9fc3add 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 49b0543c428..03b15f9c862 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 49b0543c428..03b15f9c862 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 c03705c4cf4..97898f346f9 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 1adfb29a181..bc7a9170e29 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 c8d331edc7c..de414ac3045 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 cad4c41a492..af979f21b34 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 ef2552990a1..3dc445f2d17 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 e44f41c1996..ef5acd7d55f 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 1c0d0332fa6..16d7ced41ac 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 9a26741265b..5ccb318714b 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 32f5d86c996..89bd9045ef4 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 32f5d86c996..89bd9045ef4 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 afa63f7ba33..0d46e1f187d 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 3ad84cb6966..6f5faa3091b 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 f854d7b49be..dd216a8bc8d 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 44d9f3c173f..066c297a322 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 c545933f565..908867a4633 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 c545933f565..908867a4633 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 68298283100..8779cbdeabd 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 ee2348c85ab..7eba41bee98 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 fadefe1f3e4..cc0712eb477 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 6ec0ed2c7c3..40ddcec7016 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 863e5ba0a29..403b4169c17 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 9eb072c28e9..6930a9c4741 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 00000000000..758997853d3
--- /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 00000000000..758997853d3
--- /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 6db54aa859e..e0bcf266375 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 b52f58679e5..63a290eedce 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 8e1101b3c27..16f0e40ddaa 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 8e1101b3c27..16f0e40ddaa 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 eecf507b2d7..b09462117d4 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 624b42cfe88..7d7245dcaef 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 6b7354a356d..d43659faf50 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 6b7354a356d..d43659faf50 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 6ac30ce1b03..8187bd9b1d2 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 13210971418..563cb72ec73 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 4cebebc641f..dc069fd655e 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 4cebebc641f..dc069fd655e 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 6a4bba4d523..94f13e139d4 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 e7645e29a74..5db867a9f76 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 68a3330749b..d6281b63bea 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 23b46445739..fbea9e275c7 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 16212ce0bec..af4ebcce682 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 e4b40084976..4d516552be2 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 21a8c8b0bb9..1f4ffe1bebb 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 248c8af9cc2..4980d960074 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 1b0901c5660..66f81f4d6bd 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 2d59ce2eeda..46bacb15a6b 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 4f06836f4be..8f9966c9c1e 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 c1ab49ed8ff..96541df2fae 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 f5797a4e813..acfabfbe662 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 4fe509716ad..85256158819 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 ef3bee7f9ac..bb7f7e8f18c 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 303b4b0c0e5..2fb1e73b1fe 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 99fcc322383..50518820452 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 621041c743d..9ce9941b7a4 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 0bb3ff7fee2..4bfb1336228 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 bd910bdf9b8..eeebc509279 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 2a29c1cd035..d49790719a9 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 24c9085a67a..222fcd18532 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 b62c74b7930..a1629852a05 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 e5c23161271..3dd3d4c4642 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 75d68e3a4ae..c252659bc4c 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 40316cdce21..a16eedd6442 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 f166bba7846..ede07276894 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 f166bba7846..ede07276894 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 938fb1d7d7f..02930c8750c 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 2042277c0a8..faaa5173ff1 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 570841204e6..7723a2ff42a 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 d26ad81d910..0579223fec6 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 dddad854902..68e6ea08da0 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 e561d2dc01d..c7d1ad4854c 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 a8899867a2d..7e58babf3c6 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 330bd859fb7..a4fb1b9c644 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 0c215a823fd..b2a6b735ac1 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 013d4c42c5c..f467ad1814a 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 84272cb7240..ff5150c54ab 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 f4b58164d5e..454c8a8c574 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 00000000000..e69de29bb2d
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 00000000000..1bd7d9fc259
--- /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 00000000000..e69de29bb2d
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 00000000000..1bd7d9fc259
--- /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 ca3b93ba6a8..ef38527a9d3 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 525695a8f82..52a40dc10ac 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 27bf5852675..ef1e58080e4 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 27bf5852675..ef1e58080e4 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 decf200de85..9b2187cb4ff 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 7d4f021a945..ba4417a3682 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 310a54b035b..c0b07db75bb 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 6636c868d96..c5011899f7e 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 a04137bd4fb..6aa84685b51 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 9a2feea64ed..0dd840891ce 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 041424bba53..db2c30fd595 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 041424bba53..db2c30fd595 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 d4f48f1b451..eeb367bf19d 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 1e433e7dfca..2ca60b8b32b 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 00000000000..7078d0e56a7
--- /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;
+}
--
GitLab