Module type Pulselib__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:(Pulselib.PulseBasicInterface.AbstractValue.t -> bool) -> t -> t
filter both heap and attrs
val filter_addr_with_discarded_addrs : f:(Pulselib.PulseBasicInterface.AbstractValue.t -> bool) -> t -> t * Pulselib.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