From 3639519f46f12fd828d26831a33b30f03fdacf77 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 18 Sep 2013 08:07:08 +0000
Subject: [PATCH] [E-ACSL] -no-results for value in tests [E-ACSL] fix typing
bug with divisions/modulos over floats
---
.../e-acsl-runtime/oracle/addrOf.1.res.oracle | 8 --
.../e-acsl-runtime/oracle/addrOf.res.oracle | 8 --
.../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 | 6 --
.../e-acsl-runtime/oracle/array.res.oracle | 6 --
.../e-acsl-runtime/oracle/at.1.res.oracle | 20 -----
.../tests/e-acsl-runtime/oracle/at.res.oracle | 20 -----
.../oracle/bts1304.1.res.oracle | 7 --
.../e-acsl-runtime/oracle/bts1304.res.oracle | 7 --
.../oracle/bts1307.1.res.oracle | 16 ----
.../e-acsl-runtime/oracle/bts1307.res.oracle | 19 +----
.../oracle/bts1324.1.res.oracle | 13 ---
.../e-acsl-runtime/oracle/bts1324.res.oracle | 13 ---
.../oracle/bts1326.1.res.oracle | 13 ---
.../e-acsl-runtime/oracle/bts1326.res.oracle | 13 ---
.../oracle/bts1390.1.res.oracle | 9 ---
.../e-acsl-runtime/oracle/bts1390.res.oracle | 9 ---
.../oracle/bts1398.1.res.oracle | 13 ---
.../e-acsl-runtime/oracle/bts1398.res.oracle | 13 ---
.../oracle/bts1399.1.res.oracle | 11 ---
.../e-acsl-runtime/oracle/bts1399.res.oracle | 11 ---
.../oracle/bts1478.1.res.oracle | 9 ---
.../e-acsl-runtime/oracle/bts1478.res.oracle | 9 ---
.../e-acsl-runtime/oracle/call.1.res.oracle | 20 -----
.../e-acsl-runtime/oracle/call.res.oracle | 20 -----
.../e-acsl-runtime/oracle/cast.1.res.oracle | 4 -
.../e-acsl-runtime/oracle/cast.res.oracle | 4 -
.../oracle/comparison.1.res.oracle | 5 --
.../oracle/comparison.res.oracle | 5 --
.../e-acsl-runtime/oracle/false.1.res.oracle | 3 -
.../e-acsl-runtime/oracle/false.res.oracle | 3 -
.../oracle/function_contract.1.res.oracle | 39 ---------
.../oracle/function_contract.res.oracle | 39 ---------
.../e-acsl-runtime/oracle/ghost.1.res.oracle | 8 --
.../e-acsl-runtime/oracle/ghost.res.oracle | 8 --
.../oracle/integer_constant.1.res.oracle | 3 -
.../oracle/integer_constant.res.oracle | 3 -
.../oracle/invariant.1.res.oracle | 3 -
.../oracle/invariant.res.oracle | 3 -
.../oracle/labeled_stmt.1.res.oracle | 6 --
.../oracle/labeled_stmt.res.oracle | 6 --
.../e-acsl-runtime/oracle/lazy.1.res.oracle | 4 -
.../e-acsl-runtime/oracle/lazy.res.oracle | 4 -
.../oracle/linear_search.1.res.oracle | 9 ---
.../oracle/linear_search.res.oracle | 9 ---
.../oracle/literal_string.1.res.oracle | 14 ----
.../oracle/literal_string.res.oracle | 14 ----
.../oracle/localvar.1.res.oracle | 19 -----
.../e-acsl-runtime/oracle/localvar.res.oracle | 19 -----
.../oracle/longlong.1.res.oracle | 8 --
.../e-acsl-runtime/oracle/longlong.res.oracle | 8 --
.../e-acsl-runtime/oracle/loop.1.res.oracle | 40 ----------
.../e-acsl-runtime/oracle/loop.res.oracle | 79 -------------------
.../oracle/nested_code_annot.1.res.oracle | 4 -
.../oracle/nested_code_annot.res.oracle | 4 -
.../e-acsl-runtime/oracle/not.1.res.oracle | 3 -
.../e-acsl-runtime/oracle/not.res.oracle | 3 -
.../e-acsl-runtime/oracle/null.1.res.oracle | 2 -
.../e-acsl-runtime/oracle/null.res.oracle | 2 -
.../oracle/other_constants.1.res.oracle | 2 -
.../oracle/other_constants.res.oracle | 2 -
.../e-acsl-runtime/oracle/ptr.1.res.oracle | 8 --
.../e-acsl-runtime/oracle/ptr.res.oracle | 8 --
.../oracle/ptr_init.1.res.oracle | 18 -----
.../e-acsl-runtime/oracle/ptr_init.res.oracle | 18 -----
.../oracle/quantif.1.res.oracle | 2 -
.../e-acsl-runtime/oracle/quantif.res.oracle | 2 -
.../e-acsl-runtime/oracle/result.1.res.oracle | 14 ----
.../e-acsl-runtime/oracle/result.res.oracle | 14 ----
.../e-acsl-runtime/oracle/sizeof.1.res.oracle | 3 -
.../e-acsl-runtime/oracle/sizeof.res.oracle | 3 -
.../oracle/stmt_contract.1.res.oracle | 4 -
.../oracle/stmt_contract.res.oracle | 4 -
.../e-acsl-runtime/oracle/true.1.res.oracle | 3 -
.../e-acsl-runtime/oracle/true.res.oracle | 3 -
.../oracle/typedef.1.res.oracle | 3 -
.../e-acsl-runtime/oracle/typedef.res.oracle | 3 -
.../e-acsl-runtime/oracle/valid.1.res.oracle | 25 ------
.../e-acsl-runtime/oracle/valid.res.oracle | 25 ------
.../oracle/valid_alias.1.res.oracle | 13 ---
.../oracle/valid_alias.res.oracle | 13 ---
.../oracle/valid_in_contract.1.res.oracle | 7 --
.../oracle/valid_in_contract.res.oracle | 7 --
.../e-acsl-runtime/oracle/vector.1.res.oracle | 21 -----
.../e-acsl-runtime/oracle/vector.res.oracle | 21 -----
.../e-acsl/tests/e-acsl-runtime/test_config | 4 +-
src/plugins/e-acsl/typing.ml | 7 +-
88 files changed, 9 insertions(+), 936 deletions(-)
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 aa55f57b681..8773d06ed29 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
@@ -30,11 +30,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- m ∈ {123}
- u ∈ {{ &m }}
- p ∈ {{ &m }}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- x ∈ {0}
- __retres ∈ {0}
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 aa55f57b681..8773d06ed29 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
@@ -30,11 +30,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- m ∈ {123}
- u ∈ {{ &m }}
- p ∈ {{ &m }}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- x ∈ {0}
- __retres ∈ {0}
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 e826a10252a..569a317907e 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
@@ -86,7 +86,3 @@ tests/e-acsl-runtime/arith.i:33:[value] Assertion got status valid.
tests/e-acsl-runtime/arith.i:33:[value] Assertion 'E_ACSL' got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {-3}
- y ∈ {2}
- __retres ∈ {0}
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 a5f2cd71f27..9d33b17f15c 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
@@ -38,7 +38,3 @@ tests/e-acsl-runtime/arith.i:32:[value] Assertion got status valid.
tests/e-acsl-runtime/arith.i:33:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {-3}
- y ∈ {2}
- __retres ∈ {0}
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 1d3b8f7c042..c4cd42d3ae3 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
@@ -26,9 +26,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
tests/e-acsl-runtime/array.i:16:[value] Assertion got status unknown.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- T1[0] ∈ {0; 2}
- [1..2] ∈ {0; 1; 2}
- T2[0] ∈ {0; 2}
- [1..3] ∈ {0; 2; 4; 6}
- __retres ∈ {0}
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 3f7c1963f28..9c76d866663 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
@@ -35,9 +35,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition
tests/e-acsl-runtime/array.i:16:[value] Assertion got status unknown.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- T1[0] ∈ {0; 2}
- [1..2] ∈ {0; 1; 2}
- T2[0] ∈ {0; 2}
- [1..3] ∈ {0; 2; 4; 6}
- __retres ∈ {0}
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 8a0364192b2..a05225b59c2 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
@@ -69,23 +69,3 @@ tests/e-acsl-runtime/at.i:34:[value] Assertion got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- A ∈ {3}
-[value] Values at end of function __e_acsl_f:
- A ∈ {3}
-[value] Values at end of function g:
- A ∈ {4}
- x ∈ {1}
- t[0] ∈ {2}
- [1] ∈ {3}
-[value] Values at end of function h:
-
-[value] Values at end of function __e_acsl_h:
- __retres ∈ {0}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- A ∈ {4}
- x ∈ {1}
- t[0] ∈ {2}
- [1] ∈ {3}
- __retres ∈ {0}
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 4e633188c05..8ca19010e11 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
@@ -50,23 +50,3 @@ tests/e-acsl-runtime/at.i:34:[value] Assertion got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- A ∈ {3}
-[value] Values at end of function __e_acsl_f:
- A ∈ {3}
-[value] Values at end of function g:
- A ∈ {4}
- x ∈ {1}
- t[0] ∈ {2}
- [1] ∈ {3}
-[value] Values at end of function h:
-
-[value] Values at end of function __e_acsl_h:
- __retres ∈ {0}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- A ∈ {4}
- x ∈ {1}
- t[0] ∈ {2}
- [1] ∈ {3}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
index 6640da36b1d..1cb0bf21fee 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
@@ -29,10 +29,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function read_sensor_4:
- buf[0..11] ∈ {0} or UNINITIALIZED
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- buf[0..11] ∈ {0}
- i ∈ {3}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
index 6640da36b1d..1cb0bf21fee 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
@@ -29,10 +29,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function read_sensor_4:
- buf[0..11] ∈ {0} or UNINITIALIZED
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- buf[0..11] ∈ {0}
- i ∈ {3}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
index 313e9f7afd2..11f4a771e50 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
@@ -7,9 +7,7 @@
tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
[e-acsl] beginning translation.
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating type `real' by `long double'
-tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
@@ -78,17 +76,3 @@ tests/e-acsl-runtime/bts1307.i:25:[value] Function __e_acsl_bar, behavior UnderE
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function bar:
- h ∈ 0.850000023842
-[value] Values at end of function __e_acsl_bar:
- h ∈ 0.850000023842
-[value] Values at end of function foo:
- h ∈ 6.
-[value] Values at end of function __e_acsl_foo:
- h ∈ 6.
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- f ∈ 1.
- g ∈ 1.
- h ∈ 0.850000023842
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
index 7fb4f34d14f..c95f7403f10 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
@@ -39,9 +39,10 @@ tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Mo
FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:93:[value] Function __valid_read: postcondition got status unknown.
FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:94:[value] Function __valid_read: postcondition got status valid.
[value] user error: type long double not implemented. Using double instead
-tests/e-acsl-runtime/bts1307.i:13:[kernel] warning: non-finite long double value ({5}):
+tests/e-acsl-runtime/bts1307.i:13:[kernel] warning: non-finite float value ([-1.79769313486e+308 .. 1.79769313486e+308]):
assert
- \is_finite((long double)(5-(long double)((long double)((int)(5/80)**__e_acsl_at_3)*0.4)));
+ \is_finite((float)(*__e_acsl_at_2+(int)(5-(long double)((float)((int)
+ (5/80)**__e_acsl_at_3)*0.4))));
tests/e-acsl-runtime/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: postcondition got status valid.
tests/e-acsl-runtime/bts1307.i:19:[value] Function __e_acsl_bar: precondition got status valid.
tests/e-acsl-runtime/bts1307.i:20:[value] Function __e_acsl_bar: precondition got status valid.
@@ -55,17 +56,3 @@ tests/e-acsl-runtime/bts1307.i:25:[value] Function __e_acsl_bar, behavior UnderE
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function bar:
- h ∈ 0.850000023842
-[value] Values at end of function __e_acsl_bar:
- h ∈ 0.850000023842
-[value] Values at end of function foo:
- h ∈ 6.
-[value] Values at end of function __e_acsl_foo:
- h ∈ 6.
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- f ∈ 1.
- g ∈ 1.
- h ∈ 0.850000023842
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
index 026e16c2440..a0f5710bcda 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
@@ -56,16 +56,3 @@ tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function sorted:
- b ∈ [7..15]
- __retres ∈ {1}
-[value] Values at end of function __e_acsl_sorted:
- __retres ∈ {1}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- t[0] ∈ {1}
- [1..2] ∈ {4}
- [3..5] ∈ {5}
- [6] ∈ {7}
- n ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
index 613e5742549..5198e195ed6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
@@ -33,16 +33,3 @@ tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function sorted:
- b ∈ [7..15]
- __retres ∈ {1}
-[value] Values at end of function __e_acsl_sorted:
- __retres ∈ {1}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- t[0] ∈ {1}
- [1..2] ∈ {4}
- [3..5] ∈ {5}
- [6] ∈ {7}
- n ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
index d151fa8905a..94b221716da 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
@@ -47,16 +47,3 @@ tests/e-acsl-runtime/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAv
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function atp_NORMAL_computeAverageAccel:
- av ∈ {3}
-[value] Values at end of function __e_acsl_atp_NORMAL_computeAverageAccel:
- av ∈ {3}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- Accel[0] ∈ {1}
- [1] ∈ {2}
- [2] ∈ {3}
- [3] ∈ {4}
- [4] ∈ {5}
- av ∈ {3}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.res.oracle
index 9ed71ba6232..8b2fe09a5f9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.res.oracle
@@ -30,16 +30,3 @@ tests/e-acsl-runtime/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAv
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function atp_NORMAL_computeAverageAccel:
- av ∈ {3}
-[value] Values at end of function __e_acsl_atp_NORMAL_computeAverageAccel:
- av ∈ {3}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- Accel[0] ∈ {1}
- [1] ∈ {2}
- [2] ∈ {3}
- [3] ∈ {4}
- [4] ∈ {5}
- av ∈ {3}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
index 028cb572556..dc531550cdf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
@@ -43,12 +43,3 @@ tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function memchr:
- i ∈ {0; 1; 2; 3; 4}
- s ∈ {{ "toto" + {0; 1} ; "tata" + [0..--] }}
- __retres ∈ {{ NULL ; "toto" + {1} }}
-[value] Values at end of function __e_acsl_memchr:
- __retres ∈ {{ NULL ; "toto" + {1} }}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
index 0b0259f7ab2..46aa73f9818 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
@@ -68,12 +68,3 @@ tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function memchr:
- i ∈ {0; 1; 2; 3; 4}
- s ∈ {{ "toto" + {0; 1} ; "tata" + [0..--] }}
- __retres ∈ {{ NULL ; "toto" + {1} }}
-[value] Values at end of function __e_acsl_memchr:
- __retres ∈ {{ NULL ; "toto" + {1} }}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
index cadee1883c3..9fabd606e3d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
@@ -56,16 +56,3 @@
[value] using specification for function printf
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- t[0] ∈ {1}
- [1] ∈ {2}
- i ∈ {1}
- __retres ∈ {0}
- S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
- [--..--]
- [0].__fc_inode ∈
- {{ NULL + [--..--] ; &S___fc_inode_0_S___fc_stdout }}
- [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
- [--..--]
- [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
index cadee1883c3..9fabd606e3d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
@@ -56,16 +56,3 @@
[value] using specification for function printf
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- t[0] ∈ {1}
- [1] ∈ {2}
- i ∈ {1}
- __retres ∈ {0}
- S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
- [--..--]
- [0].__fc_inode ∈
- {{ NULL + [--..--] ; &S___fc_inode_0_S___fc_stdout }}
- [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
- [--..--]
- [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
index 4c1213eb840..f7a92f10fe0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
@@ -49,14 +49,3 @@ FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior dealloca
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- state ∈ ESCAPINGADDR
- __retres ∈ {0}
- Frama_C_alloc[0..447] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
index 0622734bb26..e40384a482a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
@@ -68,14 +68,3 @@ FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior dealloca
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- state ∈ ESCAPINGADDR
- __retres ∈ {0}
- Frama_C_alloc[0..447] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
index 825a55c5156..88faa36b80d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
@@ -45,12 +45,3 @@ tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function loop:
-
-[value] Values at end of function __e_acsl_loop:
-
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
index c65806558f4..a4cfba3e7c9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
@@ -36,12 +36,3 @@ tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function loop:
-
-[value] Values at end of function __e_acsl_loop:
-
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- __retres ∈ {0}
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 368529f6a90..0da47a198a9 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
@@ -40,23 +40,3 @@ tests/e-acsl-runtime/call.c:12:[value] Function __e_acsl_f: postcondition got st
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
-[value] Values at end of function f:
- Frama_C_alloc[bits 0 to 31] ∈ {1}
- Frama_C_alloc_0[bits 0 to 31] ∈ {1} or UNINITIALIZED
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {{ &x }}
- Frama_C_alloc[bits 0 to 31] ∈ {1}
- Frama_C_alloc_0[bits 0 to 31] ∈ {1} or UNINITIALIZED
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- x ∈ {0}
- p ∈ {{ &x }}
- q ∈ {{ &x }}
- r ∈ {{ &Frama_C_alloc_0 }}
- __retres ∈ {0}
- Frama_C_alloc[bits 0 to 31] ∈ {1}
- Frama_C_alloc_0[bits 0 to 31] ∈ {1}
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 368529f6a90..0da47a198a9 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
@@ -40,23 +40,3 @@ tests/e-acsl-runtime/call.c:12:[value] Function __e_acsl_f: postcondition got st
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
-[value] Values at end of function f:
- Frama_C_alloc[bits 0 to 31] ∈ {1}
- Frama_C_alloc_0[bits 0 to 31] ∈ {1} or UNINITIALIZED
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {{ &x }}
- Frama_C_alloc[bits 0 to 31] ∈ {1}
- Frama_C_alloc_0[bits 0 to 31] ∈ {1} or UNINITIALIZED
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- x ∈ {0}
- p ∈ {{ &x }}
- q ∈ {{ &x }}
- r ∈ {{ &Frama_C_alloc_0 }}
- __retres ∈ {0}
- Frama_C_alloc[bits 0 to 31] ∈ {1}
- Frama_C_alloc_0[bits 0 to 31] ∈ {1}
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 9f16f96e5d0..20ae38c9e7f 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
@@ -26,7 +26,3 @@ tests/e-acsl-runtime/cast.i:19:[value] Assertion got status valid.
tests/e-acsl-runtime/cast.i:20:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- y ∈ {0}
- __retres ∈ {0}
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 6fb627ae899..6ed92f56e1f 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
@@ -45,7 +45,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: preconditio
tests/e-acsl-runtime/cast.i:20:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- y ∈ {0}
- __retres ∈ {0}
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 dc04ecac552..6961112718f 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
@@ -56,8 +56,3 @@ tests/e-acsl-runtime/comparison.i:28:[value] Assertion got status valid.
tests/e-acsl-runtime/comparison.i:29:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- y ∈ {1}
- s ∈ {{ "toto" }}
- __retres ∈ {0}
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 8cb4feb818d..e77b42acb2e 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
@@ -40,8 +40,3 @@ tests/e-acsl-runtime/comparison.i:28:[value] Assertion got status valid.
tests/e-acsl-runtime/comparison.i:29:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- y ∈ {1}
- s ∈ {{ "toto" }}
- __retres ∈ {0}
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 b5ed2908c38..dbb2932fc8d 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
@@ -18,6 +18,3 @@
__memory_size ∈ [--..--]
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- __retres ∈ {0}
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 b5ed2908c38..dbb2932fc8d 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
@@ -18,6 +18,3 @@
__memory_size ∈ [--..--]
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- __retres ∈ {0}
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 dbe3866dbb7..8889978e5cf 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
@@ -83,42 +83,3 @@ tests/e-acsl-runtime/function_contract.i:71:[value] Function __e_acsl_n, behavio
tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; postcondition not evaluated.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- X ∈ {1}
-[value] Values at end of function __e_acsl_f:
- X ∈ {1}
-[value] Values at end of function g:
- X ∈ {2}
-[value] Values at end of function __e_acsl_g:
- X ∈ {2}
-[value] Values at end of function h:
- X ∈ {3}
-[value] Values at end of function __e_acsl_h:
- X ∈ {3}
-[value] Values at end of function i:
- X ∈ {5}
-[value] Values at end of function __e_acsl_i:
- X ∈ {5}
-[value] Values at end of function j:
- X ∈ {3}
-[value] Values at end of function __e_acsl_j:
- X ∈ {3}
-[value] Values at end of function k:
- X ∈ {5}
-[value] Values at end of function __e_acsl_k:
- X ∈ {5}
-[value] Values at end of function l:
-
-[value] Values at end of function __e_acsl_l:
- __retres ∈ {5}
-[value] Values at end of function m:
- X ∈ {7}
-[value] Values at end of function __e_acsl_m:
- X ∈ {7}
-[value] Values at end of function n:
- X ∈ {8}
-[value] Values at end of function __e_acsl_n:
- X ∈ {8}
-[value] Values at end of function main:
- X ∈ {8}
- __retres ∈ {0}
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 d11a5d9f76c..874df546bf0 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
@@ -67,42 +67,3 @@ tests/e-acsl-runtime/function_contract.i:71:[value] Function __e_acsl_n, behavio
tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; postcondition not evaluated.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- X ∈ {1}
-[value] Values at end of function __e_acsl_f:
- X ∈ {1}
-[value] Values at end of function g:
- X ∈ {2}
-[value] Values at end of function __e_acsl_g:
- X ∈ {2}
-[value] Values at end of function h:
- X ∈ {3}
-[value] Values at end of function __e_acsl_h:
- X ∈ {3}
-[value] Values at end of function i:
- X ∈ {5}
-[value] Values at end of function __e_acsl_i:
- X ∈ {5}
-[value] Values at end of function j:
- X ∈ {3}
-[value] Values at end of function __e_acsl_j:
- X ∈ {3}
-[value] Values at end of function k:
- X ∈ {5}
-[value] Values at end of function __e_acsl_k:
- X ∈ {5}
-[value] Values at end of function l:
-
-[value] Values at end of function __e_acsl_l:
- __retres ∈ {5}
-[value] Values at end of function m:
- X ∈ {7}
-[value] Values at end of function __e_acsl_m:
- X ∈ {7}
-[value] Values at end of function n:
- X ∈ {8}
-[value] Values at end of function __e_acsl_n:
- X ∈ {8}
-[value] Values at end of function main:
- X ∈ {8}
- __retres ∈ {0}
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 9a7d2dab63c..dcd294fb4af 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
@@ -38,11 +38,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- G ∈ {1}
- P ∈ {{ &G }}
- q ∈ {{ &G }}
- __retres ∈ {0}
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 4880c72a7e8..6fd50ebee3c 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
@@ -43,11 +43,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- G ∈ {1}
- P ∈ {{ &G }}
- q ∈ {{ &G }}
- __retres ∈ {0}
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 9e19e37529c..698e1380734 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
@@ -37,6 +37,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:76:[value] Function __gmpz_init_set_str: postco
tests/e-acsl-runtime/integer_constant.i:13:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {1}
- __retres ∈ {0}
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 a4857abe6f9..060220d92e7 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
@@ -34,6 +34,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {1}
- __retres ∈ {0}
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 04ff9004646..1533e5e39e3 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
@@ -31,6 +31,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+i ≤ 2147483647;
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ [0..2147483647]
- __retres ∈ {0}
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 1a6d4d66bdc..248c8af9cc2 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
@@ -23,6 +23,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+i ≤ 2147483647;
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ [0..2147483647]
- __retres ∈ {0}
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 8a1f7d4ba04..28f904648cb 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
@@ -33,9 +33,3 @@ tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function __e_acsl_main: postcondit
tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function main: postcondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_main:
- X ∈ {3}
- __retres ∈ {0}
-[value] Values at end of function main:
- X ∈ {3}
- __retres ∈ {0}
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 6bcf7ea63af..2d59ce2eeda 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
@@ -24,9 +24,3 @@ tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function __e_acsl_main: postcondit
tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function main: postcondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_main:
- X ∈ {3}
- __retres ∈ {0}
-[value] Values at end of function main:
- X ∈ {3}
- __retres ∈ {0}
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 074e28f29a4..f47b81bc824 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
@@ -56,7 +56,3 @@ tests/e-acsl-runtime/lazy.i:29:[value] Assertion got status valid.
tests/e-acsl-runtime/lazy.i:30:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- y ∈ {1}
- __retres ∈ {0}
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 849cb66ea60..c1ab49ed8ff 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
@@ -39,7 +39,3 @@ tests/e-acsl-runtime/lazy.i:29:[value] Assertion got status valid.
tests/e-acsl-runtime/lazy.i:30:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- y ∈ {1}
- __retres ∈ {0}
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 f35104b955a..27fbd7dfebd 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
@@ -64,12 +64,3 @@ tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function search:
- k ∈ [0..10]
- __retres ∈ {0; 1}
-[value] Values at end of function __e_acsl_search:
- __retres ∈ {0; 1}
-[value] Values at end of function main:
- A[0..9] ∈ [0..81]
- found ∈ {0}
- __retres ∈ {0}
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 9a6166c3bcb..4fe509716ad 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
@@ -39,12 +39,3 @@ tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function search:
- k ∈ [0..10]
- __retres ∈ {0; 1}
-[value] Values at end of function __e_acsl_search:
- __retres ∈ {0; 1}
-[value] Values at end of function main:
- A[0..9] ∈ [0..81]
- found ∈ {0}
- __retres ∈ {0}
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 605f7090247..097753bfe55 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
@@ -55,17 +55,3 @@ tests/e-acsl-runtime/literal_string.i:13:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_memory_init:
- T ∈ {{ "bar" }}
- S ∈ {{ "foo" }}
- S2 ∈ {{ "foo2" }}
-[value] Values at end of function f:
- G ∈ {1}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- T ∈ {{ "bar" }}
- G ∈ {1}
- S ∈ {{ "foo" }}
- S2 ∈ {{ "foo2" }}
- SS ∈ {{ "ss" }}
- __retres ∈ {0}
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 b2591573676..57c1ac1c53f 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
@@ -47,17 +47,3 @@ tests/e-acsl-runtime/literal_string.i:13:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_memory_init:
- T ∈ {{ "bar" }}
- S ∈ {{ "foo" }}
- S2 ∈ {{ "foo2" }}
-[value] Values at end of function f:
- G ∈ {1}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- T ∈ {{ "bar" }}
- G ∈ {1}
- S ∈ {{ "foo" }}
- S2 ∈ {{ "foo2" }}
- SS ∈ {{ "ss" }}
- __retres ∈ {0}
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 be56602ae89..523c06b2b3d 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
@@ -42,22 +42,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
-[value] Values at end of function add:
- __fc_heap_status ∈ [--..--]
- new ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
- Frama_C_alloc[bits 0 to 31] ∈ {4}
- [4..7] ∈ {0}
- Frama_C_alloc_0[bits 0 to 31] ∈ {7}
- [bits 32 to 63] ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- l ∈ {{ &Frama_C_alloc_0 }}
- __retres ∈ {0}
- Frama_C_alloc[bits 0 to 31] ∈ {4}
- [4..7] ∈ {0}
- Frama_C_alloc_0[bits 0 to 31] ∈ {7}
- [bits 32 to 63] ∈ {{ &Frama_C_alloc }}
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 be56602ae89..523c06b2b3d 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
@@ -42,22 +42,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
-[value] Values at end of function add:
- __fc_heap_status ∈ [--..--]
- new ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
- Frama_C_alloc[bits 0 to 31] ∈ {4}
- [4..7] ∈ {0}
- Frama_C_alloc_0[bits 0 to 31] ∈ {7}
- [bits 32 to 63] ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- l ∈ {{ &Frama_C_alloc_0 }}
- __retres ∈ {0}
- Frama_C_alloc[bits 0 to 31] ∈ {4}
- [4..7] ∈ {0}
- Frama_C_alloc_0[bits 0 to 31] ∈ {7}
- [bits 32 to 63] ∈ {{ &Frama_C_alloc }}
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 06ca9a7373d..b4be92d36aa 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
@@ -65,11 +65,3 @@ tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison:
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-tests/e-acsl-runtime/longlong.i:11:[inout] warning: During inout context analysis of my_pow:
- ignoring probable recursive call.
-[value] Values at end of function my_pow:
- tmp ∈ [--..--]
- __retres ∈ [0..4294967294],0%2
-[value] Values at end of function main:
- x ∈ [0..4294967294],0%2
- __retres ∈ {0}
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 daeec6d3f85..bf00755202c 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
@@ -63,11 +63,3 @@ tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison: assert
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-tests/e-acsl-runtime/longlong.i:11:[inout] warning: During inout context analysis of my_pow:
- ignoring probable recursive call.
-[value] Values at end of function my_pow:
- tmp ∈ [--..--]
- __retres ∈ [0..4294967294],0%2
-[value] Values at end of function main:
- x ∈ [0..4294967294],0%2
- __retres ∈ {0}
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 2034d9ebfe3..67423ac21da 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
@@ -30,43 +30,3 @@ tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-va
tests/e-acsl-runtime/loop.i:28:[value] Loop invariant got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function nested_loops:
- t{[0][0..14]; [1][0]} ∈ {0}
- [1][1] ∈ {1}
- [1][2] ∈ {2}
- [1][3] ∈ {3}
- [1][4] ∈ {4}
- [1][5] ∈ {5}
- [1][6] ∈ {6}
- [1][7] ∈ {7}
- [1][8] ∈ {8}
- [1][9] ∈ {9}
- [1][10] ∈ {10}
- [1][11] ∈ {11}
- [1][12] ∈ {12}
- [1][13] ∈ {13}
- [1][14] ∈ {14}
- [2][0] ∈ {0}
- [2][1..3] ∈ [2..127]
- [2][4..14] ∈ [2..127] or UNINITIALIZED
- [3][0] ∈ [0..127] or UNINITIALIZED
- [3][1..14] ∈ [2..127] or UNINITIALIZED
- [4][0] ∈ [0..127] or UNINITIALIZED
- [4][1..14] ∈ [2..127] or UNINITIALIZED
- [5][0] ∈ [0..126] or UNINITIALIZED
- [5][1..14] ∈ [2..126] or UNINITIALIZED
- [6][0] ∈ [0..126] or UNINITIALIZED
- [6][1..14] ∈ [2..126] or UNINITIALIZED
- [7][0] ∈ [0..126] or UNINITIALIZED
- [7][1..14] ∈ [2..126] or UNINITIALIZED
- [8][0] ∈ [0..126] or UNINITIALIZED
- [8][1..14] ∈ [2..126] or UNINITIALIZED
- [9][0] ∈ [0..126] or UNINITIALIZED
- [9][1..14] ∈ [2..126] or UNINITIALIZED
- i ∈ {10}
-[value] Values at end of function simple_loop:
- sum ∈ {45}
-[value] Values at end of function unnatural_loop:
- x ∈ {5}
-[value] Values at end of function main:
- __retres ∈ {0}
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 a2b4b995e79..fe99e93ad60 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
@@ -65,82 +65,3 @@ tests/e-acsl-runtime/loop.i:21:[value] entering loop for the first time
tests/e-acsl-runtime/loop.i:28:[value] Loop invariant got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function nested_loops:
- t{[0][0..14]; [1][0]} ∈ {0}
- [1][1] ∈ {1}
- [1][2] ∈ {2}
- [1][3] ∈ {3}
- [1][4] ∈ {4}
- [1][5] ∈ {5}
- [1][6] ∈ {6}
- [1][7] ∈ {7}
- [1][8] ∈ {8}
- [1][9] ∈ {9}
- [1][10] ∈ {10}
- [1][11] ∈ {11}
- [1][12] ∈ {12}
- [1][13] ∈ {13}
- [1][14] ∈ {14}
- [2][0] ∈ {0}
- [2][1] ∈ {2}
- [2][2] ∈ {4}
- [2][3] ∈ {6}
- [2][4] ∈ {8}
- [2][5] ∈ {10}
- [2][6] ∈ {12}
- [2][7] ∈ {14}
- [2][8] ∈ {16}
- [2][9] ∈ {18}
- [2][10] ∈ {20}
- [2][11] ∈ {22}
- [2][12] ∈ {24}
- [2][13] ∈ {26}
- [2][14] ∈ {28}
- [3][0] ∈ {0}
- [3][1] ∈ {3}
- [3][2] ∈ {6}
- [3][3] ∈ {9}
- [3][4] ∈ {12}
- [3][5] ∈ {15}
- [3][6] ∈ {18}
- [3][7] ∈ {21}
- [3][8] ∈ {24}
- [3][9] ∈ {27}
- [3][10] ∈ {30}
- [3][11] ∈ {33}
- [3][12] ∈ {36}
- [3][13] ∈ {39}
- [3][14] ∈ {42}
- [4][0] ∈ {0}
- [4][1] ∈ {4}
- [4][2] ∈ {8}
- [4][3] ∈ {12}
- [4][4] ∈ {16}
- [4][5] ∈ {20}
- [4][6] ∈ {24}
- [4][7] ∈ {28}
- [4][8] ∈ {32}
- [4][9] ∈ {36}
- [4][10] ∈ {40}
- [4][11] ∈ {44}
- [4][12] ∈ {48}
- [4][13] ∈ {52}
- [4][14] ∈ {56}
- [5][0] ∈ {0}
- [5][1..5] ∈ [5..126]
- [5][6..14] ∈ [5..126] or UNINITIALIZED
- [6][0] ∈ [0..126] or UNINITIALIZED
- [6][1..14] ∈ [5..126] or UNINITIALIZED
- [7][0] ∈ [0..126] or UNINITIALIZED
- [7][1..14] ∈ [5..126] or UNINITIALIZED
- [8][0] ∈ [0..126] or UNINITIALIZED
- [8][1..14] ∈ [5..126] or UNINITIALIZED
- [9][0] ∈ [0..126] or UNINITIALIZED
- [9][1..14] ∈ [5..126] or UNINITIALIZED
- i ∈ {10}
-[value] Values at end of function simple_loop:
- sum ∈ {45}
-[value] Values at end of function unnatural_loop:
- x ∈ {5}
-[value] Values at end of function main:
- __retres ∈ {0}
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 278ee4bc1b8..534c38767c1 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
@@ -30,7 +30,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {2}
- y ∈ {1}
- __retres ∈ {0}
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 6557b0c429a..e5c23161271 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
@@ -21,7 +21,3 @@ tests/e-acsl-runtime/nested_code_annot.i:9:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {2}
- y ∈ {1}
- __retres ∈ {0}
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 b6da3560900..c4f9ff2db62 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
@@ -30,6 +30,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- __retres ∈ {0}
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 92fcf287fb2..40316cdce21 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
@@ -21,6 +21,3 @@ tests/e-acsl-runtime/not.i:8:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- __retres ∈ {0}
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 60f6bc16873..f166bba7846 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
@@ -21,5 +21,3 @@ tests/e-acsl-runtime/null.i:8:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __retres ∈ {0}
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 60f6bc16873..f166bba7846 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
@@ -21,5 +21,3 @@ tests/e-acsl-runtime/null.i:8:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __retres ∈ {0}
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 a968f385f31..9693e41b97b 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
@@ -31,5 +31,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition
tests/e-acsl-runtime/other_constants.i:13:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __retres ∈ {0}
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 15fc52ccb20..2042277c0a8 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
@@ -22,5 +22,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
tests/e-acsl-runtime/other_constants.i:13:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __retres ∈ {0}
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 81b8356afcf..73e6d73c9e8 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
@@ -70,11 +70,3 @@ tests/e-acsl-runtime/ptr.i:27:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- x ∈ {1}
- t[0] ∈ {2}
- [1] ∈ {3}
- [2] ∈ {5}
- p ∈ {{ &t + {8} }}
- __retres ∈ {0}
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 f8a7c968bfd..05ae42c747a 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
@@ -44,11 +44,3 @@ tests/e-acsl-runtime/ptr.i:27:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- x ∈ {1}
- t[0] ∈ {2}
- [1] ∈ {3}
- [2] ∈ {5}
- p ∈ {{ &t + {8} }}
- __retres ∈ {0}
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 8750728362c..a3038ab5ba0 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
@@ -46,21 +46,3 @@ tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈
- {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function f:
- A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
-[value] Values at end of function g:
-
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- B ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- x ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- y ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- __retres ∈ {0}
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 8750728362c..a3038ab5ba0 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
@@ -46,21 +46,3 @@ tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈
- {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function f:
- A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
-[value] Values at end of function g:
-
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- B ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- x ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- y ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- __retres ∈ {0}
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 6169ca8a5d3..850eee44a2a 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
@@ -68,5 +68,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition g
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __retres ∈ {0}
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 6186b7fcbc7..330bd859fb7 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
@@ -36,5 +36,3 @@ tests/e-acsl-runtime/quantif.i:27:[value] entering loop for the first time
tests/e-acsl-runtime/quantif.i:28:[value] entering loop for the first time
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __retres ∈ {0}
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 7b7d8af08d8..0c5e00fef6d 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
@@ -45,17 +45,3 @@ tests/e-acsl-runtime/result.i:23:[value] Function h: postcondition got status va
tests/e-acsl-runtime/result.i:23:[value] Function __e_acsl_h: postcondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- x ∈ {0}
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {0}
-[value] Values at end of function g:
-
-[value] Values at end of function __e_acsl_g:
- __retres ∈ {1}
-[value] Values at end of function h:
- __retres ∈ {0}
-[value] Values at end of function __e_acsl_h:
- __retres ∈ {0}
-[value] Values at end of function main:
- __retres ∈ {0}
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 77fe429d401..013d4c42c5c 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
@@ -27,17 +27,3 @@ tests/e-acsl-runtime/result.i:23:[value] Function h: postcondition got status va
tests/e-acsl-runtime/result.i:23:[value] Function __e_acsl_h: postcondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- x ∈ {0}
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {0}
-[value] Values at end of function g:
-
-[value] Values at end of function __e_acsl_g:
- __retres ∈ {1}
-[value] Values at end of function h:
- __retres ∈ {0}
-[value] Values at end of function __e_acsl_h:
- __retres ∈ {0}
-[value] Values at end of function main:
- __retres ∈ {0}
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 eb2ed0a97e1..46bfad9226f 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
@@ -30,6 +30,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {1}
- __retres ∈ {0}
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 32c0062cd3d..f4b58164d5e 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
@@ -21,6 +21,3 @@ tests/e-acsl-runtime/sizeof.i:10:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {1}
- __retres ∈ {0}
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 6bd184dc25a..4b5936cb976 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
@@ -36,7 +36,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition g
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {7}
- y ∈ {2}
- __retres ∈ {0}
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 a3f17f43635..525695a8f82 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
@@ -20,7 +20,3 @@
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {7}
- y ∈ {2}
- __retres ∈ {0}
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 58bbc088820..27bf5852675 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
@@ -21,6 +21,3 @@ tests/e-acsl-runtime/true.i:10:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {1}
- __retres ∈ {0}
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 58bbc088820..27bf5852675 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
@@ -21,6 +21,3 @@ tests/e-acsl-runtime/true.i:10:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {1}
- __retres ∈ {0}
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 920a2b42daf..b4764b2c963 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
@@ -34,6 +34,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- __retres ∈ {0}
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 e45df4dc9cb..7d4f021a945 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
@@ -21,6 +21,3 @@ tests/e-acsl-runtime/typedef.i:11:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- __retres ∈ {0}
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 36eaf36d15a..0f5e3407939 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
@@ -94,28 +94,3 @@ tests/e-acsl-runtime/valid.c:30:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function f:
- y ∈ {{ &n }}
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {{ &n }}
-[value] Values at end of function g:
- m ∈ {123}
- u ∈ {{ &m }}
- p ∈ {{ &u }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- X ∈ {{ &n }}
- a ∈ ESCAPINGADDR
- b ∈ {{ &n }}
- c ∈ {{ &a }}
- d ∈ {{ &c }}
- n ∈ {0}
- __retres ∈ {0}
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 36eaf36d15a..0f5e3407939 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
@@ -94,28 +94,3 @@ tests/e-acsl-runtime/valid.c:30:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function f:
- y ∈ {{ &n }}
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {{ &n }}
-[value] Values at end of function g:
- m ∈ {123}
- u ∈ {{ &m }}
- p ∈ {{ &u }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- X ∈ {{ &n }}
- a ∈ ESCAPINGADDR
- b ∈ {{ &n }}
- c ∈ {{ &a }}
- d ∈ {{ &c }}
- n ∈ {0}
- __retres ∈ {0}
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 be90ffa809a..44c5a9f2d39 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
@@ -72,16 +72,3 @@ tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for fu
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- a ∈ ESCAPINGADDR
- b ∈ ESCAPINGADDR
- n ∈ {0}
- __retres ∈ {0}
- Frama_C_alloc[0..3] ∈ UNINITIALIZED
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 32ad3893090..bda631e4dd6 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
@@ -78,16 +78,3 @@ tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for fu
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- a ∈ ESCAPINGADDR
- b ∈ ESCAPINGADDR
- n ∈ {0}
- __retres ∈ {0}
- Frama_C_alloc[0..3] ∈ UNINITIALIZED
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 3a199ccfcaa..389e3dfbfb2 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
@@ -41,10 +41,3 @@ tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavio
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- __retres ∈ {0}
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {0}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- __retres ∈ {0}
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 3a199ccfcaa..389e3dfbfb2 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
@@ -41,10 +41,3 @@ tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavio
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- __retres ∈ {0}
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {0}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- __retres ∈ {0}
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 7d060f6ba8a..89273f96587 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
@@ -50,24 +50,3 @@ FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior dealloca
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function new_inversed:
- __fc_heap_status ∈ [--..--]
- i ∈ {3}
- p ∈ {{ &Frama_C_alloc }}
- Frama_C_alloc[bits 0 to 95]# ∈ {1; 2; 3} or UNINITIALIZED repeated %32
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- LAST ∈ {1; 2; 3} or UNINITIALIZED
- x ∈ {3}
- v1[0] ∈ {1}
- [1] ∈ {2}
- [2] ∈ {3}
- v2 ∈ ESCAPINGADDR
- __retres ∈ {0}
- Frama_C_alloc[0..11] ∈ UNINITIALIZED
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 bf837c6ed6d..11a76f18854 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
@@ -59,24 +59,3 @@ FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior dealloca
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function new_inversed:
- __fc_heap_status ∈ [--..--]
- i ∈ {3}
- p ∈ {{ &Frama_C_alloc }}
- Frama_C_alloc[bits 0 to 95]# ∈ {1; 2; 3} or UNINITIALIZED repeated %32
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- LAST ∈ {1; 2; 3} or UNINITIALIZED
- x ∈ {3}
- v1[0] ∈ {1}
- [1] ∈ {2}
- [2] ∈ {3}
- v2 ∈ ESCAPINGADDR
- __retres ∈ {0}
- Frama_C_alloc[0..11] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
index a0452c1b8dd..bcf70a16ce7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
@@ -1,2 +1,2 @@
-OPT: -check -e-acsl -then-on e-acsl -val -no-val-show-progress
-OPT: -check -e-acsl -e-acsl-gmp-only -then-on e-acsl -val -no-val-show-progress
+OPT: -check -e-acsl -then-on e-acsl -val -no-val-show-progress -no-results
+OPT: -check -e-acsl -e-acsl-gmp-only -then-on e-acsl -val -no-val-show-progress -no-results
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 0c116763695..30e38e31738 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -131,9 +131,10 @@ let join ty1 ty2 = match ty1, ty2 with
| No_integral t1, No_integral t2 when Logic_type.equal t1 t2 -> ty1
| No_integral t, ty | ty, No_integral t when Cil.isLogicRealType t -> ty
| No_integral t, _ when Cil.isLogicFloatType t -> ty1
- | No_integral _, No_integral _
- | (Z | Interv _), No_integral _
- | No_integral _, (Interv _ | Z) ->
+ | (Z | Interv _), (No_integral _ as ty)
+ | (No_integral _ as ty), (Interv _ | Z) ->
+ ty
+ | No_integral _, No_integral _ ->
Options.fatal "cannot join %a and %a"
pretty_eacsl_typ ty1
pretty_eacsl_typ ty2
--
GitLab