diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml index 9cb77831f792b9f2a669c69c0d073dd58d7a20ac..c012563e68e62d5458eb3ead88a0747f3b783301 100644 --- a/src/plugins/value/partitioning/auto_loop_unroll.ml +++ b/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 diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle index a1ed5bef6632447a211bc66221b489c41af0de86..9b5007dda77cb84432095699d8e4fcc899d9704d 100644 --- a/tests/value/oracle/auto_loop_unroll.1.res.oracle +++ b/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