diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index fe65ccb612ebd7959501e935c6f8ede9cbe58063..a7138c912d6edcd7e3316299c63486fc1e5ee5aa 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -412,7 +412,8 @@ struct
match AutoLoopUnroll.compute ~max_unroll x stmt with
| None -> min_unroll
| Some i ->
- Value_parameters.warning ~once:true ~current:true
+ let source = fst (Cil_datatype.Stmt.loc stmt) in
+ Value_parameters.warning ~once:true ~current:true ~source
~wkey:Value_parameters.wkey_loop_unroll
"Automatic loop unrolling.";
i
diff --git a/tests/value/auto_loop_unroll.c b/tests/value/auto_loop_unroll.c
index ec9519bbcc7687d2e31c3fb28fd91a3d3f12b2b9..1d083a1c84154a7c112a4f25e84cdf468ac7bbbf 100644
--- a/tests/value/auto_loop_unroll.c
+++ b/tests/value/auto_loop_unroll.c
@@ -384,6 +384,34 @@ void non_natural_loops () {
res = 0;
}
+/* Tests the automatic loop unrolling on loops that follow directly each other. */
+void following_loops () {
+ int i = 0, j = 0;
+ while (i < 15) {
+ i++;
+ j++;
+ }
+ while (i < 30) {
+ i++;
+ j++;
+ }
+ Frama_C_show_each_30(j);
+ i = 0;
+ j = 0;
+ while (i < 15 && undet) {
+ i++;
+ j++;
+ }
+ while (i < 30) {
+ i++;
+ j++;
+ }
+ /* The equality relation between [i] and [j] is lost between the two loops,
+ where all states exiting the first loop are joined. However, the unrolling
+ prevents the value of [j] to be completely imprecise. */
+ Frama_C_show_each_30(j);
+}
+
void main () {
simple_loops ();
various_loops ();
@@ -392,4 +420,5 @@ void main () {
temporary_variables ();
loops_with_goto ();
non_natural_loops ();
+ following_loops ();
}
diff --git a/tests/value/oracle/auto_loop_unroll.0.res.oracle b/tests/value/oracle/auto_loop_unroll.0.res.oracle
index 9f0232a5ddc1ee3fc973ef51bfb5f87f506e4dc8..f34b2d3391c550082ac44d8e02e57b4b4b1e1dc7 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:388.
+ Called from tests/value/auto_loop_unroll.c:416.
[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:389.
+ Called from tests/value/auto_loop_unroll.c:417.
[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;
@@ -146,7 +146,7 @@
[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:390.
+ Called from tests/value/auto_loop_unroll.c:418.
[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;
@@ -205,7 +205,7 @@
[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:391.
+ Called from tests/value/auto_loop_unroll.c:419.
[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;
@@ -245,7 +245,7 @@
[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:392.
+ Called from tests/value/auto_loop_unroll.c:420.
[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;
@@ -279,7 +279,7 @@
[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:393.
+ Called from tests/value/auto_loop_unroll.c:421.
[eva] tests/value/auto_loop_unroll.c:298: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:299: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -321,7 +321,7 @@
[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:394.
+ Called from tests/value/auto_loop_unroll.c:422.
[eva:alarm] tests/value/auto_loop_unroll.c:371: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: [1..2147483647]
@@ -333,9 +333,30 @@
Frama_C_show_each_1_51: [1..2147483647]
[eva] Recording results for non_natural_loops
[eva] Done for function non_natural_loops
+[eva] computing for function following_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:423.
+[eva] tests/value/auto_loop_unroll.c:390: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:392: Warning:
+ signed overflow. assert j + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:396: Warning:
+ signed overflow. assert j + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:394: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:401: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:403: Warning:
+ signed overflow. assert j + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:407: Warning:
+ signed overflow. assert j + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:405: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [0..2147483647]
+[eva] Recording results for following_loops
+[eva] Done for function following_loops
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function following_loops:
+ i ∈ {30}
+ j ∈ [0..2147483647]
[eva:final-states] Values at end of function incr:
__retres ∈ [1..2147483647]
[eva:final-states] Values at end of function incr_g:
@@ -383,6 +404,8 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
g ∈ {64}
+[from] Computing for function following_loops
+[from] Done for function following_loops
[from] Computing for function incr
[from] Done for function incr
[from] Computing for function incr_g
@@ -410,6 +433,8 @@
[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 following_loops:
+ NO EFFECTS
[from] Function incr:
\result FROM i
[from] Function incr_g:
@@ -433,6 +458,10 @@
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
g FROM \nothing
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function following_loops:
+ i; j
+[inout] Inputs for function following_loops:
+ undet
[inout] Out (internal) for function incr:
__retres
[inout] Inputs for function incr:
diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle
index 315adc3135a575b6d642850d62faba61c083b84b..1826be4c45b15e28b686ca1477a15430deaba845 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:388.
+ Called from tests/value/auto_loop_unroll.c:416.
[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:389.
+ Called from tests/value/auto_loop_unroll.c:417.
[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.
@@ -287,7 +287,7 @@
[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:390.
+ Called from tests/value/auto_loop_unroll.c:418.
[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;
@@ -346,7 +346,7 @@
[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:391.
+ Called from tests/value/auto_loop_unroll.c:419.
[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.
@@ -366,7 +366,7 @@
[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:392.
+ Called from tests/value/auto_loop_unroll.c:420.
[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.
@@ -384,7 +384,7 @@
[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:393.
+ Called from tests/value/auto_loop_unroll.c:421.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:298: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: {30}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:307: Automatic loop unrolling.
@@ -417,16 +417,29 @@
[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:394.
+ Called from tests/value/auto_loop_unroll.c:422.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:370: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: {50}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:379: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:383: Frama_C_show_each_1_51: [1..51]
[eva] Recording results for non_natural_loops
[eva] Done for function non_natural_loops
+[eva] computing for function following_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:423.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:390: Automatic loop unrolling.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:394: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: {30}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:401: Automatic loop unrolling.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:405: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [15..45]
+[eva] Recording results for following_loops
+[eva] Done for function following_loops
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function following_loops:
+ i ∈ {30}
+ j ∈ [15..45]
[eva:final-states] Values at end of function incr:
__retres ∈ [1..25]
[eva:final-states] Values at end of function incr_g:
@@ -474,6 +487,8 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
g ∈ {64}
+[from] Computing for function following_loops
+[from] Done for function following_loops
[from] Computing for function incr
[from] Done for function incr
[from] Computing for function incr_g
@@ -501,6 +516,8 @@
[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 following_loops:
+ NO EFFECTS
[from] Function incr:
\result FROM i
[from] Function incr_g:
@@ -524,6 +541,10 @@
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
g FROM \nothing
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function following_loops:
+ i; j
+[inout] Inputs for function following_loops:
+ undet
[inout] Out (internal) for function incr:
__retres
[inout] Inputs for function incr: