Commit 9a6d9a9a authored by David Bühler's avatar David Bühler
Browse files

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

parent 8197fa33
......@@ -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