diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml index ec5d1936afa118b8fd245b5986cd08baec9078be..ccb06088ba69926fa7d198e9dbc75637011b9ff6 100644 --- a/src/plugins/value/partitioning/auto_loop_unroll.ml +++ b/src/plugins/value/partitioning/auto_loop_unroll.ml @@ -200,7 +200,7 @@ let is_safe_instruction lval = function | Asm _ -> false (* Returns true if the statement [stmt] of function [kf] does not modify [lval]. - [lval] is a candidate for the automatic loop unrolling of [loop] [loop]. *) + [lval] is a candidate for the automatic loop unrolling of [loop]. *) let is_constant kf ~loop lval stmt = let rec is_safe_stmt ~goto stmt = match stmt.skind with @@ -224,12 +224,19 @@ let is_constant kf ~loop lval stmt = that contains the current loop, which we don't want to unroll. *) let dest_blocks = Kernel_function.find_all_enclosing_blocks !dest in List.exists (Cil_datatype.Block.equal loop) dest_blocks && - (* Otherwise, the goto stays within the loop: check that the block - englobing both the source and the destination is safe. *) - let block = Kernel_function.common_block !dest stmt in - (* If this block is the loop itself, then it is not safe, - as [lval] is modified within the loop. *) - not (block == loop) && is_safe_block ~goto:true block + (* Otherwise, the goto stays within the loop. *) + begin + (* If the successors all exits the loop block, then the goto is safe. + This is the case for gotos coming from "continue" statement. *) + let all_stmts = Stmts_graph.get_block_stmts loop in + let is_outside_loop s = not (Cil_datatype.Stmt.Set.mem s all_stmts) in + List.for_all is_outside_loop !dest.succs || + (* Otherwise, check that the block englobing both the source and the + destination is safe. If this block is the loop itself, then it is + not safe, as [lval] is modified within the loop. *) + let block = Kernel_function.common_block !dest stmt in + not (block == loop) && is_safe_block ~goto:true block + end | _ -> false (* A block is safe if all its statements are safe. *) and is_safe_block ~goto b = List.for_all (is_safe_stmt ~goto) b.bstmts in diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle index 8ab0e3b67902dc4f9c802aacb041e3de3dc6eef9..8b52a2f0f5928ee15eff44ed456aebe61b177ca1 100644 --- a/tests/value/oracle/auto_loop_unroll.1.res.oracle +++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle @@ -395,21 +395,12 @@ [eva:alarm] tests/value/auto_loop_unroll.c:291: Warning: signed overflow. assert res + 1 ≤ 2147483647; [eva] tests/value/auto_loop_unroll.c:296: Frama_C_show_each_top: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:299: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:302: Warning: - signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:304: - Frama_C_show_each_0_35: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:307: Warning: - signed overflow. assert res + 1 ≤ 2147483647; -[eva:alarm] tests/value/auto_loop_unroll.c:307: Warning: - signed overflow. assert -2147483648 ≤ i - 1; -[eva] tests/value/auto_loop_unroll.c:311: Frama_C_show_each_36: [0..2147483647] -[eva] tests/value/auto_loop_unroll.c:314: starting to merge loop iterations -[eva:alarm] tests/value/auto_loop_unroll.c:317: Warning: - signed overflow. assert res + 1 ≤ 2147483647; -[eva] tests/value/auto_loop_unroll.c:319: Frama_C_show_each_27: [0..2147483647] +[eva:loop-unroll] tests/value/auto_loop_unroll.c:299: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:304: Frama_C_show_each_0_35: [0..35] +[eva:loop-unroll] tests/value/auto_loop_unroll.c:307: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:311: Frama_C_show_each_36: {36} +[eva:loop-unroll] tests/value/auto_loop_unroll.c:314: Automatic loop unrolling. +[eva] tests/value/auto_loop_unroll.c:319: Frama_C_show_each_27: {27} [eva] Recording results for loops_with_goto [eva] Done for function loops_with_goto [eva] computing for function non_natural_loops <- main.