Pulselib.PulseAccessResult
module AbductiveDomain = PulseAbductiveDomain
module DecompilerExpr = PulseDecompilerExpr
module Diagnostic = PulseDiagnostic
type error =
| PotentialInvalidAccess of {
astate : AbductiveDomain.t;
address : DecompilerExpr.t;
must_be_valid : Pulselib.PulseBasicInterface.Trace.t
* Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason
option;
}
| PotentialInvalidSpecializedCall of {
astate : AbductiveDomain.t;
specialized_type : IR.Typ.Name.t;
trace : Pulselib.PulseBasicInterface.Trace.t;
}
| ReportableError of {
astate : AbductiveDomain.t;
diagnostic : Diagnostic.t;
}
| WithSummary of error * AbductiveDomain.Summary.t
An error for which the summary corresponding to the abstract state has already been computed, to avoid having to compute the summary for a given abstract state multiple times. For convenience this is part of the error
datatype but the invariant that an error
within a WithSummary (error, summary)
cannot itself be a WithSummary _
.
val astate_of_error : error -> AbductiveDomain.t
type 'a t = ('a, error) PulseResult.t
val with_summary :
('a, error * AbductiveDomain.Summary.t) PulseResult.t ->
'a t
type abductive_error = [
| `PotentialInvalidAccess of
AbductiveDomain.t
* Pulselib.PulseBasicInterface.AbstractValue.t
* (Pulselib.PulseBasicInterface.Trace.t
* Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason option)
]
Intermediate datatype since AbductiveDomain
cannot refer to this module without creating a circular dependency.
Purposefully omits `MemoryLeak
errors as it's a good idea to double-check if you really want to report a leak.
type abductive_summary_error = [
| `PotentialInvalidAccessSummary of
AbductiveDomain.Summary.t
* AbductiveDomain.t
* DecompilerExpr.t
* (Pulselib.PulseBasicInterface.Trace.t
* Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason option)
]
val of_result_f : ('a, error) IStdlib.IStd.result -> f:(error -> 'a) -> 'a t
val of_result :
(AbductiveDomain.t, error) IStdlib.IStd.result ->
AbductiveDomain.t t
val of_abductive_summary_error :
[< abductive_summary_error ] ->
error * AbductiveDomain.Summary.t
val of_abductive_result :
('a, [< abductive_error ]) IStdlib.IStd.result ->
'a t
val of_abductive_summary_result :
('a, [< abductive_summary_error ]) IStdlib.IStd.result ->
('a, error * AbductiveDomain.Summary.t) PulseResult.t
val ignore_leaks :
(AbductiveDomain.Summary.t,
[< `MemoryLeak of
AbductiveDomain.Summary.t
* AbductiveDomain.t
* Pulselib.PulseBasicInterface.Attribute.allocator
* Pulselib.PulseBasicInterface.Trace.t
* IBase.Location.t
| `JavaResourceLeak of
AbductiveDomain.Summary.t
* AbductiveDomain.t
* IR.JavaClassName.t
* Pulselib.PulseBasicInterface.Trace.t
* IBase.Location.t
| `HackUnawaitedAwaitable of
AbductiveDomain.Summary.t
* AbductiveDomain.t
* Pulselib.PulseBasicInterface.Trace.t
* IBase.Location.t
| `CSharpResourceLeak of
AbductiveDomain.Summary.t
* AbductiveDomain.t
* IR.CSharpClassName.t
* Pulselib.PulseBasicInterface.Trace.t
* IBase.Location.t
| abductive_summary_error ])
IStdlib.IStd.result ->
(AbductiveDomain.Summary.t, [> abductive_summary_error ]) IStdlib.IStd.result