From 7c86536de618a08d10bac689fcc2a5d21a1ef4ac Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 6 Aug 2020 13:55:22 +0200
Subject: [PATCH] [Eva] fix outdated test
---
.../oracle/partitioning-annots.0.res.oracle | 35 ++++++++--------
.../oracle/partitioning-annots.1.res.oracle | 34 +++++++--------
.../oracle/partitioning-annots.2.res.oracle | 42 +++++++++----------
.../oracle/partitioning-annots.3.res.oracle | 42 +++++++++----------
.../oracle/partitioning-annots.4.res.oracle | 8 ++--
.../oracle/partitioning-annots.5.res.oracle | 8 ++--
.../oracle/partitioning-annots.6.res.oracle | 6 +--
tests/value/partitioning-annots.c | 18 ++++----
8 files changed, 94 insertions(+), 99 deletions(-)
diff --git a/tests/value/oracle/partitioning-annots.0.res.oracle b/tests/value/oracle/partitioning-annots.0.res.oracle
index 6e5eb5de077..058c2bacf2a 100644
--- a/tests/value/oracle/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle/partitioning-annots.0.res.oracle
@@ -12,19 +12,29 @@
loop not completely unrolled
[eva] tests/value/partitioning-annots.c:34: starting to merge loop iterations
[eva] tests/value/partitioning-annots.c:36: starting to merge loop iterations
-[eva:loop-unroll] tests/value/partitioning-annots.c:50:
+[eva:loop-unroll] tests/value/partitioning-annots.c:47:
loop not completely unrolled
-[eva] tests/value/partitioning-annots.c:50: starting to merge loop iterations
-[eva:loop-unroll] tests/value/partitioning-annots.c:66:
+[eva] tests/value/partitioning-annots.c:47: starting to merge loop iterations
+[eva:loop-unroll] tests/value/partitioning-annots.c:52:
loop not completely unrolled
-[eva] tests/value/partitioning-annots.c:66: starting to merge loop iterations
+[eva] tests/value/partitioning-annots.c:52: starting to merge loop iterations
[eva] Recording results for test_unroll
[eva] done for function test_unroll
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function test_unroll:
a[0..9] ∈ {42}
b[0..9] ∈ {42}
- c[0..9] ∈ {0}
+ c[0] ∈ {0}
+ [1] ∈ {1}
+ [2] ∈ {0}
+ [3] ∈ {1}
+ [4] ∈ {0}
+ [5] ∈ {1}
+ [6] ∈ {0}
+ [7] ∈ {1}
+ [8] ∈ {0}
+ [9] ∈ {1}
+ [10..19] ∈ {0; 1} or UNINITIALIZED
d[0..9] ∈ {0}
[10..19] ∈ {0} or UNINITIALIZED
e[0] ∈ {1}
@@ -36,17 +46,6 @@
[7] ∈ {36}
[8] ∈ {9}
[9] ∈ {1}
- f[0] ∈ {0}
- [1] ∈ {1}
- [2] ∈ {0}
- [3] ∈ {1}
- [4] ∈ {0}
- [5] ∈ {1}
- [6] ∈ {0}
- [7] ∈ {1}
- [8] ∈ {0}
- [9] ∈ {1}
- [10..19] ∈ {0; 1} or UNINITIALIZED
[from] Computing for function test_unroll
[from] Done for function test_unroll
[from] ====== DEPENDENCIES COMPUTED ======
@@ -55,7 +54,7 @@
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function test_unroll:
- a[0..9]; b[0..9]; c[0..9]; d[0..19]; e[0..9]; f[0..19]; i; j; i_0;
- j_0; i_1; i_2; i_3; j_1; i_4
+ a[0..9]; b[0..9]; c[0..19]; d[0..19]; e[0..9]; i; j; i_0; j_0; i_1;
+ i_2; i_3; j_1
[inout] Inputs for function test_unroll:
\nothing
diff --git a/tests/value/oracle/partitioning-annots.1.res.oracle b/tests/value/oracle/partitioning-annots.1.res.oracle
index a1f5d1c6916..d50b35a5ec2 100644
--- a/tests/value/oracle/partitioning-annots.1.res.oracle
+++ b/tests/value/oracle/partitioning-annots.1.res.oracle
@@ -6,41 +6,41 @@
k ∈ {0}
nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_split.
- Called from tests/value/partitioning-annots.c:75.
+ Called from tests/value/partitioning-annots.c:71.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:75:
+[eva] tests/value/partitioning-annots.c:71:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_split.
- Called from tests/value/partitioning-annots.c:76.
-[eva] tests/value/partitioning-annots.c:76:
+ Called from tests/value/partitioning-annots.c:72.
+[eva] tests/value/partitioning-annots.c:72:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:82:
+[eva] tests/value/partitioning-annots.c:78:
Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:85:
+[eva] tests/value/partitioning-annots.c:81:
Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1}
-[eva] tests/value/partitioning-annots.c:85:
+[eva] tests/value/partitioning-annots.c:81:
Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:87:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:87:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:87:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:87:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:87:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:87:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:89:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_second_merge: {0; 1}, {2}, {0; 1}
-[eva] tests/value/partitioning-annots.c:89:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_second_merge: {0; 1}, {1}, {0; 1}
-[eva] tests/value/partitioning-annots.c:89:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_second_merge: {0; 1}, {0}, {0; 1}
-[eva] tests/value/partitioning-annots.c:91:
+[eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_end: {0; 1}, {0; 1; 2}, {0; 1}
[eva] Recording results for test_split
[eva] done for function test_split
diff --git a/tests/value/oracle/partitioning-annots.2.res.oracle b/tests/value/oracle/partitioning-annots.2.res.oracle
index 2f28a2b0b9e..523baf86ab3 100644
--- a/tests/value/oracle/partitioning-annots.2.res.oracle
+++ b/tests/value/oracle/partitioning-annots.2.res.oracle
@@ -6,49 +6,49 @@
k ∈ {0}
nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_split.
- Called from tests/value/partitioning-annots.c:75.
+ Called from tests/value/partitioning-annots.c:71.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:75:
+[eva] tests/value/partitioning-annots.c:71:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_split.
- Called from tests/value/partitioning-annots.c:76.
-[eva] tests/value/partitioning-annots.c:76:
+ Called from tests/value/partitioning-annots.c:72.
+[eva] tests/value/partitioning-annots.c:72:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:82:
+[eva] tests/value/partitioning-annots.c:78:
Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:85:
+[eva] tests/value/partitioning-annots.c:81:
Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1}
-[eva] tests/value/partitioning-annots.c:85:
+[eva] tests/value/partitioning-annots.c:81:
Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:87:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:87:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:87:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:87:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:87:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:87:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:89:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_second_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:89:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_second_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:89:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_second_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:89:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_second_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:89:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_second_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:89:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_second_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:91:
+[eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_end: {1}, {0; 1; 2}, {1}
-[eva] tests/value/partitioning-annots.c:91:
+[eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_end: {0}, {0; 1; 2}, {0}
[eva] Recording results for test_split
[eva] done for function test_split
diff --git a/tests/value/oracle/partitioning-annots.3.res.oracle b/tests/value/oracle/partitioning-annots.3.res.oracle
index c2989a6b2d5..c2bbd71dfb8 100644
--- a/tests/value/oracle/partitioning-annots.3.res.oracle
+++ b/tests/value/oracle/partitioning-annots.3.res.oracle
@@ -6,41 +6,41 @@
k ∈ {0}
nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:109.
+ Called from tests/value/partitioning-annots.c:105.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:109:
+[eva] tests/value/partitioning-annots.c:105:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:109.
+ Called from tests/value/partitioning-annots.c:105.
[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:107: starting to merge loop iterations
+[eva] tests/value/partitioning-annots.c:103: starting to merge loop iterations
[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:109.
+ Called from tests/value/partitioning-annots.c:105.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:109.
+ Called from tests/value/partitioning-annots.c:105.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:109.
+ Called from tests/value/partitioning-annots.c:105.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:109.
+ Called from tests/value/partitioning-annots.c:105.
[eva] Done for function Frama_C_interval
-[eva:alarm] tests/value/partitioning-annots.c:116: Warning:
+[eva:alarm] tests/value/partitioning-annots.c:112: Warning:
accessing uninitialized left-value. assert \initialized(&A[i]);
-[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {9}, {42}
-[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {8}, {42}
-[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {7}, {42}
-[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {6}, {42}
-[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {5}, {42}
-[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {4}, {42}
-[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {3}, {42}
-[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {2}, {42}
-[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {1}, {42}
-[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {0}, {42}
-[eva] tests/value/partitioning-annots.c:122: assertion got status valid.
-[eva] tests/value/partitioning-annots.c:125:
+[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {9}, {42}
+[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {8}, {42}
+[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {7}, {42}
+[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {6}, {42}
+[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {5}, {42}
+[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {4}, {42}
+[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {3}, {42}
+[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {2}, {42}
+[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {1}, {42}
+[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {0}, {42}
+[eva] tests/value/partitioning-annots.c:118: assertion got status valid.
+[eva] tests/value/partitioning-annots.c:121:
Frama_C_show_each: {{ "Value 42 not found" }}
[eva] Recording results for test_loop_split
[eva] done for function test_loop_split
diff --git a/tests/value/oracle/partitioning-annots.4.res.oracle b/tests/value/oracle/partitioning-annots.4.res.oracle
index a008cf60525..f319bc5df38 100644
--- a/tests/value/oracle/partitioning-annots.4.res.oracle
+++ b/tests/value/oracle/partitioning-annots.4.res.oracle
@@ -6,13 +6,13 @@
k ∈ {0}
nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_history.
- Called from tests/value/partitioning-annots.c:131.
+ Called from tests/value/partitioning-annots.c:127.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:131:
+[eva] tests/value/partitioning-annots.c:127:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:137: Frama_C_show_each: {0; 1}, {0; 1}
-[eva:alarm] tests/value/partitioning-annots.c:140: Warning:
+[eva] tests/value/partitioning-annots.c:133: Frama_C_show_each: {0; 1}, {0; 1}
+[eva:alarm] tests/value/partitioning-annots.c:136: Warning:
division by zero. assert j ≢ 0;
[eva] Recording results for test_history
[eva] done for function test_history
diff --git a/tests/value/oracle/partitioning-annots.5.res.oracle b/tests/value/oracle/partitioning-annots.5.res.oracle
index 35f1b8e40b2..22626883a48 100644
--- a/tests/value/oracle/partitioning-annots.5.res.oracle
+++ b/tests/value/oracle/partitioning-annots.5.res.oracle
@@ -6,13 +6,13 @@
k ∈ {0}
nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_history.
- Called from tests/value/partitioning-annots.c:131.
+ Called from tests/value/partitioning-annots.c:127.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:131:
+[eva] tests/value/partitioning-annots.c:127:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:137: Frama_C_show_each: {0}, {0}
-[eva] tests/value/partitioning-annots.c:137: Frama_C_show_each: {1}, {1}
+[eva] tests/value/partitioning-annots.c:133: Frama_C_show_each: {0}, {0}
+[eva] tests/value/partitioning-annots.c:133: Frama_C_show_each: {1}, {1}
[eva] Recording results for test_history
[eva] done for function test_history
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/partitioning-annots.6.res.oracle b/tests/value/oracle/partitioning-annots.6.res.oracle
index 99f4e609217..504718adca8 100644
--- a/tests/value/oracle/partitioning-annots.6.res.oracle
+++ b/tests/value/oracle/partitioning-annots.6.res.oracle
@@ -5,9 +5,9 @@
[eva:initial-state] Values of globals at initialization
k ∈ {0}
nondet ∈ [--..--]
-[eva] tests/value/partitioning-annots.c:154: starting to merge loop iterations
-[eva] tests/value/partitioning-annots.c:159: starting to merge loop iterations
-[eva] tests/value/partitioning-annots.c:179:
+[eva] tests/value/partitioning-annots.c:150: starting to merge loop iterations
+[eva] tests/value/partitioning-annots.c:155: starting to merge loop iterations
+[eva] tests/value/partitioning-annots.c:175:
Trace partitioning superposing up to 100 states
[eva] Recording results for test_slevel
[eva] done for function test_slevel
diff --git a/tests/value/partitioning-annots.c b/tests/value/partitioning-annots.c
index 062adc54226..9bb04019ce3 100644
--- a/tests/value/partitioning-annots.c
+++ b/tests/value/partitioning-annots.c
@@ -15,7 +15,7 @@
void test_unroll()
{
- int a[N], b[N], c[N], d[2*N], e[N], f[2*N];
+ int a[N], b[N], c[2*N], d[2*N], e[N];
// The inner loop needs to be unrolled to allow strong updates
// The outer loops doesn't need to be unrolled
@@ -40,10 +40,12 @@ void test_unroll()
// At the end, we must have both arrays a and b to be fully initialized at 42
- // Small loops can be unrolled without giving an unroll parameter
- //@ loop unroll N;
- for (int i = 0 ; i < N ; i++)
- c[i] = 0;
+ // Small loops can be unrolled with the annotation "unroll full".
+ // The actual limit of the number of iterations can be overriden with
+ // the option -eva-default-loop-unroll
+ //@ loop unroll full;
+ for (int i = 0 ; i < 2*N ; i++)
+ c[i] = i % 2;
// Longer loops won't be completely unrolled when not giving a parameter
//@ loop unroll N;
@@ -60,12 +62,6 @@ void test_unroll()
e[j] += e[j-1];
}
}
-
- // Full unroll is limited by option -eva-default-loop-unroll
- //@ loop unroll full;
- for (int i = 0 ; i < 2*N ; i++) {
- f[i] = i % 2;
- }
}
int k;
--
GitLab