Module Pulselib__PulseOperations.Import
For open
ing in other modules.
type access_mode
=
Imported types for ease of use and so we can write variants without the corresponding module prefix
type 'abductive_domain_t execution_domain_base_t
= 'abductive_domain_t Pulselib.PulseDomainInterface.ExecutionDomain.base_t
=
|
ContinueProgram of 'abductive_domain_t
|
ExitProgram of Pulselib.PulseDomainInterface.AbductiveDomain.summary
|
AbortProgram of Pulselib.PulseDomainInterface.AbductiveDomain.summary
|
LatentAbortProgram of
{
astate : Pulselib.PulseDomainInterface.AbductiveDomain.summary;
latent_issue : Pulselib.PulseDomainInterface.LatentIssue.t;
}
|
LatentInvalidAccess of
{
astate : Pulselib.PulseDomainInterface.AbductiveDomain.summary;
address : Pulselib.PulseBasicInterface.AbstractValue.t;
must_be_valid : Pulselib.PulseBasicInterface.Trace.t;
calling_context : (Pulselib.PulseBasicInterface.CallEvent.t * IBase.Location.t) list;
}
|
ISLLatentMemoryError of Pulselib.PulseDomainInterface.AbductiveDomain.summary
type 'astate base_error
= 'astate Pulselib.PulseDomainInterface.AccessResult.error
=
|
PotentialInvalidAccess of
{
astate : 'astate;
address : Pulselib.PulseBasicInterface.AbstractValue.t;
must_be_valid : Pulselib.PulseBasicInterface.Trace.t;
}
|
PotentialInvalidAccessSummary of
{
astate : Pulselib.PulseDomainInterface.AbductiveDomain.summary;
address : Pulselib.PulseBasicInterface.AbstractValue.t;
must_be_valid : Pulselib.PulseBasicInterface.Trace.t;
}
|
ReportableError of
{
astate : 'astate;
diagnostic : Pulselib.PulseBasicInterface.Diagnostic.t;
}
|
ISLError of 'astate
Monadic syntax
include module type of IStdlib.IResult.Let_syntax
include module type of IStdlib.IStd.Result.Monad_infix
val let+ : ('ok, 'err) IStdlib.IStd.result -> ('ok -> 'okk) -> ('okk, 'err) IStdlib.IStd.result
val let* : ('ok, 'err) IStdlib.IStd.result -> ('ok -> ('okk, 'err) IStdlib.IStd.result) -> ('okk, 'err) IStdlib.IStd.result
val let<*> : 'a Pulselib.PulseDomainInterface.AccessResult.t -> ('a -> 'b Pulselib.PulseDomainInterface.AccessResult.t list) -> 'b Pulselib.PulseDomainInterface.AccessResult.t list
monadic "bind" but not really that turns an
AccessResult.t
into a list ofAccessResult.t
s (not really because the first type is not anAccessResult.t list
but just anAccessResult.t
)
val let<+> : 'a Pulselib.PulseDomainInterface.AccessResult.t -> ('a -> 'abductive_domain_t) -> 'abductive_domain_t execution_domain_base_t Pulselib.PulseDomainInterface.AccessResult.t list
monadic "map" but even less really that turns an
AccessResult.t
into an analysis result