diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml index 03af652f8f472d3236c1d4ae4b9f321f75f0fd59..9cb77831f792b9f2a669c69c0d073dd58d7a20ac 100644 --- a/src/plugins/value/partitioning/auto_loop_unroll.ml +++ b/src/plugins/value/partitioning/auto_loop_unroll.ml @@ -55,23 +55,24 @@ let is_true = function | `True | `TrueReduced _ -> true | _ -> false -(* Is a statement a loop exit condition? If so, returns the condition and - whether the condition must hold to exit the loop. Otherwise, returns None. *) -let is_conditional_break stmt = - match stmt.skind with - | If (cond, {bstmts=[{skind=Break _}]}, _, _) -> Some (cond, true) - | If (cond, _, {bstmts=[{skind=Break _}]}, _) -> Some (cond, false) - | _ -> None - -(* Returns a loop exit condition, as the conditional expression and whether - the condition must be zero or non-zero to exit the loop. *) +(* Does a block exits a loop? *) +let is_break block = + match block.bstmts with + | [{skind = Break _}] -> true + | _ -> false + +(* Returns a list of loop exit conditions. Each condition is expressed as an + expression and whether it must be zero or non-zero to exit the loop. *) let find_loop_exit_condition loop = let rec aux = function | [] -> [] | stmt :: tl -> - match is_conditional_break stmt with - | Some x -> x :: aux tl - | None -> aux tl + match stmt.skind with + | If (cond, b1, b2, _) when is_break b1 || is_break b2 -> + if is_break b1 + then (cond, true) :: aux (b2.bstmts @ tl) + else (cond, false) :: aux (b1.bstmts @ tl) + | _ -> aux tl in aux loop.bstmts @@ -437,6 +438,8 @@ module Make (Abstract: Abstractions.Eva) = struct | Block block -> cross_block acc block | UnspecifiedSequence list -> List.fold_left (fun acc (s, _, _, _, _) -> cross_stmt acc s) acc list + | If (_, {bstmts=[{skind=Break _}]}, block, _) + | If (_, block, {bstmts=[{skind=Break _}]}, _) -> cross_block acc block | _ -> acc and cross_block acc block = List.fold_left cross_stmt acc block.bstmts diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle index 942c41640392fdd051c3f4972218cc78e19e14d9..a1ed5bef6632447a211bc66221b489c41af0de86 100644 --- a/tests/value/oracle/auto_loop_unroll.1.res.oracle +++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle @@ -347,13 +347,8 @@ [eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: {12} [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; -[eva:alarm] tests/value/auto_loop_unroll.c:208: Warning: - signed overflow. assert -2147483648 ≤ i_1 - 1; -[eva] tests/value/auto_loop_unroll.c:211: - Frama_C_show_each_0_14: [0..2147483647] +[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;