Module Pulselib.PulseExecutionDomain

module AbductiveDomain = PulseAbductiveDomain
module LatentIssue = PulseLatentIssue
type 'abductive_domain_t base_t =
| ContinueProgram of 'abductive_domain_t

represents the state at the program point

| ExitProgram of 'abductive_domain_t

represents the state originating at exit/divergence.

| AbortProgram of AbductiveDomain.summary

represents the state at the program point that caused an error

| LatentAbortProgram of {
astate : AbductiveDomain.summary;
latent_issue : LatentIssue.t;
}

this path leads to an error but we don't have conclusive enough data to report it yet

type t = AbductiveDomain.t base_t
include Absint.AbstractDomain.NoJoin with type t := t
include IStdlib.PrettyPrintable.PrintableType
type t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val leq : lhs:t -> rhs:t -> bool

the implication relation: lhs <= rhs means lhs |- rhs

val continue : AbductiveDomain.t -> t
val mk_initial : IR.Procdesc.t -> t
type summary = AbductiveDomain.summary base_t
val summary_of_posts : IR.Procdesc.t -> t list -> summary list