[Eva] The automatic loop unrolling finds loop exit conditions in blocks.

src/plugins/value/partitioning/auto_loop_unroll.ml

@@ -72,6 +72,7 @@ let find_loop_exit_condition loop =
         if is_break b1
         then (cond, true) :: aux (b2.bstmts @ tl)
         else (cond, false) :: aux (b1.bstmts @ tl)
+      | Block b -> aux (b.bstmts @ tl)
       | _ -> aux tl
   in
   aux loop.bstmts

tests/value/oracle/auto_loop_unroll.1.res.oracle

@@ -349,11 +349,8 @@
 [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] 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: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: 
   Trace partitioning superposing up to 100 states