Pulselib.PulseExecutionDomain
module AbductiveDomain = PulseAbductiveDomain
module DecompilerExpr = PulseDecompilerExpr
module LatentIssue = PulseLatentIssue
type 'abductive_domain_t base_t =
| ContinueProgram of 'abductive_domain_t
represents the state at the program point
*)| ExceptionRaised of 'abductive_domain_t
state after an exception has been thrown
*)| ExitProgram of AbductiveDomain.Summary.t
represents the state originating at exit/divergence.
*)| AbortProgram of AbductiveDomain.Summary.t
represents the state at the program point that caused an error
*)| LatentAbortProgram of {
astate : AbductiveDomain.Summary.t;
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.t;
address : DecompilerExpr.t;
must_be_valid : Pulselib.PulseBasicInterface.Trace.t
* Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason
option;
calling_context : (Pulselib.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
type t = AbductiveDomain.t base_t
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 pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
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 continue : AbductiveDomain.t -> t
type summary = AbductiveDomain.Summary.t base_t
val yojson_of_summary : summary -> Ppx_yojson_conv_lib.Yojson.Safe.t
val pp_summary : F.formatter -> summary -> unit
val to_name : 'a base_t -> string