Skip to content
Snippets Groups Projects
Commit df8f7447 authored by Valentin Perrelle's avatar Valentin Perrelle Committed by David Bühler
Browse files

[Eva] Use binding operator

parent bc2bd27d
No related branches found
No related tags found
No related merge requests found
...@@ -412,7 +412,7 @@ struct ...@@ -412,7 +412,7 @@ struct
let build i acc = let build i acc =
let value = Abstract.Val.inject_int (Cil.typeOf exp) i in let value = Abstract.Val.inject_int (Cil.typeOf exp) i in
let state = let state =
Abstract.Eval.assume ~valuation state exp value >>- fun valuation -> let* valuation = Abstract.Eval.assume ~valuation state exp value in
(* Check the reduction *) (* Check the reduction *)
Abstract.Dom.update (Abstract.Eval.to_domain_valuation valuation) state Abstract.Dom.update (Abstract.Eval.to_domain_valuation valuation) state
in in
...@@ -472,8 +472,8 @@ struct ...@@ -472,8 +472,8 @@ struct
in in
let source = fst (predicate.Cil_types.pred_loc) in let source = fst (predicate.Cil_types.pred_loc) in
let aux positive = let aux positive =
Abstract.Dom.reduce_by_predicate env state predicate positive let+ state' =
>>-: fun state' -> Abstract.Dom.reduce_by_predicate env state predicate positive in
let x = Abstract.Dom.evaluate_predicate env state' predicate in let x = Abstract.Dom.evaluate_predicate env state' predicate in
if x == Unknown if x == Unknown
then then
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment