diff --git a/infer/src/checkers/IdAccessPathMapDomain.ml b/infer/src/checkers/IdAccessPathMapDomain.ml index 7d9098f23..133513c65 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.ml +++ b/infer/src/checkers/IdAccessPathMapDomain.ml @@ -18,27 +18,6 @@ include IdMap let pp fmt astate = IdMap.pp ~pp_value:AccessPath.Raw.pp fmt astate -let (<=) ~lhs ~rhs = - if phys_equal lhs rhs - then true - else - try - IdMap.for_all - (fun id lhs_ap -> - let rhs_ap = IdMap.find id rhs in - let eq = AccessPath.Raw.equal lhs_ap rhs_ap in - if not eq && Config.debug_exceptions - then - failwithf "Id %a maps to both %a and %a@." - Var.pp id - AccessPath.Raw.pp lhs_ap - AccessPath.Raw.pp rhs_ap; - eq) - lhs - with Not_found -> false - -(* in principle, could do a join here if the access paths have the same root. but they should - always be equal if we are using the map correctly *) let check_invariant ap1 ap2 = function | Var.ProgramVar pvar when Pvar.is_frontend_tmp pvar -> (* Sawja reuses temporary variables which sometimes breaks this invariant *) @@ -52,6 +31,18 @@ let check_invariant ap1 ap2 = function AccessPath.Raw.pp ap1 AccessPath.Raw.pp ap2 +let (<=) ~lhs ~rhs = + if phys_equal lhs rhs + then true + else + IdMap.for_all + (fun id lhs_ap -> + let rhs_has = IdMap.mem id rhs in + if rhs_has && Config.debug_exceptions + then check_invariant lhs_ap (IdMap.find id rhs) id; + rhs_has) + lhs + let join astate1 astate2 = if phys_equal astate1 astate2 then astate1