Commit 53bc0a2e authored by David Bühler's avatar David Bühler
Browse files

[Eva] Adds empty lines to a test to minimize oracle diff on next commit.

parent 40c9bc09
......@@ -6,13 +6,13 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function test_slevel <- main.
Called from partitioning-annots.c:205.
[eva] partitioning-annots.c:170: starting to merge loop iterations
[eva] partitioning-annots.c:175: starting to merge loop iterations
Called from partitioning-annots.c:223.
[eva] partitioning-annots.c:188: starting to merge loop iterations
[eva] partitioning-annots.c:193: 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 partitioning-annots.c:206.
Called from partitioning-annots.c:224.
[eva:loop-unroll:partial] partitioning-annots.c:26: loop not completely unrolled
[eva] partitioning-annots.c:26: starting to merge loop iterations
[eva:loop-unroll:partial] partitioning-annots.c:34: loop not completely unrolled
......@@ -25,7 +25,7 @@
[eva] Recording results for test_unroll
[eva] Done for function test_unroll
[eva] computing for function test_split <- main.
Called from partitioning-annots.c:207.
Called from partitioning-annots.c:225.
[eva] computing for function Frama_C_interval <- test_split <- main.
Called from partitioning-annots.c:73.
[eva] using specification for function Frama_C_interval
......@@ -65,7 +65,7 @@
[eva] Recording results for test_split
[eva] Done for function test_split
[eva] computing for function test_dynamic_split <- main.
Called from partitioning-annots.c:208.
Called from partitioning-annots.c:226.
[eva] partitioning-annots.c:95: Warning:
this partitioning parameter cannot be evaluated safely on all states
[eva] computing for function Frama_C_interval <- test_dynamic_split <- main.
......
......@@ -6,41 +6,41 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function Frama_C_interval <- test_loop_split.
Called from partitioning-annots.c:127.
Called from partitioning-annots.c:145.
[eva] using specification for function Frama_C_interval
[eva] partitioning-annots.c:127:
[eva] partitioning-annots.c:145:
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 partitioning-annots.c:127.
Called from partitioning-annots.c:145.
[eva] Done for function Frama_C_interval
[eva] partitioning-annots.c:125: starting to merge loop iterations
[eva] partitioning-annots.c:143: starting to merge loop iterations
[eva] computing for function Frama_C_interval <- test_loop_split.
Called from partitioning-annots.c:127.
Called from partitioning-annots.c:145.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
Called from partitioning-annots.c:127.
Called from partitioning-annots.c:145.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
Called from partitioning-annots.c:127.
Called from partitioning-annots.c:145.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
Called from partitioning-annots.c:127.
Called from partitioning-annots.c:145.
[eva] Done for function Frama_C_interval
[eva:alarm] partitioning-annots.c:134: Warning:
[eva:alarm] partitioning-annots.c:152: Warning:
accessing uninitialized left-value. assert \initialized(&A[i]);
[eva] partitioning-annots.c:139: Frama_C_show_each: {9}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {8}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {7}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {6}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {5}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {4}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {3}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {2}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {1}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {0}, {42}
[eva] partitioning-annots.c:140: assertion got status valid.
[eva] partitioning-annots.c:143: Frama_C_show_each: {{ "Value 42 not found" }}
[eva] partitioning-annots.c:157: Frama_C_show_each: {9}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {8}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {7}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {6}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {5}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {4}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {3}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {2}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {1}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {0}, {42}
[eva] partitioning-annots.c:158: assertion got status valid.
[eva] partitioning-annots.c:161: 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 ======
......
......@@ -6,13 +6,13 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function Frama_C_interval <- test_history.
Called from partitioning-annots.c:149.
Called from partitioning-annots.c:167.
[eva] using specification for function Frama_C_interval
[eva] partitioning-annots.c:149:
[eva] partitioning-annots.c:167:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] partitioning-annots.c:155: Frama_C_show_each: {0; 1}, {0; 1}
[eva:alarm] partitioning-annots.c:158: Warning:
[eva] partitioning-annots.c:173: Frama_C_show_each: {0; 1}, {0; 1}
[eva:alarm] partitioning-annots.c:176: Warning:
division by zero. assert j ≢ 0;
[eva] Recording results for test_history
[eva] done for function test_history
......
......@@ -6,13 +6,13 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function Frama_C_interval <- test_history.
Called from partitioning-annots.c:149.
Called from partitioning-annots.c:167.
[eva] using specification for function Frama_C_interval
[eva] partitioning-annots.c:149:
[eva] partitioning-annots.c:167:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] partitioning-annots.c:155: Frama_C_show_each: {0}, {0}
[eva] partitioning-annots.c:155: Frama_C_show_each: {1}, {1}
[eva] partitioning-annots.c:173: Frama_C_show_each: {0}, {0}
[eva] partitioning-annots.c:173: Frama_C_show_each: {1}, {1}
[eva] Recording results for test_history
[eva] done for function test_history
[eva] ====== VALUES COMPUTED ======
......
15,16d14
< [eva:alarm] partitioning-annots.c:158: Warning:
< [eva:alarm] partitioning-annots.c:176: Warning:
< division by zero. assert j ≢ 0;
30,31d29
< [eva:alarm] partitioning-annots.c:134: Warning:
< [eva:alarm] partitioning-annots.c:152: Warning:
< accessing uninitialized left-value. assert \initialized(&A[i]);
/* run.config*
STDOPT: #"-eva-default-loop-unroll 10"
STDOPT: +"-main test_split -eva-partition-value k"
STDOPT: #"-main test_loop_split -eva-partition-history 1"
......@@ -109,6 +109,24 @@ void test_dynamic_split()
Frama_C_show_each_no_split(a, b);
}
void test_loop_split()
{
int A[N];
......@@ -165,7 +183,7 @@ void test_slevel()
for (int i = 0; i < N; i++) {
a[i] = 42;
}
//@slevel default;
for (int i = 0; i < N; i++) {
b[i] = 42;
......@@ -188,7 +206,7 @@ void test_slevel()
//@slevel merge;
; // Otherwise previous annotation is ignored
}
//@slevel 0;
;
//@slevel full;
......@@ -207,4 +225,3 @@ void main(void)
test_split();
test_dynamic_split();
}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment