diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/longlong.i b/src/plugins/e-acsl/tests/e-acsl-runtime/longlong.i
index ae2b3343a9667d29683806083254b85615b41bb9..061276f4f38897578768573330ae281e37daa4ab 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/longlong.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/longlong.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: upgrading longlong to GMP
- STDOPT: +"-val-ignore-recursive-calls"
+ STDOPT: +"-no-eva -val-ignore-recursive-calls"
EXECNOW: LOG gen_longlong.c BIN gen_longlong.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/longlong.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_longlong.c > /dev/null && ./gcc_runtime.sh longlong
EXECNOW: LOG gen_longlong2.c BIN gen_longlong2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/longlong.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_longlong2.c > /dev/null && ./gcc_runtime.sh longlong2
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle
index 19e00442d13e9c982f0137f0ad040c8c22bddbbc..690693003a4cb5e6428789685ebfa94282e7f540 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle
@@ -33,8 +33,7 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
__memory_size ∈ [--..--]
[value] using specification for function __store_block
tests/e-acsl-runtime/freeable.c:15:[value] Assertion got status unknown.
-tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value: assert \initialized(&p);
-tests/e-acsl-runtime/freeable.c:15:[kernel] warning: completely indeterminate value in p.
tests/e-acsl-runtime/freeable.c:15:[value] completely invalid value in evaluation of
argument (void *)p
+tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value. assert \initialized(&p);
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle
index 516efe5ad151cf98f9125e5d09804f3fad5dbf94..2f31a65647b8efb236c41fe7b016b2051288870b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle
@@ -25,8 +25,7 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
__memory_size ∈ [--..--]
[value] using specification for function __store_block
tests/e-acsl-runtime/freeable.c:15:[value] Assertion got status unknown.
-tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value: assert \initialized(&p);
-tests/e-acsl-runtime/freeable.c:15:[kernel] warning: completely indeterminate value in p.
tests/e-acsl-runtime/freeable.c:15:[value] completely invalid value in evaluation of
argument (void *)p
+tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value. assert \initialized(&p);
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
index bc5af2b6f639f875bcbaf5b9e5434465faad91db..7b2aac32b7ae44a4c9a77e1b84860e8449e2ad1a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
@@ -26,8 +26,8 @@ tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknow
tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
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 e143e1fd124f46323faa881d6e7078ad735a83ae..feccbdb6ddb785f724c6161f27796d73f1476dc5 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
@@ -28,27 +28,27 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition g
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_get_ui
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
-tests/e-acsl-runtime/linear_search.i:9:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_i_2 < 10;
+tests/e-acsl-runtime/linear_search.i:9:[kernel] warning: accessing out of bounds index. assert __e_acsl_i_2 < 10;
[value] using specification for function __gmpz_add
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
-tests/e-acsl-runtime/linear_search.i:9:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_3 < 10;
+tests/e-acsl-runtime/linear_search.i:9:[kernel] warning: accessing out of bounds index. assert __e_acsl_3 < 10;
[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.
tests/e-acsl-runtime/linear_search.i:14:[value] entering loop for the first time
-tests/e-acsl-runtime/linear_search.i:14:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_j_4 < 10;
+tests/e-acsl-runtime/linear_search.i:14:[kernel] warning: accessing out of bounds index. assert __e_acsl_j_4 < 10;
tests/e-acsl-runtime/linear_search.i:11:[value] entering loop for the first time
-tests/e-acsl-runtime/linear_search.i:11:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_j_2 < 10;
+tests/e-acsl-runtime/linear_search.i:11:[kernel] warning: accessing out of bounds index. assert __e_acsl_j_2 < 10;
tests/e-acsl-runtime/linear_search.i:9:[value] Function search: precondition got status unknown.
tests/e-acsl-runtime/linear_search.i:20:[value] entering loop for the first time
-tests/e-acsl-runtime/linear_search.i:20:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_i_2 < 10;
+tests/e-acsl-runtime/linear_search.i:20:[kernel] warning: accessing out of bounds index. assert __e_acsl_i_2 < 10;
tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
-tests/e-acsl-runtime/linear_search.i:20:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_i_4 < 10;
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:20:[kernel] warning: accessing out of bounds index. assert __e_acsl_i_4 < 10;
tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle
index 79dc90c91ee9e50716f733c5b5f2e6af04df9e1a..62d88b891511673e59d75a1b5235efde47aafe93 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle
@@ -45,9 +45,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:172:[value] Function __gmpz_tdiv_r: preconditio
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:173:[value] Function __gmpz_tdiv_r: precondition got status valid.
[value] using specification for function __gmpz_get_ui
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
-tests/e-acsl-runtime/longlong.i:19:[value] Reading left-value __e_acsl_4.
- It contains a garbled mix of {x} because of Arithmetic.
-tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison:
+tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison.
assert \pointer_comparable((void *)__e_acsl_4, (void *)1);
[value] using specification for function __gmpz_clear
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
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 2992d4c5a824fda7e940fb808af3425ea461d848..5fd7d5e29dbaa816a6764c1c024995dfda165e50 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
@@ -43,9 +43,7 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:171:[value] Function __gmpz_tdiv_r: precondition got status valid.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:172:[value] Function __gmpz_tdiv_r: precondition got status valid.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:173:[value] Function __gmpz_tdiv_r: precondition got status valid.
-tests/e-acsl-runtime/longlong.i:19:[value] Reading left-value __e_acsl_eq.
- It contains a garbled mix of {x} because of Arithmetic.
-tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison:
+tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison.
assert \pointer_comparable((void *)__e_acsl_eq, (void *)0);
[value] using specification for function __gmpz_clear
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.0.res.oracle
index 8f017d69ecda578fedd10674fa0e54f7ff3e4575..37df3cbad2f71abe2dbd53c0726fe49701b16d02 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.0.res.oracle
@@ -19,12 +19,7 @@ tests/e-acsl-runtime/loop.i:21:[value] Loop invariant got status unknown.
[value] Semantic level unrolling superposing up to 100 states
tests/e-acsl-runtime/loop.i:21:[value] entering loop for the first time
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value:
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value.
assert \initialized(&t[__e_acsl_k_2][__e_acsl_l_2]);
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [2400..2848],0%32.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [2880..3328],0%32.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [3360..3808],0%32.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [3840..4288],0%32.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [4320..4768],0%32.
tests/e-acsl-runtime/loop.i:28:[value] Loop invariant got status valid.
[value] done for function main
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 fd67dfecc925ca65d9f4937d6d799e2c790c6dd4..671b142c0380d4f5d044ba919fa3114c0b4e6262 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
@@ -29,22 +29,12 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition go
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
[value] using specification for function __gmpz_get_ui
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_k_2 < 10;
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_l_2 < 15;
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value:
- assert \initialized(&t[__e_acsl_k_2][__e_acsl_l_2]);
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [0..448],0%32.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [480..928],0%32.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [960..1408],0%32.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [1440..1888],0%32.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [1920..2368],0%32.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [2400..2848],0%32.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [2880..3328],0%32.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [3360..3808],0%32.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [3840..4288],0%32.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [4320..4768],0%32.
tests/e-acsl-runtime/loop.i:21:[value] completely invalid value in evaluation of
argument (long)t[__e_acsl_k_2][__e_acsl_l_2]
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index. assert __e_acsl_k_2 < 10;
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index. assert __e_acsl_l_2 < 15;
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value.
+ assert \initialized(&t[__e_acsl_k_2][__e_acsl_l_2]);
[value] using specification for function __gmpz_add
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
@@ -52,9 +42,9 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition g
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/loop.i:19:[value] Loop invariant got status valid.
tests/e-acsl-runtime/loop.i:21:[value] Loop invariant got status unknown.
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_k_4 < 10;
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_l_4 < 15;
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value:
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index. assert __e_acsl_k_4 < 10;
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index. assert __e_acsl_l_4 < 15;
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value.
assert \initialized(&t[__e_acsl_k_4][__e_acsl_l_4]);
[value] using specification for function __gmpz_mul
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid.
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 d044420359cf20d697297fb0d92bf8ebd5635913..c2049ced1b91b42cfcebef28fcac4a7b3f83f6e9 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
@@ -39,7 +39,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: preconditio
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid.
[value] using specification for function __gmpz_get_ui
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
-tests/e-acsl-runtime/ptr.i:16:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_9 < 3;
+tests/e-acsl-runtime/ptr.i:16:[kernel] warning: accessing out of bounds index. assert __e_acsl_9 < 3;
tests/e-acsl-runtime/ptr.i:18:[value] entering loop for the first time
tests/e-acsl-runtime/ptr.i:19:[value] Assertion got status valid.
[value] using specification for function __gmpz_add
@@ -51,7 +51,7 @@ tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:150:[value] Function __gmpz_sub: precondition got status valid.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:151:[value] Function __gmpz_sub: precondition got status valid.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:152:[value] Function __gmpz_sub: precondition got status valid.
-tests/e-acsl-runtime/ptr.i:20:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_15 < 3;
+tests/e-acsl-runtime/ptr.i:20:[kernel] warning: accessing out of bounds index. assert __e_acsl_15 < 3;
tests/e-acsl-runtime/ptr.i:21:[value] Assertion got status valid.
tests/e-acsl-runtime/ptr.i:19:[value] Assertion got status unknown.
tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
index aa0c31766fccb7ac5c5184b95e0bfa375744b28a..91c1eca5dae1dba97289607cf38cc60604e5ca79 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
@@ -66,11 +66,10 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
{FRAMAC_SHARE/libc/stdlib.h:178}.
FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses:
- assert ¬\dangling(&a);
-tests/e-acsl-runtime/valid.c:49:[kernel] warning: completely indeterminate value in a.
tests/e-acsl-runtime/valid.c:49:[value] completely invalid value in evaluation of
argument (void *)a
+tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&a);
tests/e-acsl-runtime/valid.c:50:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:30:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
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 4fb8f5932fda561c87754b0966b9a3d6ec7057a1..0b1fb4930fbc4fb10a6e9b7512f80cc0d4af92c2 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
@@ -58,11 +58,10 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
{FRAMAC_SHARE/libc/stdlib.h:178}.
FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses:
- assert ¬\dangling(&a);
-tests/e-acsl-runtime/valid.c:49:[kernel] warning: completely indeterminate value in a.
tests/e-acsl-runtime/valid.c:49:[value] completely invalid value in evaluation of
argument (void *)a
+tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&a);
tests/e-acsl-runtime/valid.c:50:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:30:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
index 410221074b308e05f965faa37ef8fcfa78fc6a5e..3abdd3f29587cf95fd9346b86d7033d9169a4eb9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
@@ -55,15 +55,13 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
{FRAMAC_SHARE/libc/stdlib.h:178}.
FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses:
- assert ¬\dangling(&a);
-tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in a.
tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
argument (void *)a
-tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses:
- assert ¬\dangling(&b);
-tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in b.
+tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&a);
tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
argument (void *)b
+tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&b);
[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/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index 178c3cb0cfab37c460c49c44f0eb6d512511f7ef..2fc23efb1a94f70d0863a4eafa42a3640a92a30a 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
@@ -53,15 +53,13 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
{FRAMAC_SHARE/libc/stdlib.h:178}.
FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses:
- assert ¬\dangling(&a);
-tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in a.
tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
argument (void *)a
-tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses:
- assert ¬\dangling(&b);
-tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in b.
+tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&a);
tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
argument (void *)b
+tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&b);
[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/valid_in_contract.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.0.res.oracle
index 3d3bab60483259699c068dc6bb03f87b62b51533..47b252b6e28e1f578cc74ae87b45af269855d08b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.0.res.oracle
@@ -16,9 +16,9 @@
[value] using specification for function __valid_read
[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.
-tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
tests/e-acsl-runtime/valid_in_contract.c:21:[value] completely invalid value in evaluation of
argument (void *)l->next
+tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
[value] using specification for function __full_init
[value] using specification for function __delete_block
tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
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 3d3bab60483259699c068dc6bb03f87b62b51533..47b252b6e28e1f578cc74ae87b45af269855d08b 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
@@ -16,9 +16,9 @@
[value] using specification for function __valid_read
[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.
-tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
tests/e-acsl-runtime/valid_in_contract.c:21:[value] completely invalid value in evaluation of
argument (void *)l->next
+tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
[value] using specification for function __full_init
[value] using specification for function __delete_block
tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
index 6f71759d5db5019c2d5d398579d5549896408528..2fa35f293f36e4a511d99c978162b4ae02244ba7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
@@ -45,7 +45,7 @@ FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_all
tests/e-acsl-runtime/vector.c:16:[value] entering loop for the first time
tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown.
-tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
+tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value. assert \initialized(&LAST);
FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
[value] using specification for function __freeable
:0:[value] Assigning imprecise value to __e_acsl_implies.
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 2937859c630bd772d52d272d3fcdb358b8af8036..7d92075851e3a56b79160691ff03270018ff0e28 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
@@ -37,7 +37,7 @@ FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_all
tests/e-acsl-runtime/vector.c:16:[value] entering loop for the first time
tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown.
-tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
+tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value. assert \initialized(&LAST);
[value] using specification for function __gmpz_init_set_si
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp