diff --git a/tests/value/auto_loop_unroll.c b/tests/value/auto_loop_unroll.c
index 5695f8cd18b17580852b9d2998ebdb6ffe4dd1e8..23d10397c36a6edf5e7af2059bf11c1b7df236ea 100644
--- a/tests/value/auto_loop_unroll.c
+++ b/tests/value/auto_loop_unroll.c
@@ -121,6 +121,25 @@ void various_loops () {
}
Frama_C_show_each_32_64(res);
res = 0;
+ /* Loop counter decremented or directly assigned. */
+ for (int i = 28; i > 0;) {
+ if (undet)
+ i = -1; // exits the loop
+ else
+ i--;
+ res++;
+ }
+ Frama_C_show_each_1_28(res);
+ res = 0;
+ for (int i = 28; i > 0;) {
+ if (undet)
+ i = 2; // stay in the loop
+ else
+ i--;
+ res++;
+ }
+ Frama_C_show_each_top(res);
+ res = 0;
}
/* Loops that cannot be unrolled. */
diff --git a/tests/value/oracle/auto_loop_unroll.0.res.oracle b/tests/value/oracle/auto_loop_unroll.0.res.oracle
index 23c479e7089ae8e21d641b1910f3006415fa8962..e100198c7149f3ccc6b1954ef08a8d8a43c13c70 100644
--- a/tests/value/oracle/auto_loop_unroll.0.res.oracle
+++ b/tests/value/oracle/auto_loop_unroll.0.res.oracle
@@ -6,7 +6,7 @@
undet ∈ [--..--]
g ∈ {0}
[eva] computing for function simple_loops <- main.
- Called from tests/value/auto_loop_unroll.c:347.
+ Called from tests/value/auto_loop_unroll.c:366.
[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:348.
+ Called from tests/value/auto_loop_unroll.c:367.
[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;
@@ -134,175 +134,184 @@
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:122:
Frama_C_show_each_32_64: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:125: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:130: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:132:
+ Frama_C_show_each_1_28: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:134: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:139: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:141: Frama_C_show_each_top: [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:349.
-[eva] tests/value/auto_loop_unroll.c:133: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:135: Warning:
+ Called from tests/value/auto_loop_unroll.c:368.
+[eva] tests/value/auto_loop_unroll.c:152: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:154: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:137:
+[eva] tests/value/auto_loop_unroll.c:156:
Frama_C_show_each_imprecise: [0..2147483647]
-[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:
+[eva] tests/value/auto_loop_unroll.c:160: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:161: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:162: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:146: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:165: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:145: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:164: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:148:
+[eva] tests/value/auto_loop_unroll.c:167:
Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:152: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:155: Warning:
+[eva] tests/value/auto_loop_unroll.c:171: 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:157:
+[eva] tests/value/auto_loop_unroll.c:176:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] computing for function incr_g <- complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:162.
+ Called from tests/value/auto_loop_unroll.c:181.
[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] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations
[eva] computing for function incr_g <- complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:162.
+ Called from tests/value/auto_loop_unroll.c:181.
[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:162.
+ Called from tests/value/auto_loop_unroll.c:181.
[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:162.
+ Called from tests/value/auto_loop_unroll.c:181.
[eva] Recording results for incr_g
[eva] Done for function incr_g
-[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:
+[eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g
+[eva:alarm] tests/value/auto_loop_unroll.c:183: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:166:
+[eva] tests/value/auto_loop_unroll.c:185:
Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:171: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:173: Warning:
+[eva] tests/value/auto_loop_unroll.c:190: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:192: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:175:
+[eva] tests/value/auto_loop_unroll.c:194:
Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:179: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:181: Warning:
+[eva] tests/value/auto_loop_unroll.c:198: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:200: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:180: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:199: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:183:
+[eva] tests/value/auto_loop_unroll.c:202:
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:350.
-[eva] tests/value/auto_loop_unroll.c:192: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:193: Warning:
+ Called from tests/value/auto_loop_unroll.c:369.
+[eva] tests/value/auto_loop_unroll.c:211: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:212: 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:
+[eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:216: 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: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:
+[eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:222: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:223: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:203: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:222: Warning:
signed overflow. assert -2147483648 ≤ i_0 - 1;
-[eva] tests/value/auto_loop_unroll.c:206:
+[eva] tests/value/auto_loop_unroll.c:225:
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:
+[eva] tests/value/auto_loop_unroll.c:227: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:228: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:208: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:227: Warning:
signed overflow. assert -2147483648 ≤ i_1 - 1;
-[eva] tests/value/auto_loop_unroll.c:211:
+[eva] tests/value/auto_loop_unroll.c:230:
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:
+[eva] tests/value/auto_loop_unroll.c:233: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:236: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:219:
+[eva] tests/value/auto_loop_unroll.c:238:
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:
+[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] tests/value/auto_loop_unroll.c:226:
+[eva] tests/value/auto_loop_unroll.c:245:
Frama_C_show_each_11_111: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:231: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:232: Warning:
+[eva] tests/value/auto_loop_unroll.c:250: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:251: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:234: Frama_C_show_each_16: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: [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:351.
-[eva] tests/value/auto_loop_unroll.c:243: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:243: Warning:
+ Called from tests/value/auto_loop_unroll.c:370.
+[eva] tests/value/auto_loop_unroll.c:262: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:262: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:244: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:263: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:246: Frama_C_show_each_20: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:248: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:249: Warning:
+[eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:267: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:268: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:248: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:267: Warning:
signed overflow. assert -2147483648 ≤ i - 1;
-[eva] tests/value/auto_loop_unroll.c:251: Frama_C_show_each_21: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: [0..2147483647]
[eva] Recording results for temporary_variables
[eva] Done for function temporary_variables
[eva] computing for function loops_with_goto <- main.
- Called from tests/value/auto_loop_unroll.c:352.
-[eva] tests/value/auto_loop_unroll.c:257: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:258: Warning:
+ Called from tests/value/auto_loop_unroll.c:371.
+[eva] tests/value/auto_loop_unroll.c:276: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:277: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:262: Frama_C_show_each_30: [0..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:267: Warning:
+[eva] tests/value/auto_loop_unroll.c:281: Frama_C_show_each_30: [0..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:286: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:266: starting to merge loop iterations
-[eva] tests/value/auto_loop_unroll.c:271: Frama_C_show_each_top: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:274: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:275: Warning:
+[eva] tests/value/auto_loop_unroll.c:285: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:290: Frama_C_show_each_top: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:293: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:294: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:280: Frama_C_show_each_32: [0..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:284: Warning:
+[eva] tests/value/auto_loop_unroll.c:299: Frama_C_show_each_32: [0..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:303: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:283: starting to merge loop iterations
-[eva] tests/value/auto_loop_unroll.c:288:
+[eva] tests/value/auto_loop_unroll.c:302: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:307:
Frama_C_show_each_33_inf: [0..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:292: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:311: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:291: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:291: Warning:
+[eva] tests/value/auto_loop_unroll.c:310: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:310: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_top: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:299: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:302: Warning:
+[eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_top: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:318: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:321: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:304:
+[eva] tests/value/auto_loop_unroll.c:323:
Frama_C_show_each_0_35: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:307: Warning:
+[eva] tests/value/auto_loop_unroll.c:326: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:326: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:307: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:326: Warning:
signed overflow. assert -2147483648 ≤ i - 1;
-[eva] tests/value/auto_loop_unroll.c:311: Frama_C_show_each_36: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:314: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:317: Warning:
+[eva] tests/value/auto_loop_unroll.c:330: Frama_C_show_each_36: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:333: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:336: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:319: Frama_C_show_each_27: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:338: Frama_C_show_each_27: [0..2147483647]
[eva] Recording results for loops_with_goto
[eva] Done for function loops_with_goto
[eva] computing for function non_natural_loops <- main.
- Called from tests/value/auto_loop_unroll.c:353.
-[eva:alarm] tests/value/auto_loop_unroll.c:330: Warning:
+ Called from tests/value/auto_loop_unroll.c:372.
+[eva:alarm] tests/value/auto_loop_unroll.c:349: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:334: Frama_C_show_each_50: [1..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:338: Warning:
+[eva] tests/value/auto_loop_unroll.c:353: Frama_C_show_each_50: [1..2147483647]
+[eva:alarm] tests/value/auto_loop_unroll.c:357: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:339: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:358: Warning:
signed overflow. assert -2147483648 ≤ i - 1;
-[eva] tests/value/auto_loop_unroll.c:342:
+[eva] tests/value/auto_loop_unroll.c:361:
Frama_C_show_each_1_51: [1..2147483647]
[eva] Recording results for non_natural_loops
[eva] Done for function non_natural_loops
@@ -438,7 +447,7 @@
undet
[inout] Out (internal) for function various_loops:
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
+ i_5; j; i_6; i_7; i_8
[inout] Inputs for function various_loops:
Frama_C_entropy_source; undet; g
[inout] Out (internal) for function main:
diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle
index a614d8402177a8252940c3e51ba1aff4c842dfd5..744bd6d76cf66f5ff736849ce1c8282717e2f85c 100644
--- a/tests/value/oracle/auto_loop_unroll.1.res.oracle
+++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle
@@ -6,7 +6,7 @@
undet ∈ [--..--]
g ∈ {0}
[eva] computing for function simple_loops <- main.
- Called from tests/value/auto_loop_unroll.c:347.
+ Called from tests/value/auto_loop_unroll.c:366.
[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
@@ -25,7 +25,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:348.
+ Called from tests/value/auto_loop_unroll.c:367.
[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.
@@ -278,134 +278,143 @@
[eva] tests/value/auto_loop_unroll.c:112: Frama_C_show_each_120: {120}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:115: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:122: Frama_C_show_each_32_64: [32..64]
+[eva] tests/value/auto_loop_unroll.c:125: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:130: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:132:
+ Frama_C_show_each_1_28: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:134: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:139: Warning:
+ signed overflow. assert res + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:141: Frama_C_show_each_top: [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:349.
-[eva] tests/value/auto_loop_unroll.c:133: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:135: Warning:
+ Called from tests/value/auto_loop_unroll.c:368.
+[eva] tests/value/auto_loop_unroll.c:152: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:154: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:137:
+[eva] tests/value/auto_loop_unroll.c:156:
Frama_C_show_each_imprecise: [0..2147483647]
-[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:
+[eva] tests/value/auto_loop_unroll.c:160: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:161: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:162: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:146: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:165: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:145: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:164: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:148:
+[eva] tests/value/auto_loop_unroll.c:167:
Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:152: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:155: Warning:
+[eva] tests/value/auto_loop_unroll.c:171: 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:157:
+[eva] tests/value/auto_loop_unroll.c:176:
Frama_C_show_each_imprecise: [0..2147483647]
[eva] computing for function incr_g <- complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:162.
+ Called from tests/value/auto_loop_unroll.c:181.
[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] tests/value/auto_loop_unroll.c:180: starting to merge loop iterations
[eva] computing for function incr_g <- complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:162.
+ Called from tests/value/auto_loop_unroll.c:181.
[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:162.
+ Called from tests/value/auto_loop_unroll.c:181.
[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:162.
+ Called from tests/value/auto_loop_unroll.c:181.
[eva] Recording results for incr_g
[eva] Done for function incr_g
-[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:
+[eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g
+[eva] tests/value/auto_loop_unroll.c:181: Reusing old results for call to incr_g
+[eva:alarm] tests/value/auto_loop_unroll.c:183: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:166:
+[eva] tests/value/auto_loop_unroll.c:185:
Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:171: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:173: Warning:
+[eva] tests/value/auto_loop_unroll.c:190: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:192: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:175:
+[eva] tests/value/auto_loop_unroll.c:194:
Frama_C_show_each_imprecise: [0..2147483647]
-[eva] tests/value/auto_loop_unroll.c:179: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:181: Warning:
+[eva] tests/value/auto_loop_unroll.c:198: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:200: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva:alarm] tests/value/auto_loop_unroll.c:180: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:199: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:183:
+[eva] tests/value/auto_loop_unroll.c:202:
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:350.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:192: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:195: Frama_C_show_each_11: {11}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:197: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: {12}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:203: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_0_13: [0..13]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:208: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:211: Frama_C_show_each_0_14: [0..14]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:214: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_0_15: [0..15]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:221: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:221:
+ Called from tests/value/auto_loop_unroll.c:369.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:211: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: {11}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:216: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: {12}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:222: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:225: Frama_C_show_each_0_13: [0..13]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:227: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:230: Frama_C_show_each_0_14: [0..14]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:233: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_0_15: [0..15]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:240: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:240:
Trace partitioning superposing up to 100 states
-[eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11_111: [11..111]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:231: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:234: Frama_C_show_each_16: {16}
+[eva] tests/value/auto_loop_unroll.c:245: Frama_C_show_each_11_111: [11..111]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:250: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: {16}
[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:351.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:243: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:246: Frama_C_show_each_20: {20}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:248: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:251: Frama_C_show_each_21: {21}
+ Called from tests/value/auto_loop_unroll.c:370.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:262: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: {20}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:267: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: {21}
[eva] Recording results for temporary_variables
[eva] Done for function temporary_variables
[eva] computing for function loops_with_goto <- main.
- Called from tests/value/auto_loop_unroll.c:352.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:257: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:262: Frama_C_show_each_30: {30}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:266: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:266: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:267: Warning:
+ Called from tests/value/auto_loop_unroll.c:371.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:276: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:281: Frama_C_show_each_30: {30}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:285: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:285: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:286: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:266:
+[eva] tests/value/auto_loop_unroll.c:285:
Trace partitioning superposing up to 100 states
-[eva] tests/value/auto_loop_unroll.c:271:
+[eva] tests/value/auto_loop_unroll.c:290:
Frama_C_show_each_top: [31..2147483647]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:274: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:280: Frama_C_show_each_32: {32}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:283: Automatic loop unrolling.
-[eva:alarm] tests/value/auto_loop_unroll.c:284: Warning:
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:293: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:299: Frama_C_show_each_32: {32}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:302: Automatic loop unrolling.
+[eva:alarm] tests/value/auto_loop_unroll.c:303: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:288:
+[eva] tests/value/auto_loop_unroll.c:307:
Frama_C_show_each_33_inf: [33..2147483647]
-[eva:alarm] tests/value/auto_loop_unroll.c:292: Warning:
+[eva:alarm] tests/value/auto_loop_unroll.c:311: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:291: starting to merge loop iterations
-[eva:alarm] tests/value/auto_loop_unroll.c:291: Warning:
+[eva] tests/value/auto_loop_unroll.c:310: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:310: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
-[eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_top: [0..2147483647]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:299: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:304: Frama_C_show_each_0_35: [0..35]
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:307: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:311: Frama_C_show_each_36: {36}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:314: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:319: Frama_C_show_each_27: {27}
+[eva] tests/value/auto_loop_unroll.c:315: Frama_C_show_each_top: [0..2147483647]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:318: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:323: Frama_C_show_each_0_35: [0..35]
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:326: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:330: Frama_C_show_each_36: {36}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:333: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:338: Frama_C_show_each_27: {27}
[eva] Recording results for loops_with_goto
[eva] Done for function loops_with_goto
[eva] computing for function non_natural_loops <- main.
- Called from tests/value/auto_loop_unroll.c:353.
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:329: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:334: Frama_C_show_each_50: {50}
-[eva:loop-unroll] tests/value/auto_loop_unroll.c:338: Automatic loop unrolling.
-[eva] tests/value/auto_loop_unroll.c:342: Frama_C_show_each_1_51: [1..51]
+ Called from tests/value/auto_loop_unroll.c:372.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:348: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:353: Frama_C_show_each_50: {50}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:357: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:361: Frama_C_show_each_1_51: [1..51]
[eva] Recording results for non_natural_loops
[eva] Done for function non_natural_loops
[eva] Recording results for main
@@ -540,7 +549,7 @@
undet
[inout] Out (internal) for function various_loops:
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
+ i_5; j; i_6; i_7; i_8
[inout] Inputs for function various_loops:
Frama_C_entropy_source; undet; g
[inout] Out (internal) for function main: