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

[Eva] New test file for the automatic loop unrolling heuristic.

parent 37a1c7b4
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/value/auto_loop_unroll.c 0 → 100644
+ 192
− 0
View file @ f26cf0af
/* run.config*
STDOPT: +"-eva-auto-loop-unroll 10"
STDOPT: +"-eva-auto-loop-unroll 128"
*/
/* Tests the automatic loop unrolling heuristic. */
#include <__fc_builtin.h>
volatile int undet;
int g = 0;
void incr_g () {
g++;
}
int incr (int i) {
return i+1;
}
void simple_loops () {
int res = 0;
/* This loop should be automatically unrolled on the second run. */
for (int i = 0; i < 100; i++) {
res++;
}
Frama_C_show_each_auto(res);
res = 0;
/* This loop should not be automatically unrolled. */
for (int i = 0; i < 1000; i++) {
res++;
}
Frama_C_show_each_imprecise(res);
res = 0;
/* The annotation has priority over the automatic loop unrolling:
this loop should never be unrolled. */
/*@ loop unroll 0; */
for (int i = 0; i < 100; i++) {
res++;
}
Frama_C_show_each_imprecise(res);
res = 0;
/* The annnotation has priority over the automatic loop unrolling:
this loop should always be unrolled. */
/*@ loop unroll 100; */
for (int i = 0; i < 100; i++) {
res++;
}
Frama_C_show_each_singleton(res);
}
/* Examples of various loops that should be automatically unrolled
on the second run, but not on the first. */
void various_loops () {
int res = 0;
/* Decreasing loop counter. */
for (int i = 64; i > 0; i--)
res++;
Frama_C_show_each_64(res);
res = 0;
/* Decrements the loop counter by 3. */
for (int i = 120; i > 0; i -= 3)
res++;
Frama_C_show_each_40(res);
res = 0;
/* Several increments of the loop counter. */
for (int i = 0; i < 160; i++) {
i += 2;
res++;
i--;
}
Frama_C_show_each_80(res);
res = 0;
/* Random increments of the loop counter. */
for (int i = 0; i < 160;) {
res++;
if (undet)
i += 2;
else
i += 5;
}
Frama_C_show_each_32_80(res);
res = 0;
/* Other loop breaking condition. */
for (int i = 0; i < 111; i++) {
res++;
if (undet && res > 10)
break;
}
Frama_C_show_each_11_111(res);
res = 0;
/* More complex loop condition. */
int x = 24;
int k = Frama_C_interval(0, 10);
for (int i = 75; i + x > 2 * k; i -= 2)
res++;
Frama_C_show_each_40_50(res);
res = 0;
/* Loop calling some functions that do not modify the loop counter. */
for (int i = 0; i < 25; i++) {
incr_g();
int t = incr(i);
res = incr(res);
}
Frama_C_show_each_25(res);
res = 0;
/* Nested loops. */
res = 0;
for (int i = 0; i < 16; i++) {
for (int j = 0; j < i; j++) {
res++;
}
}
Frama_C_show_each_120(res);
res = 0;
}
/* Loops that cannot be unrolled. */
void complex_loops () {
/* Loop counter modified through a pointer. */
int res = 0;
int i = 0;
int *p = &i;
while (i < 64) {
(*p)++;
res++;
}
Frama_C_show_each_imprecise(res);
/* Loop counter modified within a nested loop. */
res = 0;
i = 0;
while (i < 64) {
for (int j = 0; j < i; j++) {
i++;
}
res++;
i++;
}
Frama_C_show_each_imprecise(res);
/* Loop counter incremented under a condition. */
res = 0;
i = 0;
while (i < 10) {
if (undet)
i++;
res++;
}
Frama_C_show_each_imprecise(res);
res = 0;
i = 0;
while (i < 10) {
if (undet)
i++;
else
i++;
res++;
}
Frama_C_show_each_imprecise(res);
/* Loop counter modified by a function. */
res = 0;
g = 0;
while (g < 64) {
incr_g();
g++;
res++;
}
Frama_C_show_each_imprecise(res);
res = 0;
/* Too complex loop condition. */
int t[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
i = 0;
while (t[i] < 6) {
i++;
res++;
}
Frama_C_show_each_imprecise(res);
res = 0;
/* Random loop condition. */
i = 0;
while (i < 64 && undet) {
i++;
res++;
}
Frama_C_show_each_imprecise(res);
}
void main () {
simple_loops ();
various_loops ();
complex_loops ();
}
tests/value/oracle/auto_loop_unroll.0.res.oracle 0 → 100644
+ 297
− 0
View file @ f26cf0af
[kernel] Parsing tests/value/auto_loop_unroll.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
undet ∈ [--..--]
g ∈ {0}
[eva] computing for function simple_loops <- main.
Called from tests/value/auto_loop_unroll.c:189.
[eva] tests/value/auto_loop_unroll.c:24: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:25: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:27: Frama_C_show_each_auto: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:30: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:31: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:33:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:38: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:39: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:41:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:46:
Trace partitioning superposing up to 100 states
[eva] tests/value/auto_loop_unroll.c:49: Frama_C_show_each_singleton: {100}
[eva] Recording results for simple_loops
[eva] Done for function simple_loops
[eva] computing for function various_loops <- main.
Called from tests/value/auto_loop_unroll.c:190.
[eva] tests/value/auto_loop_unroll.c:57: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:58: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:62: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:63: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:64: Frama_C_show_each_40: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:67: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:69: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:72: Frama_C_show_each_80: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:75: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:76: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:82:
Frama_C_show_each_32_80: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:85: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:86: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:90:
Frama_C_show_each_11_111: [0..2147483647]
[eva] computing for function Frama_C_interval <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:94.
[eva] using specification for function Frama_C_interval
[eva] tests/value/auto_loop_unroll.c:94:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] tests/value/auto_loop_unroll.c:95: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:96: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:97:
Frama_C_show_each_40_50: [0..2147483647]
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] tests/value/auto_loop_unroll.c:100: starting to merge loop iterations
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:103.
[eva] Recording results for incr
[eva] Done for function incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:103.
[eva] Recording results for incr
[eva] Done for function incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva:alarm] tests/value/auto_loop_unroll.c:14: Warning:
signed overflow. assert g + 1 ≤ 2147483647;
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:103.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr_g
[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:103.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr_g
[eva] tests/value/auto_loop_unroll.c:102: Reusing old results for call to incr
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:103.
[eva:alarm] tests/value/auto_loop_unroll.c:18: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:105: Frama_C_show_each_25: [0..2147483647]
[eva:loop-unroll] tests/value/auto_loop_unroll.c:110: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:109: starting to merge loop iterations
[eva] tests/value/auto_loop_unroll.c:110: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:111: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:114: Frama_C_show_each_120: [0..2147483647]
[eva] Recording results for various_loops
[eva] Done for function various_loops
[eva] computing for function complex_loops <- main.
Called from tests/value/auto_loop_unroll.c:191.
[eva] tests/value/auto_loop_unroll.c:124: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:126: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:128:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:132: starting to merge loop iterations
[eva] tests/value/auto_loop_unroll.c:133: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:134: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
[eva:alarm] tests/value/auto_loop_unroll.c:137: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
[eva:alarm] tests/value/auto_loop_unroll.c:136: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:139:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:143: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:146: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:148:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:151: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:156: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:158:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
[eva] tests/value/auto_loop_unroll.c:162: starting to merge loop iterations
[eva] computing for function incr_g <- complex_loops <- main.
Called from tests/value/auto_loop_unroll.c:163.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr_g <- complex_loops <- main.
Called from tests/value/auto_loop_unroll.c:163.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr_g <- complex_loops <- main.
Called from tests/value/auto_loop_unroll.c:163.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
[eva:alarm] tests/value/auto_loop_unroll.c:165: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:167:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:172: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:174: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:176:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:182: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:184:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] Recording results for complex_loops
[eva] Done for function complex_loops
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function incr:
__retres ∈ [1..2147483647]
[eva:final-states] Values at end of function incr_g:
g ∈ [1..2147483647]
[eva:final-states] Values at end of function complex_loops:
g ∈ {64}
res ∈ [0..2147483647]
i ∈ [0..64]
p ∈ {{ &i }}
t[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {2}
[3] ∈ {3}
[4] ∈ {4}
[5] ∈ {5}
[6] ∈ {6}
[7] ∈ {7}
[8] ∈ {8}
[9] ∈ {9}
[eva:final-states] Values at end of function simple_loops:
res ∈ {100}
[eva:final-states] Values at end of function various_loops:
Frama_C_entropy_source ∈ [--..--]
g ∈ [0..2147483647]
res ∈ {0}
x ∈ {24}
k ∈ [0..10]
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
g ∈ {64}
[from] Computing for function incr
[from] Done for function incr
[from] Computing for function incr_g
[from] Done for function incr_g
[from] Computing for function complex_loops
[from] Done for function complex_loops
[from] Computing for function simple_loops
[from] Done for function simple_loops
[from] Computing for function various_loops
[from] Computing for function Frama_C_interval <-various_loops
[from] Done for function Frama_C_interval
[from] Done for function various_loops
[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 incr:
\result FROM i
[from] Function incr_g:
g FROM g
[from] Function complex_loops:
g FROM \nothing
[from] Function simple_loops:
NO EFFECTS
[from] Function various_loops:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
g FROM g (and SELF)
[from] Function main:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
g FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function incr:
__retres
[inout] Inputs for function incr:
\nothing
[inout] Out (internal) for function incr_g:
g
[inout] Inputs for function incr_g:
g
[inout] Out (internal) for function complex_loops:
g; res; i; p; j; t[0..9]
[inout] Inputs for function complex_loops:
undet; g
[inout] Out (internal) for function simple_loops:
res; i; i_0; i_1; i_2
[inout] Inputs for function simple_loops:
\nothing
[inout] Out (internal) for function various_loops:
Frama_C_entropy_source; g; res; i; i_0; i_1; i_2; i_3; x; k; i_4; i_5;
t; i_6; j
[inout] Inputs for function various_loops:
Frama_C_entropy_source; undet; g
[inout] Out (internal) for function main:
Frama_C_entropy_source; g
[inout] Inputs for function main:
Frama_C_entropy_source; undet; g
tests/value/oracle/auto_loop_unroll.1.res.oracle 0 → 100644
+ 431
− 0
View file @ f26cf0af
[kernel] Parsing tests/value/auto_loop_unroll.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
undet ∈ [--..--]
g ∈ {0}
[eva] computing for function simple_loops <- main.
Called from tests/value/auto_loop_unroll.c:189.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:24: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:24:
Trace partitioning superposing up to 100 states
[eva] tests/value/auto_loop_unroll.c:27: Frama_C_show_each_auto: {100}
[eva] tests/value/auto_loop_unroll.c:30: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:31: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:33:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:38: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:39: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:41:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:49: Frama_C_show_each_singleton: {100}
[eva] Recording results for simple_loops
[eva] Done for function simple_loops
[eva] computing for function various_loops <- main.
Called from tests/value/auto_loop_unroll.c:190.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:57: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: {64}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:62: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:64: Frama_C_show_each_40: {40}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:67: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:72: Frama_C_show_each_80: {80}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:75: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:75:
Trace partitioning superposing up to 100 states
[eva] tests/value/auto_loop_unroll.c:82: Frama_C_show_each_32_80: [32..80]
[eva:loop-unroll] tests/value/auto_loop_unroll.c:85: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:90: Frama_C_show_each_11_111: [11..111]
[eva] computing for function Frama_C_interval <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:94.
[eva] using specification for function Frama_C_interval
[eva] tests/value/auto_loop_unroll.c:94:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva:loop-unroll] tests/value/auto_loop_unroll.c:95: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:97: Frama_C_show_each_40_50: [40..50]
[eva:loop-unroll] tests/value/auto_loop_unroll.c:100: Automatic loop unrolling.
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:102.
[eva] Recording results for incr
[eva] Done for function incr
[eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
[eva] tests/value/auto_loop_unroll.c:105: Frama_C_show_each_25: {25}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:109: Automatic loop unrolling.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:110: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:114: Frama_C_show_each_120: {120}
[eva] Recording results for various_loops
[eva] Done for function various_loops
[eva] computing for function complex_loops <- main.
Called from tests/value/auto_loop_unroll.c:191.
[eva] tests/value/auto_loop_unroll.c:124: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:126: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:128:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:132: starting to merge loop iterations
[eva] tests/value/auto_loop_unroll.c:133: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:134: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
[eva:alarm] tests/value/auto_loop_unroll.c:137: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
[eva:alarm] tests/value/auto_loop_unroll.c:136: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:139:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:143: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:146: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:148:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:151: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:156: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:158:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
[eva] tests/value/auto_loop_unroll.c:162: starting to merge loop iterations
[eva] computing for function incr_g <- complex_loops <- main.
Called from tests/value/auto_loop_unroll.c:163.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr_g <- complex_loops <- main.
Called from tests/value/auto_loop_unroll.c:163.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] computing for function incr_g <- complex_loops <- main.
Called from tests/value/auto_loop_unroll.c:163.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
[eva] tests/value/auto_loop_unroll.c:163: Reusing old results for call to incr_g
[eva:alarm] tests/value/auto_loop_unroll.c:165: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:167:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:172: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:174: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:176:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:182: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:184:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] Recording results for complex_loops
[eva] Done for function complex_loops
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function incr:
__retres ∈ [1..25]
[eva:final-states] Values at end of function incr_g:
g ∈ [1..63]
[eva:final-states] Values at end of function complex_loops:
g ∈ {64}
res ∈ [0..2147483647]
i ∈ [0..64]
p ∈ {{ &i }}
t[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {2}
[3] ∈ {3}
[4] ∈ {4}
[5] ∈ {5}
[6] ∈ {6}
[7] ∈ {7}
[8] ∈ {8}
[9] ∈ {9}
[eva:final-states] Values at end of function simple_loops:
res ∈ {100}
[eva:final-states] Values at end of function various_loops:
Frama_C_entropy_source ∈ [--..--]
g ∈ {25}
res ∈ {0}
x ∈ {24}
k ∈ [0..10]
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
g ∈ {64}
[from] Computing for function incr
[from] Done for function incr
[from] Computing for function incr_g
[from] Done for function incr_g
[from] Computing for function complex_loops
[from] Done for function complex_loops
[from] Computing for function simple_loops
[from] Done for function simple_loops
[from] Computing for function various_loops
[from] Computing for function Frama_C_interval <-various_loops
[from] Done for function Frama_C_interval
[from] Done for function various_loops
[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 incr:
\result FROM i
[from] Function incr_g:
g FROM g
[from] Function complex_loops:
g FROM \nothing
[from] Function simple_loops:
NO EFFECTS
[from] Function various_loops:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
g FROM g (and SELF)
[from] Function main:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
g FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function incr:
__retres
[inout] Inputs for function incr:
\nothing
[inout] Out (internal) for function incr_g:
g
[inout] Inputs for function incr_g:
g
[inout] Out (internal) for function complex_loops:
g; res; i; p; j; t[0..9]
[inout] Inputs for function complex_loops:
undet; g
[inout] Out (internal) for function simple_loops:
res; i; i_0; i_1; i_2
[inout] Inputs for function simple_loops:
\nothing
[inout] Out (internal) for function various_loops:
Frama_C_entropy_source; g; res; i; i_0; i_1; i_2; i_3; x; k; i_4; i_5;
t; i_6; j
[inout] Inputs for function various_loops:
Frama_C_entropy_source; undet; g
[inout] Out (internal) for function main:
Frama_C_entropy_source; g
[inout] Inputs for function main:
Frama_C_entropy_source; undet; g
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