diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml
index defdb8a340dea48232822f53e376731b3ca019a9..9ede36c8b414390ecf13be140d5f36a038abf733 100644
--- a/src/plugins/value/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/value/partitioning/auto_loop_unroll.ml
@@ -395,6 +395,8 @@ module Make (Abstract: Abstractions.Eva) = struct
| If (_e, b1, b2, _loc) ->
join_delta (delta_block acc b1) (delta_block acc b2)
| Block b -> delta_block acc b
+ | UnspecifiedSequence list ->
+ List.fold_left (fun acc (s, _, _, _, _) -> delta_stmt acc s) acc list
| _ ->
(* For other statements, we only check that they do not modify [lval]. *)
if is_safe lval ~loop stmt then acc else raise NoIncrement
@@ -407,6 +409,43 @@ module Make (Abstract: Abstractions.Eva) = struct
final_delta delta >> fun d -> Some d
with NoIncrement -> None
+ (* If in the block [loop], [lval] is assigned once to the value of another
+ lvalue, returns this new lvalue. Otherwise, returns [lval]. *)
+ let cross_equality lval loop =
+ (* If no such single equality can be found, return [lval] unchanged. *)
+ let exception No_equality in
+ let rec find_lval acc expr =
+ if acc <> None then raise No_equality else
+ match expr.enode with
+ | Lval lval -> Some lval
+ | Info (e, _) -> find_lval acc e
+ | _ -> raise No_equality
+ in
+ let cross_instr acc = function
+ | Set (lv, expr, _loc) when Cil_datatype.LvalStructEq.equal lv lval ->
+ find_lval acc expr
+ | Local_init (varinfo, AssignInit (SingleInit expr), _loc)
+ when Cil_datatype.LvalStructEq.equal (Cil.var varinfo) lval ->
+ find_lval acc expr
+ | Call (Some lv, _, _, _) when Cil_datatype.LvalStructEq.equal lval lv ->
+ raise No_equality
+ | _ -> acc
+ in
+ let rec cross_stmt acc stmt =
+ match stmt.skind with
+ | Instr instr -> cross_instr acc instr
+ | Block block -> cross_block acc block
+ | UnspecifiedSequence list ->
+ List.fold_left (fun acc (s, _, _, _, _) -> cross_stmt acc s) acc list
+ | _ -> acc
+ and cross_block acc block =
+ List.fold_left cross_stmt acc block.bstmts
+ in
+ match cross_block None loop with
+ | None -> lval
+ | Some lval -> lval
+ | exception No_equality -> lval
+
(* If [lval] is a varinfo out-of-scope at statement [stmt] of function [kf],
introduces it to the [state]. *)
let enter_scope state kf stmt lval =
@@ -443,6 +482,10 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Reduce [condition] to a sufficient hypothesis over the [lval] value:
if [lval] ∈ [v_exit] then [condition = positive]. *)
reduce_to_lval_from_state state lval condition positive >>= fun v_exit ->
+ (* If [lval] is only assigned to the value of another lvalue, uses it
+ instead. This is especially useful to deal with temporary variables
+ introduced by the Frama-C normalization. *)
+ let lval = cross_equality lval loop_block in
(* Evaluates the initial value [v_init] of [lval] in the loop entry state. *)
evaluate_lvalue state lval >>= fun v_init ->
(* Computes an over-approximation [v_delta] of the increment of [lval]
diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle
index 624e97c523d62cd65926953ed45e3ec3a0422ac5..942c41640392fdd051c3f4972218cc78e19e14d9 100644
--- a/tests/value/oracle/auto_loop_unroll.1.res.oracle
+++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle
@@ -345,13 +345,8 @@
[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] 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: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] 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;
@@ -372,18 +367,10 @@
[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:loop-unroll] tests/value/auto_loop_unroll.c:235: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: {20}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:240: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: {21}
[eva] Recording results for temporary_variables
[eva] Done for function temporary_variables
[eva] Recording results for main
@@ -412,8 +399,8 @@
[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]
+ i ∈ {-1}
+ res ∈ {21}
[eva:final-states] Values at end of function various_conditions:
i ∈ {12}
res ∈ {0}