diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 3be8b31ad..60eb84eb8 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -34,7 +34,7 @@ module type BaseDomain = sig val filter_addr : f:(AbstractValue.t -> bool) -> t -> t (**filter both heap and attrs *) - include AbstractDomain.NoJoin with type t := t + val pp : F.formatter -> t -> unit end (* just to expose record field names without having to type @@ -83,9 +83,6 @@ module InvertedDomain : BaseDomain = struct let empty = BaseDomain.empty let pp = BaseDomain.pp - - (** inverted lattice *) - let leq ~lhs ~rhs = BaseDomain.leq ~rhs:lhs ~lhs:rhs end (** biabduction-style pre/post state *) diff --git a/infer/src/pulse/PulseBaseDomain.ml b/infer/src/pulse/PulseBaseDomain.ml index 7e2938de0..4417a3bc0 100644 --- a/infer/src/pulse/PulseBaseDomain.ml +++ b/infer/src/pulse/PulseBaseDomain.ml @@ -190,10 +190,6 @@ module GraphComparison = struct match isograph_map ~lhs ~rhs mapping with IsomorphicUpTo _ -> true | NotIsomorphic -> false end -let leq ~lhs ~rhs = - phys_equal lhs rhs || GraphComparison.is_isograph ~lhs ~rhs GraphComparison.empty_mapping - - let pp fmt {heap; stack; skipped_calls; attrs} = F.fprintf fmt "{@[ roots=@[%a@];@;mem =@[%a@];@;attrs=@[%a@];@;skipped_calls=@[%a@];@]}" diff --git a/infer/src/pulse/PulseBaseDomain.mli b/infer/src/pulse/PulseBaseDomain.mli index 2fbac7aaa..89920a839 100644 --- a/infer/src/pulse/PulseBaseDomain.mli +++ b/infer/src/pulse/PulseBaseDomain.mli @@ -7,6 +7,7 @@ open! IStd open PulseBasicInterface +module F = Format module SkippedTrace : sig type t = PulseTrace.t @@ -25,8 +26,6 @@ type cell = PulseBaseMemory.Edges.t * Attributes.t val empty : t -include AbstractDomain.NoJoin with type t := t - val reachable_addresses : t -> AbstractValue.Set.t (** compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable from the stack variables *) @@ -44,3 +43,5 @@ val isograph_map : lhs:t -> rhs:t -> mapping -> isograph_relation val is_isograph : lhs:t -> rhs:t -> mapping -> bool val find_cell_opt : AbstractValue.t -> t -> cell option + +val pp : F.formatter -> t -> unit