Commit 67c9b34c authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

Merge branch 'fix/eva/auto-loop-unroll' into 'master'

[Eva] Fixes the automatic loop unrolling on loops with no counter increment.

Closes #937

See merge request frama-c/frama-c!2804
parents 0ed6b546 9a6d9a9a
......@@ -415,7 +415,8 @@ module Make (Abstract: Abstractions.Eva) = struct
try
let zero_delta = { current = `Value Val.zero; final = `Bottom; } in
let delta = delta_block zero_delta loop in
final_delta delta >> fun d -> Some d
final_delta delta >> fun d ->
if is_true (Val.assume_non_zero d) then Some d else None
with NoIncrement -> None
(* If in the block [loop], [lval] is assigned once to the value of another
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment