diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index fcbc45a77..94c723399 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -21,6 +21,11 @@ module type BaseDomainSig = sig (* private because the lattice is not the same for preconditions and postconditions so we don't want to confuse them *) type t = private BaseDomain.t [@@deriving compare, equal, yojson_of] +end + +(* defined in two parts to avoid exporting internal APIs to the .mli *) +module type BaseDomainSig_ = sig + include BaseDomainSig val empty : t @@ -46,7 +51,7 @@ type base_domain = BaseDomain.t = (** represents the post abstract state at each program point *) module PostDomain : sig - include BaseDomainSig + include BaseDomainSig_ val initialize : AbstractValue.t -> t -> t end = struct @@ -87,7 +92,7 @@ end (* NOTE: [PreDomain] and [Domain] theoretically differ in that [PreDomain] should be the inverted lattice of [Domain], but since we never actually join states or check implication the two collapse into one. *) (** represents the inferred pre-condition at each program point, biabduction style *) -module PreDomain : BaseDomainSig = PostDomain +module PreDomain : BaseDomainSig_ = PostDomain (* see documentation in this file's .mli *) type t = diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 868cbe2d1..04f7c65f3 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -6,9 +6,7 @@ *) open! IStd -module F = Format open PulseBasicInterface -module BaseAddressAttributes = PulseBaseAddressAttributes module BaseDomain = PulseBaseDomain module BaseMemory = PulseBaseMemory module BaseStack = PulseBaseStack @@ -24,24 +22,6 @@ module type BaseDomainSig = sig (* private because the lattice is not the same for preconditions and postconditions so we don't want to confuse them *) type t = private BaseDomain.t [@@deriving compare, equal, yojson_of] - - val yojson_of_t : t -> Yojson.Safe.t - - val empty : t - - val update : ?stack:BaseStack.t -> ?heap:BaseMemory.t -> ?attrs:BaseAddressAttributes.t -> t -> t - - val filter_addr : f:(AbstractValue.t -> bool) -> t -> t - (** filter both heap and attrs *) - - val filter_addr_with_discarded_addrs : - f:(AbstractValue.t -> bool) -> t -> t * AbstractValue.t list - (** compute new state containing only reachable addresses in its heap and attributes, as well as - the list of discarded unreachable addresses *) - - val subst_var : AbstractValue.t * AbstractValue.t -> t -> t SatUnsat.t - - val pp : F.formatter -> t -> unit end (** The post abstract state at each program point, or current state. *)