From 043929c1069cc40a64ff0da3ae6780d3beb7cf2f Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 15 Oct 2013 08:05:38 +0000
Subject: [PATCH] [E-ACSL] fixes oracles according to Value's changes
---
src/plugins/e-acsl/TODO | 2 ++
.../tests/e-acsl-runtime/oracle/loop.1.res.oracle | 5 +++++
.../tests/e-acsl-runtime/oracle/loop.res.oracle | 11 ++++++++++-
3 files changed, 17 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 2652369061c..27b9451be0c 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -10,6 +10,8 @@
- [Guillaume] ajouter les annotations de RTE dans la table des annotations
(avec une option)
- [David Mentré] tset
+- [Guillaume] voir les valeurs quand la spec échoue, voir Boogaloo@RV'13 à ce
+ sujet
#####################
# E-ACSL CONSTRUCTS #
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 67423ac21da..2a29c1cd035 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
@@ -27,6 +27,11 @@ 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:
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
[value] ====== VALUES COMPUTED ======
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 fe99e93ad60..c71a59ea778 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
@@ -42,7 +42,16 @@ tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index [
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..4768],0%32.
+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] all evaluations are invalid for function call argument
(long)t[__e_acsl_k_2][__e_acsl_l_2]
[value] using specification for function __gmpz_add
--
GitLab