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 AbductiveDomain.summary

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

| LatentInvalidAccess of {
astate : AbductiveDomain.summary;
address : PulseBasicInterface.AbstractValue.t;
must_be_valid : PulseBasicInterface.Trace.t * PulseBasicInterface.Invalidation.must_be_valid_reason option;
calling_context : (PulseBasicInterface.CallEvent.t * IBase.Location.t) list;
}

if address is ever observed to be invalid then there is an invalid access because it must_be_valid

| ISLLatentMemoryError of AbductiveDomain.summary

represents the state at the program point that might cause an error; used for Config.pulse_isl

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.Tenv.t -> IR.Procdesc.t -> t
val is_unsat_cheap : t -> bool

see PulsePathCondition.is_unsat_cheap

type summary = AbductiveDomain.summary base_t
val compare_summary : summary -> summary -> int
val equal_summary : summary -> summary -> bool
val yojson_of_summary : summary -> Ppx_yojson_conv_lib.Yojson.Safe.t