Module Pulselib__PulseAbductiveDomain

module F = Stdlib.Format
module BaseAddressAttributes = Pulselib.PulseBaseAddressAttributes
module BaseDomain = Pulselib.PulseBaseDomain
module BaseMemory = Pulselib.PulseBaseMemory
module BaseStack = Pulselib.PulseBaseStack
module type BaseDomainSig = sig ... end

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

module PostDomain : BaseDomainSig

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

module PreDomain : BaseDomainSig

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

type t = private {
post : PostDomain.t;

state at the current program point

pre : PreDomain.t;

inferred pre at the current program point

skipped_calls : Pulselib.PulseBasicInterface.SkippedCalls.t;

set of skipped calls

path_condition : Pulselib.PulseBasicInterface.PathCondition.t;

arithmetic facts

}

biabduction-style pre/post state + skipped calls

val leq : lhs:t -> rhs:t -> bool
val pp : Stdlib.Format.formatter -> t -> unit
val mk_initial : IR.Procdesc.t -> t
val get_pre : t -> BaseDomain.t
val get_post : t -> BaseDomain.t
module Stack : sig ... end

stack operations like BaseStack but that also take care of propagating facts to the precondition

module Memory : sig ... end

memory operations like BaseMemory but that also take care of propagating facts to the precondition

module AddressAttributes : sig ... end

attribute operations like BaseAddressAttributes but that also take care of propagating facts to the precondition

val is_local : IR.Var.t -> t -> bool
val find_post_cell_opt : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> BaseDomain.cell option
val discard_unreachable : t -> t * Pulselib.PulseBasicInterface.AbstractValue.Set.t * BaseAddressAttributes.t

discard_unreachable astate garbage collects unreachable addresses in the state to make it smaller, and retuns the new state, the live addresses, and the attributes of discarded addresses

val add_skipped_call : IR.Procname.t -> Pulselib.PulseBasicInterface.Trace.t -> t -> t
val add_skipped_calls : Pulselib.PulseBasicInterface.SkippedCalls.t -> t -> t
val set_path_condition : Pulselib.PulseBasicInterface.PathCondition.t -> t -> t
val of_post : IR.Procdesc.t -> t -> t
val set_post_edges : Pulselib.PulseBasicInterface.AbstractValue.t -> BaseMemory.Edges.t -> t -> t

directly set the edges for the given address, bypassing abduction altogether

val set_post_cell : (Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t) -> BaseDomain.cell -> IBase.Location.t -> t -> t

directly set the edges and attributes for the given address, bypassing abduction altogether