diff --git a/src/cdomain/value/cdomains/addressDomain.ml b/src/cdomain/value/cdomains/addressDomain.ml index 8f5bb4db4d..da684cc4f4 100644 --- a/src/cdomain/value/cdomains/addressDomain.ml +++ b/src/cdomain/value/cdomains/addressDomain.ml @@ -110,11 +110,6 @@ struct | StrPtr _, UnknownPtr -> None | _, _ -> Some false - let amenable_to_meet x y = match x,y with - | StrPtr _, StrPtr _ -> true - | Addr x, Addr y when Mval.equal (Mval.top_indices x) (Mval.top_indices y) -> true - | _ -> false - let leq x y = match x, y with | StrPtr s1, StrPtr s2 -> SD.leq s1 s2 | Addr x, Addr y -> Mval.leq x y @@ -183,7 +178,6 @@ struct struct include SetDomain.Joined (Addr) let may_be_equal a b = Option.value (Addr.semantic_equal a b) ~default:true - let amenable_to_meet = Addr.amenable_to_meet end module OffsetSplit = DisjointDomain.ProjectiveSetPairwiseMeet (Addr) (J) (Addr.UnitOffsetRepr) diff --git a/src/cdomain/value/cdomains/addressDomain_intf.ml b/src/cdomain/value/cdomains/addressDomain_intf.ml index b5eb5299f3..f65b2977c4 100644 --- a/src/cdomain/value/cdomains/addressDomain_intf.ml +++ b/src/cdomain/value/cdomains/addressDomain_intf.ml @@ -82,10 +82,6 @@ sig (** Check semantic equality of two addresses. @return [Some true] if definitely equal, [Some false] if definitely not equal, [None] if unknown. *) - - val amenable_to_meet: t -> t -> bool - (** Whether two addresses are amenable to meet operation, i.e., their lattice meet overapproximates the intersection - of concretizations. If true, meet is used instead of semantic_equal *) end (** Address lattice with sublattice representatives for {!DisjointDomain}. *) diff --git a/src/domain/disjointDomain.ml b/src/domain/disjointDomain.ml index 00f875bb3a..f8851155fb 100644 --- a/src/domain/disjointDomain.ml +++ b/src/domain/disjointDomain.ml @@ -182,7 +182,6 @@ module type MayEqualSetDomain = sig include SetDomain.S val may_be_equal: elt -> elt -> bool - val amenable_to_meet: elt -> elt -> bool end module ProjectiveSetPairwiseMeet (E: Lattice.S) (B: MayEqualSetDomain with type elt = E.t) (R: Representative with type elt = E.t): SetDomain.S with type elt = E.t = struct @@ -192,7 +191,8 @@ module ProjectiveSetPairwiseMeet (E: Lattice.S) (B: MayEqualSetDomain with type let meet_buckets b1 b2 acc = B.fold (fun e1 acc -> B.fold (fun e2 acc -> - if B.amenable_to_meet e1 e2 then + (* If they have the same representative, we use the normal meet within this bucket *) + if R.equal (R.of_elt e1) (R.of_elt e2) then try let m = E.meet e1 e2 in if not (E.is_bot m) then @@ -200,7 +200,7 @@ module ProjectiveSetPairwiseMeet (E: Lattice.S) (B: MayEqualSetDomain with type else acc with Lattice.Uncomparable -> - failwith (GobPretty.sprintf "amenable_to_meet %a %a returned true, but meet throws!" E.pretty e1 E.pretty e2) + failwith (GobPretty.sprintf "Elements %a and %a are in same bucket, but meet throws!" E.pretty e1 E.pretty e2) else if B.may_be_equal e1 e2 then add e1 (add e2 acc) else