diff --git a/infer/src/checkers/LithoDomain.ml b/infer/src/checkers/LithoDomain.ml index 36fe9dc9a..6888cd3e7 100644 --- a/infer/src/checkers/LithoDomain.ml +++ b/infer/src/checkers/LithoDomain.ml @@ -37,7 +37,35 @@ module MethodCall = struct end module CallSet = AbstractDomain.FiniteSet (MethodCall) -include AbstractDomain.Map (LocalAccessPath) (CallSet) +module OldDomain = AbstractDomain.Map (LocalAccessPath) (CallSet) + +module NewDomain = struct + include AbstractDomain.Empty +end + +include struct + include AbstractDomain.Pair (OldDomain) (NewDomain) + + let lift f (o, _) = f o + + let map_old f (o, n) = (f o, n) + + let empty = (OldDomain.empty, ()) + + let add k v = map_old (OldDomain.add k v) + + let remove k = map_old (OldDomain.remove k) + + let bindings = lift OldDomain.bindings + + let find k = lift (OldDomain.find k) + + let mem k = lift (OldDomain.mem k) + + let iter f = lift (OldDomain.iter f) + + let fold f (o, _) init = OldDomain.fold f o init +end let substitute ~(f_sub : LocalAccessPath.t -> LocalAccessPath.t option) astate = fold diff --git a/infer/src/checkers/LithoDomain.mli b/infer/src/checkers/LithoDomain.mli index c6d9acaf4..24810d19a 100644 --- a/infer/src/checkers/LithoDomain.mli +++ b/infer/src/checkers/LithoDomain.mli @@ -31,7 +31,23 @@ end module CallSet : module type of AbstractDomain.FiniteSet (MethodCall) -include module type of AbstractDomain.Map (LocalAccessPath) (CallSet) +module OldDomain : module type of AbstractDomain.Map (LocalAccessPath) (CallSet) + +module NewDomain : module type of AbstractDomain.Empty + +include module type of AbstractDomain.Pair (OldDomain) (NewDomain) + +val empty : t + +val add : LocalAccessPath.t -> CallSet.t -> t -> t + +val remove : LocalAccessPath.t -> t -> t + +val mem : LocalAccessPath.t -> t -> bool + +val find : LocalAccessPath.t -> t -> CallSet.t + +val bindings : t -> (LocalAccessPath.t * CallSet.t) list val substitute : f_sub:(LocalAccessPath.t -> LocalAccessPath.t option) -> t -> t (** Substitute each access path in the domain using [f_sub]. If [f_sub] returns None, the original