Skip to content
Snippets Groups Projects
Commit 22a598b1 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Uses only 5 runs for test partitioning-annots.

parent 05003f6c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 207 additions and 212 deletions
tests/value/oracle/partitioning-annots.0.res.oracle
+ 107
− 10
View file @ 22a598b1
[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing) [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] Computing initial state
[eva] Initial state computed [eva] Initial state computed
[eva:initial-state] Values of globals at initialization [eva:initial-state] Values of globals at initialization
k ∈ {0} k ∈ {0}
nondet ∈ [--..--] 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 loop not completely unrolled
[eva] tests/value/partitioning-annots.c:26: starting to merge loop iterations [eva] tests/value/partitioning-annots.c:24: starting to merge loop iterations
[eva:loop-unroll] tests/value/partitioning-annots.c:34: [eva:loop-unroll] tests/value/partitioning-annots.c:32:
loop not completely unrolled 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: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:47:
[eva:loop-unroll] tests/value/partitioning-annots.c:49:
loop not completely unrolled loop not completely unrolled
[eva] tests/value/partitioning-annots.c:49: starting to merge loop iterations [eva] tests/value/partitioning-annots.c:47: starting to merge loop iterations
[eva:loop-unroll] tests/value/partitioning-annots.c:54: [eva:loop-unroll] tests/value/partitioning-annots.c:52:
loop not completely unrolled 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] 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] ====== 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: [eva:final-states] Values at end of function test_unroll:
a[0..9] ∈ {42} a[0..9] ∈ {42}
b[0..9] ∈ {42} b[0..9] ∈ {42}
...@@ -46,15 +109,49 @@ ...@@ -46,15 +109,49 @@
[7] ∈ {36} [7] ∈ {36}
[8] ∈ {9} [8] ∈ {9}
[9] ∈ {1} [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] Computing for function test_unroll
[from] Done for function test_unroll [from] Done for function test_unroll
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ====== [from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate: 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: [from] Function test_unroll:
NO EFFECTS 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 ====== [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: [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; 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 i_2; i_3; j_1
[inout] Inputs for function test_unroll: [inout] Inputs for function test_unroll:
\nothing \nothing
[inout] Out (internal) for function main:
Frama_C_entropy_source; k
[inout] Inputs for function main:
Frama_C_entropy_source; k; nondet
tests/value/oracle/partitioning-annots.1.res.oracle
+ 27
− 19
View file @ 22a598b1
...@@ -6,42 +6,50 @@ ...@@ -6,42 +6,50 @@
k ∈ {0} k ∈ {0}
nondet ∈ [--..--] nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_split. [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] 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. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_split. [eva] computing for function Frama_C_interval <- test_split.
Called from tests/value/partitioning-annots.c:74. Called from tests/value/partitioning-annots.c:72.
[eva] tests/value/partitioning-annots.c:74: [eva] tests/value/partitioning-annots.c:72:
function Frama_C_interval: precondition 'order' got status valid. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [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} 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} 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} 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} 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} 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} 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} 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} 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} 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: [eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_before_second_merge: {0; 1}, {2}, {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}, {1}, {0; 1}
[eva] tests/value/partitioning-annots.c:87: [eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_before_second_merge: {0; 1}, {0}, {0; 1} Frama_C_show_each_end: {0}, {0; 1; 2}, {0}
[eva] tests/value/partitioning-annots.c:89:
Frama_C_show_each_end: {0; 1}, {0; 1; 2}, {0; 1}
[eva] Recording results for test_split [eva] Recording results for test_split
[eva] done for function test_split [eva] done for function test_split
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
......
tests/value/oracle/partitioning-annots.2.res.oracle
+ 48
− 57
View file @ 22a598b1
[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing) [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] Computing initial state
[eva] Initial state computed [eva] Initial state computed
[eva:initial-state] Values of globals at initialization [eva:initial-state] Values of globals at initialization
k ∈ {0} k ∈ {0}
nondet ∈ [--..--] nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_split. [eva] computing for function Frama_C_interval <- test_loop_split.
Called from tests/value/partitioning-annots.c:73. Called from tests/value/partitioning-annots.c:105.
[eva] using specification for function Frama_C_interval [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. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_split. [eva] computing for function Frama_C_interval <- test_loop_split.
Called from tests/value/partitioning-annots.c:74. Called from tests/value/partitioning-annots.c:105.
[eva] tests/value/partitioning-annots.c:74: [eva] Done for function Frama_C_interval
function Frama_C_interval: precondition 'order' got status valid. [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] Done for function Frama_C_interval
[eva] tests/value/partitioning-annots.c:80: [eva:alarm] tests/value/partitioning-annots.c:112: Warning:
Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0} accessing uninitialized left-value. assert \initialized(&A[i]);
[eva] tests/value/partitioning-annots.c:83: [eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {9}, {42}
Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1} [eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {8}, {42}
[eva] tests/value/partitioning-annots.c:83: [eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {7}, {42}
Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0} [eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {6}, {42}
[eva] tests/value/partitioning-annots.c:85: [eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {5}, {42}
Frama_C_show_each_before_first_merge: {1}, {2}, {1} [eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {4}, {42}
[eva] tests/value/partitioning-annots.c:85: [eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {3}, {42}
Frama_C_show_each_before_first_merge: {1}, {1}, {1} [eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {2}, {42}
[eva] tests/value/partitioning-annots.c:85: [eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {1}, {42}
Frama_C_show_each_before_first_merge: {1}, {0}, {1} [eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {0}, {42}
[eva] tests/value/partitioning-annots.c:85: [eva] tests/value/partitioning-annots.c:118: assertion got status valid.
Frama_C_show_each_before_first_merge: {0}, {2}, {0} [eva] tests/value/partitioning-annots.c:121:
[eva] tests/value/partitioning-annots.c:85: Frama_C_show_each: {{ "Value 42 not found" }}
Frama_C_show_each_before_first_merge: {0}, {1}, {0} [eva] Recording results for test_loop_split
[eva] tests/value/partitioning-annots.c:85: [eva] done for function test_loop_split
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] ====== VALUES COMPUTED ====== [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 ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
k ∈ {0; 1} A[0] ∈ [0..100]
i ∈ {0; 1} [1..9] ∈ [0..100] or UNINITIALIZED
j ∈ {0; 1; 2} i ∈ [0..10]
[from] Computing for function test_split [from] Computing for function test_loop_split
[from] Computing for function Frama_C_interval <-test_split [from] Computing for function Frama_C_interval <-test_loop_split
[from] Done for function Frama_C_interval [from] Done for function Frama_C_interval
[from] Done for function test_split [from] Done for function test_loop_split
[from] ====== DEPENDENCIES COMPUTED ====== [from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate: These dependencies hold at termination for the executions that terminate:
[from] Function Frama_C_interval: [from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF) Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max \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) Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
k FROM Frama_C_entropy_source
[from] ====== END OF DEPENDENCIES ====== [from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function test_split: [inout] Out (internal) for function test_loop_split:
Frama_C_entropy_source; k; i; j Frama_C_entropy_source; A[0..9]; i
[inout] Inputs for function test_split: [inout] Inputs for function test_loop_split:
Frama_C_entropy_source; k Frama_C_entropy_source
tests/value/oracle/partitioning-annots.3.res.oracle
+ 20
− 48
View file @ 22a598b1
[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing) [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] Computing initial state
[eva] Initial state computed [eva] Initial state computed
[eva:initial-state] Values of globals at initialization [eva:initial-state] Values of globals at initialization
k ∈ {0} k ∈ {0}
nondet ∈ [--..--] nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_loop_split. [eva] computing for function Frama_C_interval <- test_history.
Called from tests/value/partitioning-annots.c:107. Called from tests/value/partitioning-annots.c:127.
[eva] using specification for function Frama_C_interval [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. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split. [eva] tests/value/partitioning-annots.c:133: Frama_C_show_each: {0; 1}, {0; 1}
Called from tests/value/partitioning-annots.c:107. [eva:alarm] tests/value/partitioning-annots.c:136: Warning:
[eva] Done for function Frama_C_interval division by zero. assert j ≢ 0;
[eva] tests/value/partitioning-annots.c:105: starting to merge loop iterations [eva] Recording results for test_history
[eva] computing for function Frama_C_interval <- test_loop_split. [eva] done for function test_history
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] ====== VALUES COMPUTED ====== [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 ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
A[0] ∈ [0..100] i ∈ {0; 1}
[1..9] ∈ [0..100] or UNINITIALIZED j ∈ {0; 1}
i ∈ [0..10] k_0 ∈ {1}
[from] Computing for function test_loop_split [from] Computing for function test_history
[from] Computing for function Frama_C_interval <-test_loop_split [from] Computing for function Frama_C_interval <-test_history
[from] Done for function Frama_C_interval [from] Done for function Frama_C_interval
[from] Done for function test_loop_split [from] Done for function test_history
[from] ====== DEPENDENCIES COMPUTED ====== [from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate: These dependencies hold at termination for the executions that terminate:
[from] Function Frama_C_interval: [from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF) Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max \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) Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] ====== END OF DEPENDENCIES ====== [from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function test_loop_split: [inout] Out (internal) for function test_history:
Frama_C_entropy_source; A[0..9]; i Frama_C_entropy_source; i; j; k_0
[inout] Inputs for function test_loop_split: [inout] Inputs for function test_history:
Frama_C_entropy_source Frama_C_entropy_source
tests/value/oracle/partitioning-annots.4.res.oracle
+ 4
− 5
View file @ 22a598b1
...@@ -6,14 +6,13 @@ ...@@ -6,14 +6,13 @@
k ∈ {0} k ∈ {0}
nondet ∈ [--..--] nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_history. [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] 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. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [eva] Done for function Frama_C_interval
[eva] tests/value/partitioning-annots.c:135: Frama_C_show_each: {0; 1}, {0; 1} [eva] tests/value/partitioning-annots.c:133: Frama_C_show_each: {0}, {0}
[eva:alarm] tests/value/partitioning-annots.c:138: Warning: [eva] tests/value/partitioning-annots.c:133: Frama_C_show_each: {1}, {1}
division by zero. assert j ≢ 0;
[eva] Recording results for test_history [eva] Recording results for test_history
[eva] done for function test_history [eva] done for function test_history
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
......
tests/value/oracle/partitioning-annots.5.res.oracle deleted 100644 → 0
+ 0
− 39
View file @ 05003f6c
[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
tests/value/oracle/partitioning-annots.6.res.oracle deleted 100644 → 0
+ 0
− 30
View file @ 05003f6c
[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
tests/value/partitioning-annots.c
+ 1
− 4
View file @ 22a598b1
/* run.config* /* run.config*
STDOPT: #"-main test_unroll -eva-default-loop-unroll 10" STDOPT: #"-eva-default-loop-unroll 10"
STDOPT: #"-main test_split"
STDOPT: +"-main test_split -eva-partition-value k" STDOPT: +"-main test_split -eva-partition-value k"
STDOPT: #"-main test_loop_split -eva-partition-history 1" STDOPT: #"-main test_loop_split -eva-partition-history 1"
STDOPT: #"-main test_history -eva-partition-history 0" STDOPT: #"-main test_history -eva-partition-history 0"
STDOPT: #"-main test_history -eva-partition-history 1" STDOPT: #"-main test_history -eva-partition-history 1"
STDOPT: #"-main test_slevel"
*/ */
#include "__fc_builtin.h" #include "__fc_builtin.h"
...@@ -187,6 +185,5 @@ void main(void) ...@@ -187,6 +185,5 @@ void main(void)
test_slevel(); test_slevel();
test_unroll(); test_unroll();
test_split(); test_split();
test_loop_split();
} }
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