From 2dc27a4abfae56738a24d814e94c8e9a4d37d726 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 9 Jan 2019 14:53:36 +0100
Subject: [PATCH] [Eva] Fixes tests and updates test oracles.
---
tests/builtins/oracle/allocated.0.res.oracle | 14 ++++++--------
tests/idct/oracle/ieee_1180_1990.res.oracle | 10 ++++++++--
tests/value/inversion2.i | 2 +-
tests/value/oracle/inversion2.res.oracle | 2 +-
tests/value/precise_locations.i | 2 +-
5 files changed, 17 insertions(+), 13 deletions(-)
diff --git a/tests/builtins/oracle/allocated.0.res.oracle b/tests/builtins/oracle/allocated.0.res.oracle
index 9a9940ee92a..53996c93021 100644
--- a/tests/builtins/oracle/allocated.0.res.oracle
+++ b/tests/builtins/oracle/allocated.0.res.oracle
@@ -233,34 +233,31 @@
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
[eva:malloc] tests/builtins/allocated.c:127:
resizing variable `__malloc_main_l127' (0..31/95) to fit 0..63/127
-[eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3}
+[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] tests/builtins/allocated.c:127:
strong free on bases: {__malloc_main_l127}
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
[eva:malloc] tests/builtins/allocated.c:127:
resizing variable `__malloc_main_l127' (0..31/127) to fit 0..63/159
-[eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3; 4}
+[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] tests/builtins/allocated.c:127:
strong free on bases: {__malloc_main_l127}
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
[eva:malloc] tests/builtins/allocated.c:127:
resizing variable `__malloc_main_l127' (0..31/159) to fit 0..63/191
-[eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3; 4; 5}
+[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] tests/builtins/allocated.c:127:
strong free on bases: {__malloc_main_l127}
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
[eva:malloc] tests/builtins/allocated.c:127:
resizing variable `__malloc_main_l127' (0..31/191) to fit 0..63/319
-[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..9]
+[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
[eva:malloc] tests/builtins/allocated.c:127:
strong free on bases: {__malloc_main_l127}
-[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
-[eva:malloc] tests/builtins/allocated.c:127:
- resizing variable `__malloc_main_l127' (0..31/319) to fit 0..63/319
[eva] Recording results for main
[eva] done for function main
[eva] tests/builtins/allocated.c:27:
@@ -279,7 +276,8 @@
size ∈ [1..100]
pb ∈ ESCAPINGADDR
__retres ∈ {0}
- __malloc_w_main_l82[0..2] ∈ [7..27] or UNINITIALIZED
+ __malloc_w_main_l82[0..1] ∈ [7..2147483647] or UNINITIALIZED
+ [2] ∈ [7..27] or UNINITIALIZED
[from] Computing for function main
[from] Computing for function malloc <-main
[from] Done for function malloc
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 36bad43db98..2c7e41c81de 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -369,6 +369,8 @@
[eva] tests/idct/ieee_1180_1990.c:215: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:234: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:233: starting to merge loop iterations
+[eva] tests/idct/ieee_1180_1990.c:235: Warning:
+ 2's complement assumed for overflow
[eva] computing for function IEEE_1180_1990_dctf <- main.
Called from tests/idct/ieee_1180_1990.c:236.
[eva] Recording results for IEEE_1180_1990_dctf
@@ -446,6 +448,8 @@
[eva] tests/idct/ieee_1180_1990.c:277: Warning:
2's complement assumed for overflow
[eva] tests/idct/ieee_1180_1990.c:261: starting to merge loop iterations
+[eva] tests/idct/ieee_1180_1990.c:281: Warning:
+ 2's complement assumed for overflow
[eva] tests/idct/ieee_1180_1990.c:280: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:279: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:282:
@@ -518,6 +522,8 @@
[eva] tests/idct/ieee_1180_1990.c:323: Warning:
2's complement assumed for overflow
[eva] tests/idct/ieee_1180_1990.c:307: starting to merge loop iterations
+[eva] tests/idct/ieee_1180_1990.c:327: Warning:
+ 2's complement assumed for overflow
[eva] tests/idct/ieee_1180_1990.c:326: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:325: starting to merge loop iterations
[eva] tests/idct/ieee_1180_1990.c:328:
@@ -898,7 +904,7 @@
[eva:final-states] Values at end of function IEEE_1180_1990_mkbk:
i ∈ {8}
j ∈ {8} or UNINITIALIZED
- M1[0..7][0..7] ∈ [-2147483647..2147483647]
+ M1[0..7][0..7] ∈ [--..--]
IEEE_1180_1990_rand_randx ∈ [--..--]
[eva:final-states] Values at end of function IEEE_1180_1990_dctf:
i ∈ {8}
@@ -951,7 +957,7 @@
omse ∈ [--..--] or UNINITIALIZED
ome ∈ [--..--] or UNINITIALIZED
err ∈ [--..--] or UNINITIALIZED
- M1[0..7][0..7] ∈ [-2147483647..2147483647]
+ M1[0..7][0..7] ∈ [--..--]
IEEE_1180_1990_rand_randx ∈ [--..--]
IEEE_1180_1990_dctf_mcos[0..7][0..7] ∈
[-1.0000000000000000*2^-1 .. 1.0000000000000000*2^-1]
diff --git a/tests/value/inversion2.i b/tests/value/inversion2.i
index d1f31a4f0e4..e9a935555be 100644
--- a/tests/value/inversion2.i
+++ b/tests/value/inversion2.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-then -wlevel 4"
+ STDOPT: +"-then -eva-widening-delay 4 -eva-widening-period 3"
*/
int T[3] = {3,1,2};
diff --git a/tests/value/oracle/inversion2.res.oracle b/tests/value/oracle/inversion2.res.oracle
index 60312c7f172..1c380b36ac4 100644
--- a/tests/value/oracle/inversion2.res.oracle
+++ b/tests/value/oracle/inversion2.res.oracle
@@ -21,7 +21,7 @@
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
- G ∈ {5; 7; 15; 99}
+ G ∈ [5..99],1%2
i ∈ {3}
j ∈ {1; 2; 3; 4; 77}
[from] Computing for function main
diff --git a/tests/value/precise_locations.i b/tests/value/precise_locations.i
index 3f3051f0dc6..06340dba48a 100644
--- a/tests/value/precise_locations.i
+++ b/tests/value/precise_locations.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-then -inout -load-module report -report -then -plevel 250"
+ STDOPT: +"-eva-widening-period 3 -then -inout -load-module report -report -then -plevel 250"
*/
struct s {
--
GitLab