diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle index 2532c0705debdae0c04bd3b145d657e2f7699ac2..157883e6ff0133b739ede4af930676acbf2c8643 100644 --- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle +++ b/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle @@ -6,42 +6,42 @@ nondet ∈ [--..--] [eva] computing for function f1 <- main. Called from tests/loop_analysis/with_value.i:187. -[eva] tests/loop_analysis/with_value.i:6: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:6: Automatic loop unrolling. [eva] Recording results for f1 [eva] Done for function f1 [eva] computing for function f2 <- main. Called from tests/loop_analysis/with_value.i:188. -[eva] tests/loop_analysis/with_value.i:10: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:10: Automatic loop unrolling. [eva] Recording results for f2 [eva] Done for function f2 [eva] computing for function f3 <- main. Called from tests/loop_analysis/with_value.i:189. -[eva] tests/loop_analysis/with_value.i:14: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:14: Automatic loop unrolling. [eva] Recording results for f3 [eva] Done for function f3 [eva] computing for function f4 <- main. Called from tests/loop_analysis/with_value.i:190. -[eva] tests/loop_analysis/with_value.i:18: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:18: Automatic loop unrolling. [eva] Recording results for f4 [eva] Done for function f4 [eva] computing for function f5 <- main. Called from tests/loop_analysis/with_value.i:191. -[eva] tests/loop_analysis/with_value.i:22: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:22: Automatic loop unrolling. [eva] Recording results for f5 [eva] Done for function f5 [eva] computing for function f6 <- main. Called from tests/loop_analysis/with_value.i:192. -[eva] tests/loop_analysis/with_value.i:26: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:26: Automatic loop unrolling. [eva] Recording results for f6 [eva] Done for function f6 [eva] computing for function f7 <- main. Called from tests/loop_analysis/with_value.i:193. -[eva] tests/loop_analysis/with_value.i:30: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:30: Automatic loop unrolling. [eva] Recording results for f7 [eva] Done for function f7 [eva] computing for function f8 <- main. Called from tests/loop_analysis/with_value.i:194. -[eva] tests/loop_analysis/with_value.i:34: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:34: Automatic loop unrolling. [eva] Recording results for f8 [eva] Done for function f8 [eva] computing for function g1 <- main. @@ -102,7 +102,7 @@ [eva] Done for function g8 [eva] computing for function h1 <- main. Called from tests/loop_analysis/with_value.i:203. -[eva] tests/loop_analysis/with_value.i:70: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:70: Automatic loop unrolling. [eva] Recording results for h1 [eva] Done for function h1 [eva] computing for function h1 <- main. @@ -111,7 +111,7 @@ [eva] Done for function h1 [eva] computing for function h2 <- main. Called from tests/loop_analysis/with_value.i:205. -[eva] tests/loop_analysis/with_value.i:74: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:74: Automatic loop unrolling. [eva] Recording results for h2 [eva] Done for function h2 [eva] computing for function h2 <- main. @@ -120,7 +120,7 @@ [eva] Done for function h2 [eva] computing for function h3 <- main. Called from tests/loop_analysis/with_value.i:207. -[eva] tests/loop_analysis/with_value.i:78: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:78: Automatic loop unrolling. [eva] Recording results for h3 [eva] Done for function h3 [eva] computing for function h3 <- main. @@ -129,7 +129,7 @@ [eva] Done for function h3 [eva] computing for function h4 <- main. Called from tests/loop_analysis/with_value.i:209. -[eva] tests/loop_analysis/with_value.i:82: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:82: Automatic loop unrolling. [eva] Recording results for h4 [eva] Done for function h4 [eva] computing for function h4 <- main. @@ -138,7 +138,7 @@ [eva] Done for function h4 [eva] computing for function h5 <- main. Called from tests/loop_analysis/with_value.i:211. -[eva] tests/loop_analysis/with_value.i:86: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:86: Automatic loop unrolling. [eva] Recording results for h5 [eva] Done for function h5 [eva] computing for function h5 <- main. @@ -147,7 +147,7 @@ [eva] Done for function h5 [eva] computing for function h6 <- main. Called from tests/loop_analysis/with_value.i:213. -[eva] tests/loop_analysis/with_value.i:90: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:90: Automatic loop unrolling. [eva] Recording results for h6 [eva] Done for function h6 [eva] computing for function h6 <- main. @@ -156,7 +156,7 @@ [eva] Done for function h6 [eva] computing for function h7 <- main. Called from tests/loop_analysis/with_value.i:215. -[eva] tests/loop_analysis/with_value.i:94: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:94: Automatic loop unrolling. [eva] Recording results for h7 [eva] Done for function h7 [eva] computing for function h7 <- main. @@ -165,7 +165,7 @@ [eva] Done for function h7 [eva] computing for function h8 <- main. Called from tests/loop_analysis/with_value.i:217. -[eva] tests/loop_analysis/with_value.i:98: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:98: Automatic loop unrolling. [eva] Recording results for h8 [eva] Done for function h8 [eva] computing for function h8 <- main. @@ -174,40 +174,50 @@ [eva] Done for function h8 [eva] computing for function i1 <- main. Called from tests/loop_analysis/with_value.i:219. -[eva] tests/loop_analysis/with_value.i:102: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:102: + Automatic loop unrolling. [eva] Recording results for i1 [eva] Done for function i1 [eva] computing for function i2 <- main. Called from tests/loop_analysis/with_value.i:220. -[eva] tests/loop_analysis/with_value.i:106: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:106: + Automatic loop unrolling. [eva] Recording results for i2 [eva] Done for function i2 [eva] computing for function i3 <- main. Called from tests/loop_analysis/with_value.i:221. -[eva] tests/loop_analysis/with_value.i:110: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:110: + Automatic loop unrolling. [eva] Recording results for i3 [eva] Done for function i3 [eva] computing for function i4 <- main. Called from tests/loop_analysis/with_value.i:222. -[eva] tests/loop_analysis/with_value.i:114: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:114: + Automatic loop unrolling. [eva] Recording results for i4 [eva] Done for function i4 [eva] computing for function j1 <- main. Called from tests/loop_analysis/with_value.i:223. -[eva] tests/loop_analysis/with_value.i:118: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:118: + Automatic loop unrolling. [eva] Recording results for j1 [eva] Done for function j1 [eva] computing for function j2 <- main. Called from tests/loop_analysis/with_value.i:224. -[eva] tests/loop_analysis/with_value.i:122: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:122: + Automatic loop unrolling. [eva] Recording results for j2 [eva] Done for function j2 [eva] computing for function j3 <- main. Called from tests/loop_analysis/with_value.i:225. +[eva:loop-unroll] tests/loop_analysis/with_value.i:126: + Automatic loop unrolling. [eva] Recording results for j3 [eva] Done for function j3 [eva] computing for function j4 <- main. Called from tests/loop_analysis/with_value.i:226. +[eva:loop-unroll] tests/loop_analysis/with_value.i:130: + Automatic loop unrolling. [eva] Recording results for j4 [eva] Done for function j4 [eva] computing for function j1 <- main. @@ -220,17 +230,16 @@ [eva] Done for function j2 [eva] computing for function j3 <- main. Called from tests/loop_analysis/with_value.i:229. -[eva] tests/loop_analysis/with_value.i:126: starting to merge loop iterations [eva] Recording results for j3 [eva] Done for function j3 [eva] computing for function j4 <- main. Called from tests/loop_analysis/with_value.i:230. -[eva] tests/loop_analysis/with_value.i:130: starting to merge loop iterations [eva] Recording results for j4 [eva] Done for function j4 [eva] computing for function f2_u_const <- main. Called from tests/loop_analysis/with_value.i:232. -[eva] tests/loop_analysis/with_value.i:134: starting to merge loop iterations +[eva:loop-unroll] tests/loop_analysis/with_value.i:134: + Automatic loop unrolling. [eva] Recording results for f2_u_const [eva] Done for function f2_u_const [eva] computing for function ne1 <- main. @@ -321,15 +330,15 @@ [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function f1: - i ∈ [7..2147483647] + i ∈ {7} [eva:final-states] Values at end of function f2: - i ∈ [8..2147483647] + i ∈ {8} [eva:final-states] Values at end of function f2_u_const: i ∈ {8} [eva:final-states] Values at end of function f3: - i ∈ [8..2147483647] + i ∈ {8} [eva:final-states] Values at end of function f4: - i ∈ [7..2147483647] + i ∈ {7} [eva:final-states] Values at end of function f5: i ∈ {3} [eva:final-states] Values at end of function f6: @@ -355,13 +364,13 @@ [eva:final-states] Values at end of function g8: i ∈ [-2147483646..1] [eva:final-states] Values at end of function h1: - i ∈ [12..2147483647] + i ∈ {12; 22} [eva:final-states] Values at end of function h2: - i ∈ [13..2147483647] + i ∈ {13; 23} [eva:final-states] Values at end of function h3: - i ∈ [13..2147483647] + i ∈ {13; 23} [eva:final-states] Values at end of function h4: - i ∈ [12..2147483647] + i ∈ {12; 22} [eva:final-states] Values at end of function h5: i ∈ {1} [eva:final-states] Values at end of function h6: @@ -371,21 +380,21 @@ [eva:final-states] Values at end of function h8: i ∈ {1} [eva:final-states] Values at end of function i1: - i ∈ [15..2147483647] + i ∈ {15} [eva:final-states] Values at end of function i2: - i ∈ [16..2147483647] + i ∈ {16} [eva:final-states] Values at end of function i3: - i ∈ {1; 2; 3; 4; 5; 6; 7} + i ∈ {7} [eva:final-states] Values at end of function i4: - i ∈ {1; 2; 3; 4; 5; 6} + i ∈ {6} [eva:final-states] Values at end of function j1: - i ∈ [37..2147483647] + i ∈ {37; 47} [eva:final-states] Values at end of function j2: - i ∈ [38..2147483647] + i ∈ {38; 48} [eva:final-states] Values at end of function j3: - i ∈ [1..26] + i ∈ {17; 26} [eva:final-states] Values at end of function j4: - i ∈ [1..26] + i ∈ {16; 26} [eva:final-states] Values at end of function ne1: i ∈ {46} [eva:final-states] Values at end of function ne2: diff --git a/src/plugins/nonterm/tests/nonterm/oracle/callstack.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/callstack.res.oracle index 93e52b1abcc2748f95222a8ff3613add99c96c80..5e82cdb8fda5a0675c7bf9585616f288df1692b0 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/callstack.res.oracle +++ b/src/plugins/nonterm/tests/nonterm/oracle/callstack.res.oracle @@ -4,6 +4,7 @@ [eva] Initial state computed [eva:initial-state] Values of globals at initialization +[eva:loop-unroll] tests/nonterm/callstack.i:11: Automatic loop unrolling. [eva] computing for function g <- main. Called from tests/nonterm/callstack.i:12. [eva] computing for function f <- g <- main. diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n1.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n1.res.oracle index d767e6bc3ffa986cc0ffe1cffb7fa7c2606d882a..12c0c0fbb32a1a559eafd2e983481be9f00fc2d9 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/n1.res.oracle +++ b/src/plugins/nonterm/tests/nonterm/oracle/n1.res.oracle @@ -4,14 +4,12 @@ [eva] Initial state computed [eva:initial-state] Values of globals at initialization -[eva] tests/nonterm/n1.i:6: starting to merge loop iterations -[eva:alarm] tests/nonterm/n1.i:7: Warning: - signed overflow. assert res + i ≤ 2147483647; +[eva:loop-unroll] tests/nonterm/n1.i:6: Automatic loop unrolling. [eva] Recording results for main [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function main: i ∈ {10} - res ∈ [0..2147483647] + res ∈ {45} __retres ∈ {0} [nonterm] Analysis done. diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n7.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n7.res.oracle index 49675ab4fccdb6e01ffacc1f686da9e2b97922c8..18c410fdd7c018993bc7aad14464ec921a75482f 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/n7.res.oracle +++ b/src/plugins/nonterm/tests/nonterm/oracle/n7.res.oracle @@ -4,7 +4,7 @@ [eva] Initial state computed [eva:initial-state] Values of globals at initialization -[eva] tests/nonterm/n7.i:5: starting to merge loop iterations +[eva:loop-unroll] tests/nonterm/n7.i:5: Automatic loop unrolling. [eva] Recording results for main [eva] done for function main [eva] ====== VALUES COMPUTED ====== diff --git a/src/plugins/variadic/tests/defined/oracle/annot-formal.res.oracle b/src/plugins/variadic/tests/defined/oracle/annot-formal.res.oracle index 208a9cae21b756cd30ca8b051b1eb1b8807c38f6..842f84da121cc71a3b3d89a5263959ce8754f556 100644 --- a/src/plugins/variadic/tests/defined/oracle/annot-formal.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/annot-formal.res.oracle @@ -4,6 +4,7 @@ [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed +[eva:loop-unroll] tests/defined/annot-formal.c:11: Automatic loop unrolling. [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function sum: diff --git a/src/plugins/variadic/tests/defined/oracle/annot-loc.res.oracle b/src/plugins/variadic/tests/defined/oracle/annot-loc.res.oracle index 1a7b9cd9cf2d9bf1023003d192f3f6a794512d4f..f47ef5195afb3ee6cbd1dd849f743e18f8b58d4f 100644 --- a/src/plugins/variadic/tests/defined/oracle/annot-loc.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/annot-loc.res.oracle @@ -4,6 +4,7 @@ [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed +[eva:loop-unroll] tests/defined/annot-loc.c:11: Automatic loop unrolling. [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function sum: diff --git a/src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle b/src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle index 7f338532acdc46cb6ab68dfd84819601cf787197..9ca02969343a055b214876c7bc7fc9a102cd4164 100644 --- a/src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle @@ -4,6 +4,7 @@ [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed +[eva:loop-unroll] tests/defined/empty-vpar.c:10: Automatic loop unrolling. [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function sum: diff --git a/src/plugins/variadic/tests/defined/oracle/forward.res.oracle b/src/plugins/variadic/tests/defined/oracle/forward.res.oracle index a7b3971db2a4c52c818065884c15d0e53fcb0e66..7b42f741aeffe06135ce7ae74fc7f2d556df5e63 100644 --- a/src/plugins/variadic/tests/defined/oracle/forward.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/forward.res.oracle @@ -4,6 +4,7 @@ [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed +[eva:loop-unroll] tests/defined/forward.c:18: Automatic loop unrolling. [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function sum: diff --git a/src/plugins/variadic/tests/defined/oracle/max.res.oracle b/src/plugins/variadic/tests/defined/oracle/max.res.oracle index ded04c65a71a2325e204765ab517b6285fd3fda3..d44b6ac787a1ea0599d77d78691bf1c677db08ae 100644 --- a/src/plugins/variadic/tests/defined/oracle/max.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/max.res.oracle @@ -4,6 +4,7 @@ [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed +[eva:loop-unroll] tests/defined/max.c:10: Automatic loop unrolling. [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function max: diff --git a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle index 7369a68d0b2dff785f411483c5f39da4584de845..20142167b8a27541bed909c4d5f632f0a0d1fa5e 100644 --- a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle @@ -7,6 +7,8 @@ [eva] Initial state computed [eva] tests/defined/multiple-va_start.c:20: allocating variable __malloc_pack_l20 +[eva:loop-unroll] tests/defined/multiple-va_start.c:23: + Automatic loop unrolling. [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function pack: diff --git a/src/plugins/variadic/tests/defined/oracle/pointers-to-va.res.oracle b/src/plugins/variadic/tests/defined/oracle/pointers-to-va.res.oracle index 0bc3f144390573516f1965b8d5b4e9df34944ff4..3421bc03a435ab73945da39cafe4a27b980656ab 100644 --- a/src/plugins/variadic/tests/defined/oracle/pointers-to-va.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/pointers-to-va.res.oracle @@ -12,6 +12,8 @@ [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed +[eva:loop-unroll] tests/defined/pointers-to-va.c:10: Automatic loop unrolling. +[eva:loop-unroll] tests/defined/pointers-to-va.c:21: Automatic loop unrolling. [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function f: diff --git a/src/plugins/variadic/tests/defined/oracle/simple.res.oracle b/src/plugins/variadic/tests/defined/oracle/simple.res.oracle index 44c52cd1b73640e3ea054e44b82a79f6b48f2b12..260619be3c82397db4d9ae0dabdfe21c7b8f7498 100644 --- a/src/plugins/variadic/tests/defined/oracle/simple.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/simple.res.oracle @@ -4,6 +4,7 @@ [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed +[eva:loop-unroll] tests/defined/simple.c:10: Automatic loop unrolling. [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function sum: diff --git a/src/plugins/variadic/tests/defined/oracle/struct.res.oracle b/src/plugins/variadic/tests/defined/oracle/struct.res.oracle index e65d36e637b8b349c7431136d307c68622bfdad9..f4edc97074848ad5bd9f31f80a8133accc837112 100644 --- a/src/plugins/variadic/tests/defined/oracle/struct.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/struct.res.oracle @@ -4,6 +4,7 @@ [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed +[eva:loop-unroll] tests/defined/struct.c:25: Automatic loop unrolling. [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function max: diff --git a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle index 83a0ba4f9cf11e5afd51b149f043b7ed155f2658..c44e3a128afc256084479e56058b36e46bbae2e7 100644 --- a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle @@ -5,6 +5,7 @@ [eva] Computing initial state [eva] Initial state computed [eva] tests/defined/va_copy.c:21: allocating variable __malloc_pack_l21 +[eva:loop-unroll] tests/defined/va_copy.c:23: Automatic loop unrolling. [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function pack: diff --git a/src/plugins/variadic/tests/defined/oracle/va_list-as-arg.res.oracle b/src/plugins/variadic/tests/defined/oracle/va_list-as-arg.res.oracle index 5fc590007e57e1a9c02fabfa279c7f055923488f..09e397b9a5ac3d25f1bdc258ad4c9daf6bb273be 100644 --- a/src/plugins/variadic/tests/defined/oracle/va_list-as-arg.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/va_list-as-arg.res.oracle @@ -5,6 +5,7 @@ [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed +[eva:loop-unroll] tests/defined/va_list-as-arg.c:6: Automatic loop unrolling. [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function vsum: