Module type PulseAbductiveDomain.BaseDomainSig

signature common to the "normal" Domain, representing the post at the current program point, and the inverted PreDomain, representing the inferred pre-condition

type t = private BaseDomain.t
val empty : t
val update : ?⁠stack:BaseStack.t -> ?⁠heap:BaseMemory.t -> ?⁠attrs:BaseAddressAttributes.t -> t -> t
val filter_addr : f:(PulseBasicInterface.AbstractValue.t -> bool) -> t -> t

filter both heap and attrs

val filter_addr_with_discarded_addrs : f:(PulseBasicInterface.AbstractValue.t -> bool) -> t -> t * PulseBasicInterface.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 pp : F.formatter -> t -> unit