From 22a598b1e69de6f501fc3fbc59138e3bf300fabb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 17 May 2021 14:00:32 +0200
Subject: [PATCH] [Eva] Uses only 5 runs for test partitioning-annots.
---
.../oracle/partitioning-annots.0.res.oracle | 117 ++++++++++++++++--
.../oracle/partitioning-annots.1.res.oracle | 46 ++++---
.../oracle/partitioning-annots.2.res.oracle | 105 +++++++---------
.../oracle/partitioning-annots.3.res.oracle | 68 +++-------
.../oracle/partitioning-annots.4.res.oracle | 9 +-
.../oracle/partitioning-annots.5.res.oracle | 39 ------
.../oracle/partitioning-annots.6.res.oracle | 30 -----
tests/value/partitioning-annots.c | 5 +-
8 files changed, 207 insertions(+), 212 deletions(-)
delete mode 100644 tests/value/oracle/partitioning-annots.5.res.oracle
delete mode 100644 tests/value/oracle/partitioning-annots.6.res.oracle
diff --git a/tests/value/oracle/partitioning-annots.0.res.oracle b/tests/value/oracle/partitioning-annots.0.res.oracle
index f6e785c3e31..2c8c96f8d80 100644
--- a/tests/value/oracle/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle/partitioning-annots.0.res.oracle
@@ -1,26 +1,89 @@
[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
-[eva] Analyzing a complete application starting at test_unroll
+[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
k ∈ {0}
nondet ∈ [--..--]
-[eva:loop-unroll] tests/value/partitioning-annots.c:26:
+[eva] computing for function test_slevel <- main.
+ Called from tests/value/partitioning-annots.c:185.
+[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] Recording results for test_slevel
+[eva] Done for function test_slevel
+[eva] computing for function test_unroll <- main.
+ Called from tests/value/partitioning-annots.c:186.
+[eva:loop-unroll] tests/value/partitioning-annots.c:24:
loop not completely unrolled
-[eva] tests/value/partitioning-annots.c:26: starting to merge loop iterations
-[eva:loop-unroll] tests/value/partitioning-annots.c:34:
+[eva] tests/value/partitioning-annots.c:24: starting to merge loop iterations
+[eva:loop-unroll] tests/value/partitioning-annots.c:32:
loop not completely unrolled
+[eva] tests/value/partitioning-annots.c:32: starting to merge loop iterations
[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:49:
+[eva:loop-unroll] tests/value/partitioning-annots.c:47:
loop not completely unrolled
-[eva] tests/value/partitioning-annots.c:49: starting to merge loop iterations
-[eva:loop-unroll] tests/value/partitioning-annots.c:54:
+[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:54: 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] Done for function test_unroll
+[eva] computing for function test_split <- main.
+ Called from tests/value/partitioning-annots.c:187.
+[eva] computing for function Frama_C_interval <- test_split <- main.
+ Called from tests/value/partitioning-annots.c:71.
+[eva] using specification for function Frama_C_interval
+[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 <- main.
+ 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:78:
+ Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
+[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:81:
+ Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
+[eva] tests/value/partitioning-annots.c:83:
+ Frama_C_show_each_before_first_merge: {1}, {2}, {1}
+[eva] tests/value/partitioning-annots.c:83:
+ Frama_C_show_each_before_first_merge: {1}, {1}, {1}
+[eva] tests/value/partitioning-annots.c:83:
+ Frama_C_show_each_before_first_merge: {1}, {0}, {1}
+[eva] tests/value/partitioning-annots.c:83:
+ Frama_C_show_each_before_first_merge: {0}, {2}, {0}
+[eva] tests/value/partitioning-annots.c:83:
+ Frama_C_show_each_before_first_merge: {0}, {1}, {0}
+[eva] tests/value/partitioning-annots.c:83:
+ Frama_C_show_each_before_first_merge: {0}, {0}, {0}
+[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:85:
+ Frama_C_show_each_before_second_merge: {0; 1}, {1}, {0; 1}
+[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: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
+[eva] Recording results for main
+[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function test_slevel:
+ a[0..9] ∈ {42}
+ b[0..9] ∈ {42} or UNINITIALIZED
+ c[0..3] ∈ {33; 42}
+ [4..9] ∈ {33; 42} or UNINITIALIZED
+ d[0..9] ∈ {33; 42}
+ e[0..3] ∈ {33; 42}
+[eva:final-states] Values at end of function test_split:
+ Frama_C_entropy_source ∈ [--..--]
+ k ∈ {0; 1}
+ i ∈ {0; 1}
+ j ∈ {0; 1; 2}
[eva:final-states] Values at end of function test_unroll:
a[0..9] ∈ {42}
b[0..9] ∈ {42}
@@ -46,15 +109,49 @@
[7] ∈ {36}
[8] ∈ {9}
[9] ∈ {1}
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
+ k ∈ {0; 1}
+[from] Computing for function test_slevel
+[from] Done for function test_slevel
+[from] Computing for function test_split
+[from] Computing for function Frama_C_interval <-test_split
+[from] Done for function Frama_C_interval
+[from] Done for function test_split
[from] Computing for function test_unroll
[from] Done for function test_unroll
+[from] Computing for function main
+[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function test_slevel:
+ NO EFFECTS
+[from] Function test_split:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ k FROM Frama_C_entropy_source
[from] Function test_unroll:
NO EFFECTS
+[from] Function main:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ k FROM Frama_C_entropy_source
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function test_slevel:
+ a[0..9]; b[0..9]; c[0..9]; d[0..9]; e[0..3]; i; i_0; i_1; i_2; i_3
+[inout] Inputs for function test_slevel:
+ nondet
+[inout] Out (internal) for function test_split:
+ Frama_C_entropy_source; k; i; j
+[inout] Inputs for function test_split:
+ Frama_C_entropy_source; k
[inout] Out (internal) for function test_unroll:
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
+[inout] Out (internal) for function main:
+ Frama_C_entropy_source; k
+[inout] Inputs for function main:
+ Frama_C_entropy_source; k; nondet
diff --git a/tests/value/oracle/partitioning-annots.1.res.oracle b/tests/value/oracle/partitioning-annots.1.res.oracle
index 3a489cae4e1..4c75b70926a 100644
--- a/tests/value/oracle/partitioning-annots.1.res.oracle
+++ b/tests/value/oracle/partitioning-annots.1.res.oracle
@@ -6,42 +6,50 @@
k ∈ {0}
nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_split.
- Called from tests/value/partitioning-annots.c:73.
+ Called from tests/value/partitioning-annots.c:71.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:73:
+[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:74.
-[eva] tests/value/partitioning-annots.c:74:
+ 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:80:
+[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:83:
+[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:83:
+[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:85:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:85:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:85:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:85:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:85:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:85:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_first_merge: {0}, {0}, {0}
+[eva] tests/value/partitioning-annots.c:85:
+ Frama_C_show_each_before_second_merge: {1}, {2}, {1}
+[eva] tests/value/partitioning-annots.c:85:
+ Frama_C_show_each_before_second_merge: {1}, {1}, {1}
+[eva] tests/value/partitioning-annots.c:85:
+ Frama_C_show_each_before_second_merge: {1}, {0}, {1}
+[eva] tests/value/partitioning-annots.c:85:
+ Frama_C_show_each_before_second_merge: {0}, {2}, {0}
+[eva] tests/value/partitioning-annots.c:85:
+ Frama_C_show_each_before_second_merge: {0}, {1}, {0}
+[eva] tests/value/partitioning-annots.c:85:
+ Frama_C_show_each_before_second_merge: {0}, {0}, {0}
[eva] tests/value/partitioning-annots.c:87:
- Frama_C_show_each_before_second_merge: {0; 1}, {2}, {0; 1}
-[eva] tests/value/partitioning-annots.c:87:
- Frama_C_show_each_before_second_merge: {0; 1}, {1}, {0; 1}
+ Frama_C_show_each_end: {1}, {0; 1; 2}, {1}
[eva] tests/value/partitioning-annots.c:87:
- Frama_C_show_each_before_second_merge: {0; 1}, {0}, {0; 1}
-[eva] tests/value/partitioning-annots.c:89:
- Frama_C_show_each_end: {0; 1}, {0; 1; 2}, {0; 1}
+ Frama_C_show_each_end: {0}, {0; 1; 2}, {0}
[eva] Recording results for test_split
[eva] done for function test_split
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/partitioning-annots.2.res.oracle b/tests/value/oracle/partitioning-annots.2.res.oracle
index dde4f315592..c2bbd71dfb8 100644
--- a/tests/value/oracle/partitioning-annots.2.res.oracle
+++ b/tests/value/oracle/partitioning-annots.2.res.oracle
@@ -1,77 +1,68 @@
[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
-[eva] Analyzing a complete application starting at test_split
+[eva] Analyzing a complete application starting at test_loop_split
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
k ∈ {0}
nondet ∈ [--..--]
-[eva] computing for function Frama_C_interval <- test_split.
- Called from tests/value/partitioning-annots.c:73.
+[eva] computing for function Frama_C_interval <- test_loop_split.
+ Called from tests/value/partitioning-annots.c:105.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:73:
+[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_split.
- Called from tests/value/partitioning-annots.c:74.
-[eva] tests/value/partitioning-annots.c:74:
- function Frama_C_interval: precondition 'order' got status valid.
+[eva] computing for function Frama_C_interval <- test_loop_split.
+ Called from tests/value/partitioning-annots.c:105.
+[eva] Done for function Frama_C_interval
+[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: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: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: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:105.
[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:80:
- Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:83:
- Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1}
-[eva] tests/value/partitioning-annots.c:83:
- Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:85:
- Frama_C_show_each_before_first_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:85:
- Frama_C_show_each_before_first_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:85:
- Frama_C_show_each_before_first_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:85:
- Frama_C_show_each_before_first_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:85:
- Frama_C_show_each_before_first_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:85:
- Frama_C_show_each_before_first_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:87:
- Frama_C_show_each_before_second_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:87:
- Frama_C_show_each_before_second_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:87:
- Frama_C_show_each_before_second_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:87:
- Frama_C_show_each_before_second_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:87:
- Frama_C_show_each_before_second_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:87:
- Frama_C_show_each_before_second_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:89:
- Frama_C_show_each_end: {1}, {0; 1; 2}, {1}
-[eva] tests/value/partitioning-annots.c:89:
- Frama_C_show_each_end: {0}, {0; 1; 2}, {0}
-[eva] Recording results for test_split
-[eva] done for function test_split
+[eva:alarm] tests/value/partitioning-annots.c:112: Warning:
+ accessing uninitialized left-value. assert \initialized(&A[i]);
+[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
[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function test_split:
+[eva:final-states] Values at end of function test_loop_split:
Frama_C_entropy_source ∈ [--..--]
- k ∈ {0; 1}
- i ∈ {0; 1}
- j ∈ {0; 1; 2}
-[from] Computing for function test_split
-[from] Computing for function Frama_C_interval <-test_split
+ A[0] ∈ [0..100]
+ [1..9] ∈ [0..100] or UNINITIALIZED
+ i ∈ [0..10]
+[from] Computing for function test_loop_split
+[from] Computing for function Frama_C_interval <-test_loop_split
[from] Done for function Frama_C_interval
-[from] Done for function test_split
+[from] Done for function test_loop_split
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
-[from] Function test_split:
+[from] Function test_loop_split:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
- k FROM Frama_C_entropy_source
[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function test_split:
- Frama_C_entropy_source; k; i; j
-[inout] Inputs for function test_split:
- Frama_C_entropy_source; k
+[inout] Out (internal) for function test_loop_split:
+ Frama_C_entropy_source; A[0..9]; i
+[inout] Inputs for function test_loop_split:
+ Frama_C_entropy_source
diff --git a/tests/value/oracle/partitioning-annots.3.res.oracle b/tests/value/oracle/partitioning-annots.3.res.oracle
index 0726db35992..f319bc5df38 100644
--- a/tests/value/oracle/partitioning-annots.3.res.oracle
+++ b/tests/value/oracle/partitioning-annots.3.res.oracle
@@ -1,68 +1,40 @@
[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
-[eva] Analyzing a complete application starting at test_loop_split
+[eva] Analyzing a complete application starting at test_history
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
k ∈ {0}
nondet ∈ [--..--]
-[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:107.
+[eva] computing for function Frama_C_interval <- test_history.
+ Called from tests/value/partitioning-annots.c:127.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:107:
+[eva] tests/value/partitioning-annots.c:127:
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:107.
-[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:105: starting to merge loop iterations
-[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:107.
-[eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:107.
-[eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:107.
-[eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:107.
-[eva] Done for function Frama_C_interval
-[eva:alarm] tests/value/partitioning-annots.c:114: Warning:
- accessing uninitialized left-value. assert \initialized(&A[i]);
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {9}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {8}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {7}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {6}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {5}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {4}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {3}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {2}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {1}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {0}, {42}
-[eva] tests/value/partitioning-annots.c:120: assertion got status valid.
-[eva] tests/value/partitioning-annots.c:123:
- Frama_C_show_each: {{ "Value 42 not found" }}
-[eva] Recording results for test_loop_split
-[eva] done for function test_loop_split
+[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
[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function test_loop_split:
+[eva:final-states] Values at end of function test_history:
Frama_C_entropy_source ∈ [--..--]
- A[0] ∈ [0..100]
- [1..9] ∈ [0..100] or UNINITIALIZED
- i ∈ [0..10]
-[from] Computing for function test_loop_split
-[from] Computing for function Frama_C_interval <-test_loop_split
+ i ∈ {0; 1}
+ j ∈ {0; 1}
+ k_0 ∈ {1}
+[from] Computing for function test_history
+[from] Computing for function Frama_C_interval <-test_history
[from] Done for function Frama_C_interval
-[from] Done for function test_loop_split
+[from] Done for function test_history
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
-[from] Function test_loop_split:
+[from] Function test_history:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function test_loop_split:
- Frama_C_entropy_source; A[0..9]; i
-[inout] Inputs for function test_loop_split:
+[inout] Out (internal) for function test_history:
+ Frama_C_entropy_source; i; j; k_0
+[inout] Inputs for function test_history:
Frama_C_entropy_source
diff --git a/tests/value/oracle/partitioning-annots.4.res.oracle b/tests/value/oracle/partitioning-annots.4.res.oracle
index 95b65614d11..22626883a48 100644
--- a/tests/value/oracle/partitioning-annots.4.res.oracle
+++ b/tests/value/oracle/partitioning-annots.4.res.oracle
@@ -6,14 +6,13 @@
k ∈ {0}
nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_history.
- Called from tests/value/partitioning-annots.c:129.
+ Called from tests/value/partitioning-annots.c:127.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:129:
+[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:135: Frama_C_show_each: {0; 1}, {0; 1}
-[eva:alarm] tests/value/partitioning-annots.c:138: Warning:
- division by zero. assert j ≢ 0;
+[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.5.res.oracle b/tests/value/oracle/partitioning-annots.5.res.oracle
deleted file mode 100644
index e2009fcbb60..00000000000
--- a/tests/value/oracle/partitioning-annots.5.res.oracle
+++ /dev/null
@@ -1,39 +0,0 @@
-[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
-[eva] Analyzing a complete application starting at test_history
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- k ∈ {0}
- nondet ∈ [--..--]
-[eva] computing for function Frama_C_interval <- test_history.
- Called from tests/value/partitioning-annots.c:129.
-[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:129:
- function Frama_C_interval: precondition 'order' got status valid.
-[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:135: Frama_C_show_each: {0}, {0}
-[eva] tests/value/partitioning-annots.c:135: Frama_C_show_each: {1}, {1}
-[eva] Recording results for test_history
-[eva] done for function test_history
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function test_history:
- Frama_C_entropy_source ∈ [--..--]
- i ∈ {0; 1}
- j ∈ {0; 1}
- k_0 ∈ {1}
-[from] Computing for function test_history
-[from] Computing for function Frama_C_interval <-test_history
-[from] Done for function Frama_C_interval
-[from] Done for function test_history
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_interval:
- Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
- \result FROM Frama_C_entropy_source; min; max
-[from] Function test_history:
- Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function test_history:
- Frama_C_entropy_source; i; j; k_0
-[inout] Inputs for function test_history:
- Frama_C_entropy_source
diff --git a/tests/value/oracle/partitioning-annots.6.res.oracle b/tests/value/oracle/partitioning-annots.6.res.oracle
deleted file mode 100644
index 405717c890d..00000000000
--- a/tests/value/oracle/partitioning-annots.6.res.oracle
+++ /dev/null
@@ -1,30 +0,0 @@
-[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
-[eva] Analyzing a complete application starting at test_slevel
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- k ∈ {0}
- nondet ∈ [--..--]
-[eva] tests/value/partitioning-annots.c:152: starting to merge loop iterations
-[eva] tests/value/partitioning-annots.c:157: starting to merge loop iterations
-[eva] Recording results for test_slevel
-[eva] done for function test_slevel
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function test_slevel:
- a[0..9] ∈ {42}
- b[0..9] ∈ {42} or UNINITIALIZED
- c[0..3] ∈ {33; 42}
- [4..9] ∈ {33; 42} or UNINITIALIZED
- d[0..9] ∈ {33; 42}
- e[0..3] ∈ {33; 42}
-[from] Computing for function test_slevel
-[from] Done for function test_slevel
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function test_slevel:
- NO EFFECTS
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function test_slevel:
- a[0..9]; b[0..9]; c[0..9]; d[0..9]; e[0..3]; i; i_0; i_1; i_2; i_3
-[inout] Inputs for function test_slevel:
- nondet
diff --git a/tests/value/partitioning-annots.c b/tests/value/partitioning-annots.c
index 4aa95cc322d..c84390f8c98 100644
--- a/tests/value/partitioning-annots.c
+++ b/tests/value/partitioning-annots.c
@@ -1,12 +1,10 @@
/* run.config*
- STDOPT: #"-main test_unroll -eva-default-loop-unroll 10"
- STDOPT: #"-main test_split"
+ STDOPT: #"-eva-default-loop-unroll 10"
STDOPT: +"-main test_split -eva-partition-value k"
STDOPT: #"-main test_loop_split -eva-partition-history 1"
STDOPT: #"-main test_history -eva-partition-history 0"
STDOPT: #"-main test_history -eva-partition-history 1"
- STDOPT: #"-main test_slevel"
*/
#include "__fc_builtin.h"
@@ -187,6 +185,5 @@ void main(void)
test_slevel();
test_unroll();
test_split();
- test_loop_split();
}
--
GitLab