diff --git a/src/plugins/eva/partitioning/partition.ml b/src/plugins/eva/partitioning/partition.ml index bb0413884134893bdb0e8b2bfb9f97472b17d7dd..4c8675e975e8049a309f7dc4666cd1e72042f7f3 100644 --- a/src/plugins/eva/partitioning/partition.ml +++ b/src/plugins/eva/partitioning/partition.ml @@ -470,21 +470,24 @@ struct let states = function _ -> Abstract.Dom.top in Abstract_domain.{ states; result = None } in - let source = fst (predicate.Cil_types.pred_loc) in - let aux positive = - let+ state' = - Abstract.Dom.reduce_by_predicate env state predicate positive in - let x = Abstract.Dom.evaluate_predicate env state' predicate in - if x == Unknown - then begin - Self.warning ~source ~once:true - "failing to learn perfectly from split predicate"; - 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 - Bottom.list_values [ aux true; aux false ] + match Abstract.Dom.evaluate_predicate env state predicate with + | True -> [ Integer.one, state ] + | False -> [ Integer.zero, state ] + | Unknown -> + let source = fst (predicate.Cil_types.pred_loc) in + let aux positive = + let+ state' = + Abstract.Dom.reduce_by_predicate env state predicate positive in + let x = Abstract.Dom.evaluate_predicate env state' predicate in + if x == Unknown + then + Self.warning ~source ~once:true + "failing to learn perfectly from split predicate"; + if Abstract.Dom.equal state' state then raise Operation_failed; + let value = if positive then Integer.one else Integer.zero in + value, state' + in + Bottom.list_values [ aux true; aux false ] (* --- Applying partitioning actions onto flows --------------------------- *)