Module `PulseAbductiveDomain.PreDomain`

The inferred pre-condition at each program point, biabduction style.

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. *

type t = private BaseDomain.t

val compare : t -> t -> int
val equal : t -> t -> bool
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t

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