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

[Eva] Adds new tests for the automatic loop unrolling heuristic. 

With loops whose exit conditions are not relational comparisons,
loops with several exit conditions,
and loops where Frama-C introduces temporary variables.
parent 75b7205a
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
tests/value/auto_loop_unroll.c
+ 82
− 21
View file @ c81253b8
......@@ -81,14 +81,6 @@ void various_loops () {
}
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);
......@@ -96,6 +88,12 @@ void various_loops () {
res++;
Frama_C_show_each_40_50(res);
res = 0;
/* Global loop counter. */
for (g = 0; g < 101; g++) {
res++;
}
Frama_C_show_each_101(res);
res = 0;
/* Loop calling some functions that do not modify the loop counter. */
for (int i = 0; i < 25; i++) {
incr_g();
......@@ -113,6 +111,16 @@ void various_loops () {
}
Frama_C_show_each_120(res);
res = 0;
/* Loop counter modified on both sides of a conditional statement. */
for (int i = 0; i < 64;) {
if (undet)
i++;
else
i+=2;
res++;
}
Frama_C_show_each_32_64(res);
res = 0;
}
/* Loops that cannot be unrolled. */
......@@ -120,8 +128,9 @@ void complex_loops () {
/* Loop counter modified through a pointer. */
int res = 0;
int i = 0;
int *p = &i;
while (i < 64) {
int j = 0;
int *p = &j;
while (j < 64) {
(*p)++;
res++;
}
......@@ -147,17 +156,7 @@ void complex_loops () {
}
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();
......@@ -177,16 +176,78 @@ void complex_loops () {
res = 0;
/* Random loop condition. */
i = 0;
while (i < 64 && undet) {
while (i < 64 || undet) {
i++;
res++;
}
Frama_C_show_each_imprecise(res);
}
/* Examples of loops with other exit conditions than simple comparisons.
All loops could be automatically unrolled on the second run, but should
not be unrolled on the first run. */
void various_conditions () {
int i, res = 0;
/* Exit conditions using equality. */
for (i = 11; i; i--) {
res++;
}
Frama_C_show_each_11(res);
res = 0;
for (i = 0; i != 12; i++) {
res++;
}
Frama_C_show_each_12(res);
res = 0;
/* Loops with conjonction of exit conditions. */
for (int i = 13 ; i-- && undet; ) {
res ++;
}
Frama_C_show_each_0_13(res);
res = 0;
for (int i = 14 ; undet && i-- ; ) {
res ++;
}
Frama_C_show_each_0_14(res);
res = 0;
/* Loops with several exit conditions. */
for (int i = 0 ; undet ; i++) {
if (undet || i >= 15)
break;
res ++;
}
Frama_C_show_each_0_15(res);
res = 0;
for (int i = 0; i < 111; i++) {
res++;
if (undet && res > 10)
break;
}
Frama_C_show_each_11_111(res);
res = 0;
}
/* Examples of loops where temporary variables are introduced by Frama-C.
All loops could be automatically unrolled on the second run, but should
not be unrolled on the first run. */
void temporary_variables () {
int i, res = 0;
for (i = 0; i++ < 20;) {
res++;
}
Frama_C_show_each_20(res);
res = 0;
for (i = 21; i--;) {
res++;
}
Frama_C_show_each_21(res);
}
void main () {
simple_loops ();
various_loops ();
complex_loops ();
various_conditions ();
temporary_variables ();
}
tests/value/oracle/auto_loop_unroll.0.res.oracle
+ 155
− 88
View file @ c81253b8
......@@ -6,7 +6,7 @@
undet ∈ [--..--]
g ∈ {0}
[eva] computing for function simple_loops <- main.
Called from tests/value/auto_loop_unroll.c:189.
Called from tests/value/auto_loop_unroll.c:248.
[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;
......@@ -27,7 +27,7 @@
[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.
Called from tests/value/auto_loop_unroll.c:249.
[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;
......@@ -45,164 +45,208 @@
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.
Called from tests/value/auto_loop_unroll.c:86.
[eva] using specification for function Frama_C_interval
[eva] tests/value/auto_loop_unroll.c:94:
[eva] tests/value/auto_loop_unroll.c:86:
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:
[eva] tests/value/auto_loop_unroll.c:87: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:88: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:97:
[eva] tests/value/auto_loop_unroll.c:89:
Frama_C_show_each_40_50: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:92: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:93: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:95: Frama_C_show_each_101: [0..2147483647]
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
Called from tests/value/auto_loop_unroll.c:99.
[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.
Called from tests/value/auto_loop_unroll.c:100.
[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] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
[eva] tests/value/auto_loop_unroll.c:98: starting to merge loop iterations
[eva] computing for function incr_g <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:101.
Called from tests/value/auto_loop_unroll.c:99.
[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.
Called from tests/value/auto_loop_unroll.c:100.
[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:101: 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.
Called from tests/value/auto_loop_unroll.c:99.
[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.
Called from tests/value/auto_loop_unroll.c:100.
[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:101: 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.
Called from tests/value/auto_loop_unroll.c:99.
[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.
Called from tests/value/auto_loop_unroll.c:100.
[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.
Called from tests/value/auto_loop_unroll.c:101.
[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.
Called from tests/value/auto_loop_unroll.c:99.
[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] tests/value/auto_loop_unroll.c:100: Reusing old results for call to incr
[eva] computing for function incr <- various_loops <- main.
Called from tests/value/auto_loop_unroll.c:103.
Called from tests/value/auto_loop_unroll.c:101.
[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.
Called from tests/value/auto_loop_unroll.c:99.
[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] tests/value/auto_loop_unroll.c:100: 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.
Called from tests/value/auto_loop_unroll.c:101.
[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:
[eva] tests/value/auto_loop_unroll.c:103: Frama_C_show_each_25: [0..2147483647]
[eva:loop-unroll] tests/value/auto_loop_unroll.c:108: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:107: starting to merge loop iterations
[eva] tests/value/auto_loop_unroll.c:108: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:109: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:114: Frama_C_show_each_120: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:112: Frama_C_show_each_120: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:115: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:120: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:122:
Frama_C_show_each_32_64: [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
Called from tests/value/auto_loop_unroll.c:250.
[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:
[eva:alarm] tests/value/auto_loop_unroll.c:135: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:139:
[eva] tests/value/auto_loop_unroll.c:137:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:143: starting to merge loop iterations
[eva] tests/value/auto_loop_unroll.c:141: starting to merge loop iterations
[eva] tests/value/auto_loop_unroll.c:142: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:143: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
[eva:alarm] tests/value/auto_loop_unroll.c:146: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
[eva:alarm] tests/value/auto_loop_unroll.c:145: 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:
[eva] tests/value/auto_loop_unroll.c:152: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:155: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:158:
[eva] tests/value/auto_loop_unroll.c:157:
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.
Called from tests/value/auto_loop_unroll.c:162.
[eva] Recording results for incr_g
[eva] Done for function incr_g
[eva] tests/value/auto_loop_unroll.c:161: starting to merge loop iterations
[eva] computing for function incr_g <- complex_loops <- main.
Called from tests/value/auto_loop_unroll.c:162.
[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.
Called from tests/value/auto_loop_unroll.c:162.
[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.
Called from tests/value/auto_loop_unroll.c:162.
[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:
[eva] tests/value/auto_loop_unroll.c:162: Reusing old results for call to incr_g
[eva] tests/value/auto_loop_unroll.c:162: Reusing old results for call to incr_g
[eva:alarm] tests/value/auto_loop_unroll.c:164: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:167:
[eva] tests/value/auto_loop_unroll.c:166:
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:
[eva] tests/value/auto_loop_unroll.c:171: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:173: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:176:
[eva] tests/value/auto_loop_unroll.c:175:
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:
[eva] tests/value/auto_loop_unroll.c:179: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:181: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:184:
[eva:alarm] tests/value/auto_loop_unroll.c:180: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:183:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] Recording results for complex_loops
[eva] Done for function complex_loops
[eva] computing for function various_conditions <- main.
Called from tests/value/auto_loop_unroll.c:251.
[eva] tests/value/auto_loop_unroll.c:192: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:193: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:195: Frama_C_show_each_11: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:197: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:198: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:203: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:204: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva:alarm] tests/value/auto_loop_unroll.c:203: Warning:
signed overflow. assert -2147483648 ≤ i_0 - 1;
[eva] tests/value/auto_loop_unroll.c:206:
Frama_C_show_each_0_13: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:208: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:209: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva:alarm] tests/value/auto_loop_unroll.c:208: Warning:
signed overflow. assert -2147483648 ≤ i_1 - 1;
[eva] tests/value/auto_loop_unroll.c:211:
Frama_C_show_each_0_14: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:214: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:217: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:219:
Frama_C_show_each_0_15: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:221: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:222: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:226:
Frama_C_show_each_11_111: [0..2147483647]
[eva] Recording results for various_conditions
[eva] Done for function various_conditions
[eva] computing for function temporary_variables <- main.
Called from tests/value/auto_loop_unroll.c:252.
[eva] tests/value/auto_loop_unroll.c:235: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:235: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
[eva:alarm] tests/value/auto_loop_unroll.c:236: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: [0..2147483647]
[eva] tests/value/auto_loop_unroll.c:240: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:241: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva:alarm] tests/value/auto_loop_unroll.c:240: Warning:
signed overflow. assert -2147483648 ≤ i - 1;
[eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: [0..2147483647]
[eva] Recording results for temporary_variables
[eva] Done for function temporary_variables
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
......@@ -213,8 +257,9 @@
[eva:final-states] Values at end of function complex_loops:
g ∈ {64}
res ∈ [0..2147483647]
i ∈ [0..64]
p ∈ {{ &i }}
i ∈ [64..2147483647]
j ∈ {64}
p ∈ {{ &j }}
t[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {2}
......@@ -227,9 +272,15 @@
[9] ∈ {9}
[eva:final-states] Values at end of function simple_loops:
res ∈ {100}
[eva:final-states] Values at end of function temporary_variables:
i ∈ [-2147483648..20]
res ∈ [0..2147483647]
[eva:final-states] Values at end of function various_conditions:
i ∈ {12}
res ∈ {0}
[eva:final-states] Values at end of function various_loops:
Frama_C_entropy_source ∈ [--..--]
g ∈ [0..2147483647]
g ∈ [101..2147483647]
res ∈ {0}
x ∈ {24}
k ∈ [0..10]
......@@ -244,6 +295,10 @@
[from] Done for function complex_loops
[from] Computing for function simple_loops
[from] Done for function simple_loops
[from] Computing for function temporary_variables
[from] Done for function temporary_variables
[from] Computing for function various_conditions
[from] Done for function various_conditions
[from] Computing for function various_loops
[from] Computing for function Frama_C_interval <-various_loops
[from] Done for function Frama_C_interval
......@@ -263,9 +318,13 @@
g FROM \nothing
[from] Function simple_loops:
NO EFFECTS
[from] Function temporary_variables:
NO EFFECTS
[from] Function various_conditions:
NO EFFECTS
[from] Function various_loops:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
g FROM g (and SELF)
g FROM \nothing
[from] Function main:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
g FROM \nothing
......@@ -279,16 +338,24 @@
[inout] Inputs for function incr_g:
g
[inout] Out (internal) for function complex_loops:
g; res; i; p; j; t[0..9]
g; res; i; j; p; j_0; 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 temporary_variables:
i; res; tmp; tmp_0
[inout] Inputs for function temporary_variables:
\nothing
[inout] Out (internal) for function various_conditions:
i; res; i_0; tmp; i_1; tmp_0; i_2; i_3
[inout] Inputs for function various_conditions:
undet
[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
Frama_C_entropy_source; g; res; i; i_0; i_1; i_2; x; k; i_3; i_4; t;
i_5; j; i_6
[inout] Inputs for function various_loops:
Frama_C_entropy_source; undet; g
[inout] Out (internal) for function main:
......
tests/value/oracle/auto_loop_unroll.1.res.oracle
+ 204
− 128
View file @ c81253b8
This diff is collapsed.
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