Commit 40c9bc09 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Fixes partitioning splits on ACSL predicates.

A split has failed if the reduced state is equal to the entry state _and_
the predicate evaluates to Unknown.
If the predicate evaluates to True/False in the entry state, then the state
cannot be reduced: the reduced state is then equal to the entry state), but
this is not a failure: the split holds.
parent 2705371d
......@@ -476,10 +476,11 @@ struct
Abstract.Dom.reduce_by_predicate env state predicate positive in
let x = Abstract.Dom.evaluate_predicate env state' predicate in
if x == Unknown
then
then begin
Self.warning ~source ~once:true
"failing to learn perfectly from split predicate";
if Abstract.Dom.equal state' state then raise Operation_failed;
if Abstract.Dom.equal state' state then raise Operation_failed
end;
let value = if positive then Integer.one else Integer.zero in
value, state'
in
......
Supports Markdown
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