From 0bf19f5e46a9848e1321ef4bffad995abebe7dfa Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 28 Apr 2015 14:15:24 +0200
Subject: [PATCH] [tests] cherry-picked hack for fopen
---
src/plugins/e-acsl/doc/Changelog | 1 +
src/plugins/e-acsl/main.ml | 7 ++-
.../tests/bts/oracle/bts1304.0.res.oracle | 4 +-
.../tests/bts/oracle/bts1304.1.res.oracle | 4 +-
.../tests/bts/oracle/bts1304.res.oracle | 4 +-
.../tests/bts/oracle/bts1307.0.res.oracle | 4 +-
.../tests/bts/oracle/bts1307.1.res.oracle | 4 +-
.../tests/bts/oracle/bts1307.res.oracle | 4 +-
.../tests/bts/oracle/bts1324.0.res.oracle | 4 +-
.../tests/bts/oracle/bts1324.1.res.oracle | 4 +-
.../tests/bts/oracle/bts1324.res.oracle | 4 +-
.../tests/bts/oracle/bts1326.0.res.oracle | 4 +-
.../tests/bts/oracle/bts1326.1.res.oracle | 4 +-
.../tests/bts/oracle/bts1326.res.oracle | 4 +-
.../tests/bts/oracle/bts1390.0.res.oracle | 4 +-
.../tests/bts/oracle/bts1390.1.res.oracle | 4 +-
.../tests/bts/oracle/bts1390.res.oracle | 4 +-
.../tests/bts/oracle/bts1398.0.res.oracle | 8 +--
.../tests/bts/oracle/bts1398.1.res.oracle | 8 +--
.../tests/bts/oracle/bts1398.res.oracle | 8 +--
.../tests/bts/oracle/bts1399.0.res.oracle | 4 +-
.../tests/bts/oracle/bts1399.1.res.oracle | 4 +-
.../tests/bts/oracle/bts1399.res.oracle | 4 +-
.../tests/bts/oracle/bts1478.0.res.oracle | 4 +-
.../tests/bts/oracle/bts1478.1.res.oracle | 4 +-
.../tests/bts/oracle/bts1478.res.oracle | 4 +-
.../tests/bts/oracle/bts1700.0.res.oracle | 4 +-
.../tests/bts/oracle/bts1700.1.res.oracle | 4 +-
.../tests/bts/oracle/bts1700.res.oracle | 4 +-
.../tests/bts/oracle/bts1717.0.res.oracle | 4 +-
.../tests/bts/oracle/bts1717.1.res.oracle | 4 +-
.../tests/bts/oracle/bts1717.res.oracle | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts1304.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts13042.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts1307.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts13072.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts1324.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts13242.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts1326.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts13262.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts1390.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts13902.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts1398.c | 8 +--
.../e-acsl/tests/bts/oracle/gen_bts13982.c | 8 +--
.../e-acsl/tests/bts/oracle/gen_bts1399.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts13992.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts1478.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts14782.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts1700.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts1717.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts17172.c | 4 +-
.../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 +-
.../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_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 +-
.../tests/e-acsl-runtime/oracle/gen_init.c | 4 +-
.../tests/e-acsl-runtime/oracle/gen_init2.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 +-
.../e-acsl-runtime/oracle/gen_mainargs.c | 4 +-
.../e-acsl-runtime/oracle/gen_mainargs2.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 | 51 ++++++++++++++--
.../tests/e-acsl-runtime/oracle/gen_stdout2.c | 58 +++++++++++++++++--
.../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 +-
.../e-acsl-runtime/oracle/init.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/init.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/mainargs.1.res.oracle | 4 +-
.../e-acsl-runtime/oracle/mainargs.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.res.oracle | 22 +++++--
.../e-acsl-runtime/oracle/stdout.res.oracle | 22 +++++--
.../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 | 3 +-
210 files changed, 554 insertions(+), 442 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index af4b444dc68..bba0ff9f020 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,7 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2015/04/28] Fix bug when using fopen.
o E-ACSL [2014/12/17] Export a minimal API for other plug-ins.
-* E-ACSL [2014/10/27] Add a missing cast when translating an integral
type used in a floating point/real context in an annotation.
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index 6f14f3ff9c8..a584ede0c19 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -218,11 +218,12 @@ let change_printer =
let pp () = object
inherit (Printer.extensible_printer ()) as super
method !varinfo fmt vi =
- if not vi.Cil_types.vghost then
+ if vi.Cil_types.vghost || vi.Cil_types.vstorage <> Cil_types.Extern
+ then
+ super#varinfo fmt vi
+ else
let s = Str.replace_first r "" vi.Cil_types.vname in
Format.fprintf fmt "%s" s
- else
- super#varinfo fmt vi
end in
Printer.change_printer pp
end
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
index f4cf8ba21c7..6c989f972cd 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
index f4cf8ba21c7..6c989f972cd 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
index f4cf8ba21c7..6c989f972cd 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
index 2a6424a798c..ec68e5b9442 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
@@ -8,8 +8,8 @@ tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
index df325fe187b..6291429ab43 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
@@ -8,8 +8,8 @@ tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
index 2a6424a798c..ec68e5b9442 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
@@ -8,8 +8,8 @@ tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
index 36fc1092d18..77eafde3d46 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
index c7976205437..9d10a4d5f85 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
index 36fc1092d18..77eafde3d46 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
index 7583cbd29fd..ec79b9e70c9 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
index 0a2e472a6f0..7b216576b83 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
index 7583cbd29fd..ec79b9e70c9 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
index c98c0cb1cdd..617549275c1 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
index 59bc686a665..6cff7458703 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
index c98c0cb1cdd..617549275c1 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
index 1b7e2835fd5..e8aef1cfbc2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
@@ -4,15 +4,15 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
- fopen[0..511] ∈ {0}
- _p__fc_fopen ∈ {{ &fopen[0] }}
+ __fc_fopen[0..511] ∈ {0}
+ _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
[--..--]
[0].[bits 80 to 95] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
index 1b7e2835fd5..e8aef1cfbc2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
@@ -4,15 +4,15 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
- fopen[0..511] ∈ {0}
- _p__fc_fopen ∈ {{ &fopen[0] }}
+ __fc_fopen[0..511] ∈ {0}
+ _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
[--..--]
[0].[bits 80 to 95] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
index 1b7e2835fd5..e8aef1cfbc2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
@@ -4,15 +4,15 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
- fopen[0..511] ∈ {0}
- _p__fc_fopen ∈ {{ &fopen[0] }}
+ __fc_fopen[0..511] ∈ {0}
+ _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
[--..--]
[0].[bits 80 to 95] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
index b07e6a38955..03deca85384 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
@@ -19,8 +19,8 @@ FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
index 4d1df873684..ca19d80fd5e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
@@ -27,8 +27,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
index 45341f00fdc..98e36f797bf 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
@@ -19,8 +19,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
index aa1818323b8..615a1182b18 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
index c71bbdb36d4..ca69d07a0e9 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
index aa1818323b8..615a1182b18 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
index 282bf108a65..36ad7b7e87f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
index 282bf108a65..36ad7b7e87f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
index 282bf108a65..36ad7b7e87f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
index 91778b7edbe..eb2f883c086 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
index 91778b7edbe..eb2f883c086 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
index 91778b7edbe..eb2f883c086 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
index 603392116eb..b2f7f38d180 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
@@ -34,8 +34,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = 32767UL;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = 32767UL;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c
index 603392116eb..b2f7f38d180 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c
@@ -34,8 +34,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = 32767UL;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = 32767UL;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index 6db200ab0af..bf2eb65234b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c
index ba08554994b..b0fc85c485e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index 2a8d7cab33d..f1e6def71d2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c
index 800ef64be2b..aab5a6b1228 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index e89a9bbab03..a5bf59395c9 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -19,8 +19,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c
index ed44677b2fd..c5e1dc20355 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c
@@ -19,8 +19,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index 9db9f987df0..2686494f297 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
index 05478205fdb..ff382f5a14f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
index 828a0e2f6c7..9de11fd683b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
@@ -50,8 +50,8 @@ typedef struct __fc_FILE FILE;
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
@@ -84,8 +84,8 @@ predicate diffSize{L1, L2}(ℤ i) =
*/
extern FILE *stdout;
-FILE fopen[512];
-FILE const *_p__fc_fopen = (FILE const *)(fopen);
+FILE __fc_fopen[512];
+FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
/*@ assigns *__fc_stdout;
assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
index 828a0e2f6c7..9de11fd683b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
@@ -50,8 +50,8 @@ typedef struct __fc_FILE FILE;
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
@@ -84,8 +84,8 @@ predicate diffSize{L1, L2}(ℤ i) =
*/
extern FILE *stdout;
-FILE fopen[512];
-FILE const *_p__fc_fopen = (FILE const *)(fopen);
+FILE __fc_fopen[512];
+FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
/*@ assigns *__fc_stdout;
assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
index 21f61f904cc..1b1a391506d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
@@ -24,8 +24,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
index 3c686df28e3..84b12d496e0 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
@@ -24,8 +24,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
index 291c1d24a82..de9f0a6c865 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c
index 5bfa785f3bf..3be5246cfb3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
index a1f40a83d09..487a65e7f23 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
@@ -21,8 +21,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
index b4d554830ba..bfd83983a86 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c
index b4d554830ba..bfd83983a86 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
index 70b672564a3..4bcd25d2c38 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
index 70b672564a3..4bcd25d2c38 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle
index fddcb52a99b..e16771bba8f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.res.oracle
index fddcb52a99b..e16771bba8f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
index c0f02d51b0f..1f09cb63b6e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index 11e9eec074f..9e13e05e51d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
index 654ef2d58ed..ee1253b86e5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
index c2858d85435..f776ff5e949 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
index b6325ad939d..6ba9bf6d9e7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
index ded5a71b828..96720f05fdb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
index 11a917359cf..b0025ffba8e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
@@ -17,8 +17,8 @@ FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `logic functio
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
index 86e479dd88b..7ad062afafc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
@@ -13,8 +13,8 @@ tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `logic functio
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
index 5ee27b10d16..61fa2dd0ad7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
index 72b8370d3d6..ec9a3771068 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
index 2908d36305d..c3e6e6d19c5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index ebab496bdc6..b75bd5d4086 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
index e1cd531afcb..c96be87ab71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
@@ -24,8 +24,8 @@ typedef unsigned int size_t;
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
index e1cd531afcb..c96be87ab71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
@@ -24,8 +24,8 @@ typedef unsigned int size_t;
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
index b77ed944f63..6d6583f6638 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
index b77ed944f63..6d6583f6638 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
index cd1aa87a38f..2cc6f18177e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
index f594a2e7523..1bbc0c9654d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
index d09d7c3c54b..af4f3a3fd81 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
index d09d7c3c54b..af4f3a3fd81 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
index f38509d6a42..2fde5581758 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
index f38509d6a42..2fde5581758 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
index 8a8625abd82..5514e19c20c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
index 6c3acc4d9ec..e9448e971bb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
index 1615b6ef377..35a2e76b508 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
index 0ac93b33fe0..37e63248597 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
index 60038ef2900..1d784f2cdac 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
index e1d38eb53a0..715a1a81196 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
index cf51d7d5248..d8e01ffbb5d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
index cf51d7d5248..d8e01ffbb5d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
index 6f92774bd2d..7ec7966af93 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
index 7ec45739b59..c45b13af219 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index 6c7cb59e21e..df1b5c1fbf7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
index b8e9076ac30..4c2fe7776ae 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
index 3ed665699cc..f5f1034d249 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
index 3ed665699cc..f5f1034d249 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
index 253d3d4adca..02887746306 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
index b91ecab66e4..329843c1b49 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
index f91e395aa1f..7f0e671807c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
index 7e4312e3b45..2b76c7ef682 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
index 2ad63c456df..862762c9009 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c
index 2ad63c456df..862762c9009 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index 4e4655bb33a..e817129f94b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
index 357c3ba8ae9..c6747b03d28 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
index ca95f8bc50f..17edc7547d3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
index 4c27d12cf49..43521357a7b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
index f54bb89c336..f9514e7699f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
index e0769e4505e..65543717ad6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
index cf4ce4f86ef..d3ce4ce6b8b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
index 1112e66a665..56c8f4f7969 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index 313b731f630..50947884763 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
index 3877084d38e..6f087c5d81d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
index ce2452867a9..e4a52463a66 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
index 6dbaf12b8f1..7e106b402af 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
index 780abf1d50c..a6fe60a1e27 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
@@ -22,8 +22,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
index 780abf1d50c..a6fe60a1e27 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
@@ -22,8 +22,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
index 1ec68a1de68..a4bb6efa875 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
index 268ad6c1baf..983c49f3da4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
index 0c2cf126e6e..017d65d08d5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
index 8a78fcd3c38..789eeed6d95 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
index b8a8828aa6e..2dffc64ca52 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
@@ -19,8 +19,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
index 359147001c4..fcb3ad3ac0b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
@@ -19,8 +19,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
index d12f78a04b9..f3bdecf2704 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
index e3f8fbe0b6c..d9b8a0192cc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
index 80dce51c3a6..4fe3c73b67c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
index 72532dc387c..676e7c3a328 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
index 216bb084e2b..a09b2333e52 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
index 216bb084e2b..a09b2333e52 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
index 4c13b1477b9..3cfb1dca11d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
@@ -22,8 +22,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
index d9cc1e20330..20eb9f1b21f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
@@ -22,8 +22,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
index 878b9a3407a..3cd0ce6d69f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
index 1e3430db814..b58a645ffe7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
index a79f65348bf..7eba374f37b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
index a79f65348bf..7eba374f37b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
index b882f493333..b3e10d11118 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
index 4adb08a08f2..b026674235d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
index 2792dcf8aaf..e2992629f11 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
index 90cdc6aeae0..c8306f004fe 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
index 77e7a73136d..7c3daa2acdc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
index f6c96b33c08..e6821c6545f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
index 7531b683c53..f4eedb8b927 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
@@ -58,8 +58,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
@@ -82,6 +82,9 @@ extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
+
/*@ ghost extern int __e_acsl_internal_heap; */
/*@ assigns __e_acsl_internal_heap;
@@ -97,8 +100,31 @@ predicate diffSize{L1, L2}(ℤ i) =
*/
extern FILE *stdout;
-FILE fopen[512];
-FILE const *_p__fc_fopen = (FILE const *)(fopen);
+FILE __fc_fopen[512];
+FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
+/*@ ensures
+ \result ≡ \null ∨
+ (\valid(\result) ∧ \subset(\result, &__fc_fopen[0 ..]));
+ assigns \result;
+ assigns \result \from *(filename+(..)), *(mode+(..)), _p__fc_fopen;
+ */
+extern FILE *fopen(char const *filename, char const *mode);
+
+/*@ ensures
+ \result ≡ \null ∨
+ (\valid(\result) ∧ \subset(\result, &__fc_fopen[0 ..]));
+ assigns \result;
+ assigns \result \from *(filename+(..)), *(mode+(..)), _p__fc_fopen;
+ */
+FILE *__e_acsl_fopen(char const *filename, char const *mode)
+{
+ FILE *__retres;
+ __store_block((void *)(& __retres),8UL);
+ __retres = fopen(filename,mode);
+ __delete_block((void *)(& __retres));
+ return __retres;
+}
+
void __e_acsl_memory_init(void)
{
__store_block((void *)(& stdout),8UL);
@@ -108,17 +134,32 @@ void __e_acsl_memory_init(void)
int main(void)
{
+ char *__e_acsl_literal_string_2;
+ char *__e_acsl_literal_string;
int __retres;
FILE *f;
+ FILE *f2;
__e_acsl_memory_init();
+ __store_block((void *)(& f2),8UL);
__store_block((void *)(& f),8UL);
__full_init((void *)(& f));
f = stdout;
+ __e_acsl_literal_string = "foo";
+ __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
+ __full_init((void *)__e_acsl_literal_string);
+ __literal_string((void *)__e_acsl_literal_string);
+ __e_acsl_literal_string_2 = "wb";
+ __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
+ __full_init((void *)__e_acsl_literal_string_2);
+ __literal_string((void *)__e_acsl_literal_string_2);
+ __full_init((void *)(& f2));
+ f2 = __e_acsl_fopen(__e_acsl_literal_string,__e_acsl_literal_string_2);
/*@ assert f ≡ __fc_stdout; */
e_acsl_assert(f == stdout,(char *)"Assertion",(char *)"main",
- (char *)"f == __fc_stdout",12);
+ (char *)"f == __fc_stdout",13);
__retres = 0;
__delete_block((void *)(& stdout));
+ __delete_block((void *)(& f2));
__delete_block((void *)(& f));
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
index 7531b683c53..13b9fa9cf18 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
@@ -58,8 +58,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
@@ -82,6 +82,16 @@ extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
/*@ ghost extern int __e_acsl_internal_heap; */
/*@ assigns __e_acsl_internal_heap;
@@ -97,8 +107,31 @@ predicate diffSize{L1, L2}(ℤ i) =
*/
extern FILE *stdout;
-FILE fopen[512];
-FILE const *_p__fc_fopen = (FILE const *)(fopen);
+FILE __fc_fopen[512];
+FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
+/*@ ensures
+ \result ≡ \null ∨
+ (\valid(\result) ∧ \subset(\result, &__fc_fopen[0 ..]));
+ assigns \result;
+ assigns \result \from *(filename+(..)), *(mode+(..)), _p__fc_fopen;
+ */
+extern FILE *fopen(char const *filename, char const *mode);
+
+/*@ ensures
+ \result ≡ \null ∨
+ (\valid(\result) ∧ \subset(\result, &__fc_fopen[0 ..]));
+ assigns \result;
+ assigns \result \from *(filename+(..)), *(mode+(..)), _p__fc_fopen;
+ */
+FILE *__e_acsl_fopen(char const *filename, char const *mode)
+{
+ FILE *__retres;
+ __store_block((void *)(& __retres),8UL);
+ __retres = fopen(filename,mode);
+ __delete_block((void *)(& __retres));
+ return __retres;
+}
+
void __e_acsl_memory_init(void)
{
__store_block((void *)(& stdout),8UL);
@@ -108,17 +141,32 @@ void __e_acsl_memory_init(void)
int main(void)
{
+ char *__e_acsl_literal_string_2;
+ char *__e_acsl_literal_string;
int __retres;
FILE *f;
+ FILE *f2;
__e_acsl_memory_init();
+ __store_block((void *)(& f2),8UL);
__store_block((void *)(& f),8UL);
__full_init((void *)(& f));
f = stdout;
+ __e_acsl_literal_string = "foo";
+ __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
+ __full_init((void *)__e_acsl_literal_string);
+ __literal_string((void *)__e_acsl_literal_string);
+ __e_acsl_literal_string_2 = "wb";
+ __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
+ __full_init((void *)__e_acsl_literal_string_2);
+ __literal_string((void *)__e_acsl_literal_string_2);
+ __full_init((void *)(& f2));
+ f2 = __e_acsl_fopen(__e_acsl_literal_string,__e_acsl_literal_string_2);
/*@ assert f ≡ __fc_stdout; */
e_acsl_assert(f == stdout,(char *)"Assertion",(char *)"main",
- (char *)"f == __fc_stdout",12);
+ (char *)"f == __fc_stdout",13);
__retres = 0;
__delete_block((void *)(& stdout));
+ __delete_block((void *)(& f2));
__delete_block((void *)(& f));
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
index b7927180ad1..dbada0dda05 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
index e0cdb70d6ea..ac6f0177bbb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
index 720929a8f71..c7f61875787 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
index 720929a8f71..c7f61875787 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
index 8149e2edc10..146b775b2f6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
@@ -19,8 +19,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
index e69481cbede..09cb51fe38a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
@@ -19,8 +19,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index 93df89f36df..e63da0d3e7f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index 93df89f36df..e63da0d3e7f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
index ddde059e921..db243d2e063 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
index 9702b5b68b4..9379b88d9ea 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index 5964f590702..45a24b77ddd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -22,8 +22,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
index 5964f590702..45a24b77ddd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
@@ -22,8 +22,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
index 3f50777239b..15e875caf18 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
index e4f0303aa76..497c9c74117 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
@@ -18,8 +18,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
index c61173356b5..97bb0712a03 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle
index fdfc7990ec2..2cee1d69b38 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
index 6f95e59543b..d0c22cc84bc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle
index 6f95e59543b..d0c22cc84bc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
index 6f64ff4256a..db4cb25cd18 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index 75e76b3c1fa..f7340321cd0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
index b5d994b3a4c..adb93500ead 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
index 1b3bf80d4f4..ada60090903 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
index 570ea6d0d06..34d08a38a82 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
index 3f92625eb67..ea82cb27ffb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
index a3babb0b4f1..55a6dc8a5ed 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
index 32af23aefb1..c79ae4bf45f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
@@ -7,8 +7,8 @@ tests/e-acsl-runtime/lazy.i:16:[rte] warning: divisor assert broken: 0 ≢ 0
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index 9d1b1436f98..ed5739d6aa1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
index 2de1029abd0..6000f8fb4f8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
index af73885cc56..89839e8fac3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
index 5109ba1df0f..cbfef42b8bf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
index 1cca0a2e3ed..b3b06850962 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
@@ -17,8 +17,8 @@ FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `logic functio
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
index c1caa33286b..823d6aabb31 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
@@ -13,8 +13,8 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
index 15598c26408..ff68f25afa0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle
index e8925e28b35..2877bdc22a3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
index 087bfb0829d..8f017d69ecd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
index 96db9cc42a3..71aa24d07a4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
index 02eb94e3703..0edcfe44db5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
@@ -13,8 +13,8 @@ FRAMAC_SHARE/libc/string.h:88:[e-acsl] warning: E-ACSL construct `applying logic
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
index 53f26299b4a..a4c8eb909d1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
@@ -13,8 +13,8 @@ FRAMAC_SHARE/libc/string.h:88:[e-acsl] warning: E-ACSL construct `applying logic
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
index e0b1cb0c3d9..8a822252367 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
index f6cf15e6ea1..151f864ecdd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
index dda4be5ebd9..57e6831e42f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
index 16bde583746..c4513a0cf3e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
index bf8c4859320..6d317b9c751 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
index bf8c4859320..6d317b9c751 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
index 966bbf3f9ed..4c6b098dd08 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
index d59dceb58ea..dec8067549f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
index d8345c4eed8..d044420359c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
index 67d6935766e..3815dcb62e0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
index 1cc53371d79..40d70b4af82 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
@@ -17,8 +17,8 @@ FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `logic functio
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
index 2879d0ab923..554ca48e718 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
@@ -13,8 +13,8 @@ tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `logic fun
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
index 67316f6bcda..f57dd54e53f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
index 539678d62e9..953488ee27e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
index 02df4c9a03f..768f090efb6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
index 40f2b194ea5..7ffb06bab75 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
index 32e1ef3c35a..505160e67de 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
index 77557d4b4f5..3d936884430 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
index b61a91ef3ae..c99d74f71f1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
@@ -1,18 +1,25 @@
[e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `fopen':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+tests/e-acsl-runtime/stdout.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdio.h:95:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
- fopen[0..511] ∈ {0}
- _p__fc_fopen ∈ {{ &fopen[0] }}
+ __fc_fopen[0..511] ∈ {0}
+ _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
[--..--]
[0].[bits 80 to 95] ∈ UNINITIALIZED
@@ -36,9 +43,12 @@
S___fc_real_data_1_S___fc_stdout[0..1] ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/stdout.c:12:[value] Assertion got status unknown.
+[value] using specification for function __literal_string
+[value] using specification for function fopen
+[value] using specification for function __delete_block
+FRAMAC_SHARE/libc/stdio.h:94:[value] Function __e_acsl_fopen: postcondition got status unknown.
+tests/e-acsl-runtime/stdout.c:13:[value] Assertion got status unknown.
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
index b61a91ef3ae..c99d74f71f1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
@@ -1,18 +1,25 @@
[e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `fopen':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+tests/e-acsl-runtime/stdout.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdio.h:95:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
- fopen[0..511] ∈ {0}
- _p__fc_fopen ∈ {{ &fopen[0] }}
+ __fc_fopen[0..511] ∈ {0}
+ _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
[--..--]
[0].[bits 80 to 95] ∈ UNINITIALIZED
@@ -36,9 +43,12 @@
S___fc_real_data_1_S___fc_stdout[0..1] ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/stdout.c:12:[value] Assertion got status unknown.
+[value] using specification for function __literal_string
+[value] using specification for function fopen
+[value] using specification for function __delete_block
+FRAMAC_SHARE/libc/stdio.h:94:[value] Function __e_acsl_fopen: postcondition got status unknown.
+tests/e-acsl-runtime/stdout.c:13:[value] Assertion got status unknown.
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
index 3c8da283445..c59e20f10fd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
index 1d4b3e00227..7e1ef6d4aa6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
index d93c1ec3603..549d5a145b5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
index d93c1ec3603..549d5a145b5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
index 07e51862ce1..eff640e073c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
index 21d29301271..3e13beeb9f8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index 9b93e8c95bd..c3ae2925bf6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -27,8 +27,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index 5044ab4e589..4a818423ac9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -19,8 +19,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index 7682f1615ba..2da3ea9dfb6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
@@ -27,8 +27,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index 060731ee943..fcddec8a4b8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
@@ -19,8 +19,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
index f4761bf8c34..3d3bab60483 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
index f4761bf8c34..3d3bab60483 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
index 86b2fcec9e2..3eea9bdbc1b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
@@ -27,8 +27,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
index 233c8f7660a..4eb0ff3fad7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
@@ -19,8 +19,8 @@ FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c b/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c
index 21c3e08bf61..10cb12f2c52 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/stdout.c
@@ -1,5 +1,5 @@
/* run.config
- COMMENT: __fc_stdout
+ COMMENT: __fc_stdout et __fc_fopen
STDOPT: #"-pp-annot"
EXECNOW: LOG gen_stdout.c BIN gen_stdout.out @frama-c@ -machdep x86_64 -pp-annot -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/stdout.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_stdout.c > /dev/null && ./gcc_runtime.sh stdout
EXECNOW: LOG gen_stdout2.c BIN gen_stdout2.out @frama-c@ -machdep x86_64 -pp-annot -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/stdout.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_stdout2.c > /dev/null && ./gcc_runtime.sh stdout2
@@ -9,5 +9,6 @@
int main(){
FILE *f = stdout;
+ FILE *f2 = fopen("foo","wb");
//@ assert f == stdout;
}
--
GitLab