diff --git a/src/plugins/occurrence/register.ml b/src/plugins/occurrence/register.ml index 8d9d94741ec37ce7bf37449cc19674c8fc73cc66..cbf6feb70846cf1dd57df3a5b3accf76e580e99d 100644 --- a/src/plugins/occurrence/register.ml +++ b/src/plugins/occurrence/register.ml @@ -106,19 +106,21 @@ class occurrence = object (self) method! vlval lv = let ki = self#current_kinstr in - if Db.Value.is_accessible ki then begin - let z = !Db.Value.lval_to_zone ki lv in - try - Locations.Zone.fold_topset_ok - (fun b _ () -> - match b with - | Base.Var (vi, _) | Base.Allocated (vi, _, _) -> - Occurrences.add vi self#current_kf ki lv - | _ -> () - ) z () - with Abstract_interp.Error_Top -> - error ~current:true "Found completely imprecise value (%a). Ignoring@." - Printer.pp_lval lv + begin + match Eva.Results.(before_kinstr ki |> eval_address lv |> as_zone) with + | Result.Error _ -> (* ignore *) () + | Ok z -> + try + Locations.Zone.fold_topset_ok + (fun b _ () -> + match b with + | Base.Var (vi, _) | Base.Allocated (vi, _, _) -> + Occurrences.add vi self#current_kf ki lv + | _ -> () + ) z () + with Abstract_interp.Error_Top -> + error ~current:true "Found completely imprecise value (%a). Ignoring@." + Printer.pp_lval lv end; DoChildren @@ -135,7 +137,7 @@ class occurrence = object (self) Db.yield (); super#vstmt_aux s - initializer !Db.Value.compute () + initializer Eva.Analysis.compute () end