From 1b728bbcf1c80ec4b09305d1a8d7d9c8657e6b9a Mon Sep 17 00:00:00 2001
From: Boris Yakobowski <boris.yakobowski@cea.fr>
Date: Tue, 5 Jan 2016 19:34:35 +0100
Subject: [PATCH] Update oracles to trunk (Value 2); keep Value 1 for recursive
call
---
.../e-acsl/tests/e-acsl-runtime/longlong.i | 2 +-
.../oracle/freeable.0.res.oracle | 3 +--
.../oracle/freeable.1.res.oracle | 3 +--
.../oracle/linear_search.0.res.oracle | 2 +-
.../oracle/linear_search.1.res.oracle | 14 +++++------
.../oracle/longlong.0.res.oracle | 4 +---
.../oracle/longlong.1.res.oracle | 4 +---
.../e-acsl-runtime/oracle/loop.0.res.oracle | 7 +-----
.../e-acsl-runtime/oracle/loop.1.res.oracle | 24 ++++++-------------
.../e-acsl-runtime/oracle/ptr.1.res.oracle | 4 ++--
.../e-acsl-runtime/oracle/valid.0.res.oracle | 5 ++--
.../e-acsl-runtime/oracle/valid.1.res.oracle | 5 ++--
.../oracle/valid_alias.0.res.oracle | 10 ++++----
.../oracle/valid_alias.1.res.oracle | 10 ++++----
.../oracle/valid_in_contract.0.res.oracle | 2 +-
.../oracle/valid_in_contract.1.res.oracle | 2 +-
.../e-acsl-runtime/oracle/vector.0.res.oracle | 2 +-
.../e-acsl-runtime/oracle/vector.1.res.oracle | 2 +-
18 files changed, 39 insertions(+), 66 deletions(-)
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 ae2b3343a96..061276f4f38 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 19e00442d13..690693003a4 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 516efe5ad15..2f31a65647b 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 bc5af2b6f63..7b2aac32b7a 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 e143e1fd124..feccbdb6ddb 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 79dc90c91ee..62d88b89151 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 2992d4c5a82..5fd7d5e29db 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 8f017d69ecd..37df3cbad2f 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 fd67dfecc92..671b142c038 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 d044420359c..c2049ced1b9 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 aa0c31766fc..91c1eca5dae 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 4fb8f5932fd..0b1fb4930fb 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 410221074b3..3abdd3f2958 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 178c3cb0cfa..2fc23efb1a9 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 3d3bab60483..47b252b6e28 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 3d3bab60483..47b252b6e28 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 6f71759d5db..2fa35f293f3 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 2937859c630..7d92075851e 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
--
GitLab