Module Pulselib.PulseExecutionDomain

module F = Stdlib.Format
module AbductiveDomain = PulseAbductiveDomain
module DecompilerExpr = PulseDecompilerExpr
module Diagnostic = PulseDiagnostic
module LatentIssue = PulseLatentIssue
type stopped_execution =
  1. | ExitProgram of AbductiveDomain.Summary.t
  2. | AbortProgram of {
    1. astate : AbductiveDomain.Summary.t;
    2. diagnostic : Diagnostic.t;
    3. trace_to_issue : Pulselib.PulseBasicInterface.Trace.t;
    }
  3. | LatentAbortProgram of {
    1. astate : AbductiveDomain.Summary.t;
    2. latent_issue : LatentIssue.t;
    }
  4. | LatentInvalidAccess of {
    1. astate : AbductiveDomain.Summary.t;
    2. address : DecompilerExpr.t;
    3. must_be_valid : Pulselib.PulseBasicInterface.Trace.t * Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason option;
    4. calling_context : (Pulselib.PulseBasicInterface.CallEvent.t * IBase.Location.t) list;
    }
  5. | LatentSpecializedTypeIssue of {
    1. astate : AbductiveDomain.Summary.t;
    2. specialized_type : IR.Typ.Name.t;
    3. trace : Pulselib.PulseBasicInterface.Trace.t;
    }
type 'abductive_domain_t base_t =
  1. | ContinueProgram of 'abductive_domain_t
  2. | ExceptionRaised of 'abductive_domain_t
  3. | Stopped of stopped_execution
include Absint.AbstractDomain.Disjunct with type t := t
include Absint.AbstractDomain.Comparable with type t := t
include IStdlib.PrettyPrintable.PrintableType with type t := t
val leq : lhs:t -> rhs:t -> bool

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

val equal_fast : t -> t -> bool

equal_fast x y must imply x <=> y; it's a good idea for this function to be "fast", e.g. not depend on the size of its input

val is_normal : t -> bool

test if the abstract state represents exactly concrete states

val is_exceptional : t -> bool

test if the abstract state represents exactly exceptional concrete states

val is_executable : t -> bool

test if the abstract state represents executable states, e.g. ContinueProgram or ExceptionRaised.

val exceptional_to_normal : t -> t

convert all exceptional states into normal states (used when reaching a handler)

val is_active_loop : t -> IR.Procdesc.Node.id option

test if the abstract state is a loop invariant under inference and return the corresponding loop header id

val pp_with_kind : IStdlib.Pp.print_kind -> PulsePathContext.t option -> F.formatter -> t -> unit
val pp : F.formatter -> t -> unit
val continue : AbductiveDomain.t -> t
val summary_of_stopped_execution : stopped_execution -> AbductiveDomain.Summary.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
val pp_summary : IStdlib.Pp.print_kind -> F.formatter -> summary -> unit
val to_name : 'a base_t -> string