Module PulseAbductiveDomain.PostDomain

The post abstract state at each program point, or current state.

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