Module PulseOperations.Import

For opening in other modules.

type access_mode =
| Read
| Write
| NoAccess

The initialized-ness of the address is not checked when it evaluates a heap address without actual memory access, for example, when evaluating &x.f we need to check initialized-ness of x, not that of x.f.

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 PulseDomainInterface.ExecutionDomain.base_t =
| ContinueProgram of 'abductive_domain_t
| ExitProgram of PulseDomainInterface.AbductiveDomain.summary
| AbortProgram of PulseDomainInterface.AbductiveDomain.summary
| LatentAbortProgram of {
astate : PulseDomainInterface.AbductiveDomain.summary;
latent_issue : PulseDomainInterface.LatentIssue.t;
}
| LatentInvalidAccess of {
astate : PulseDomainInterface.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;
}
| ISLLatentMemoryError of PulseDomainInterface.AbductiveDomain.summary
type 'astate base_error = 'astate PulseDomainInterface.AccessResult.error =
| PotentialInvalidAccess of {
astate : 'astate;
address : PulseBasicInterface.AbstractValue.t;
must_be_valid : PulseBasicInterface.Trace.t * PulseBasicInterface.Invalidation.must_be_valid_reason option;
}
| PotentialInvalidAccessSummary of {
astate : PulseDomainInterface.AbductiveDomain.summary;
address : PulseBasicInterface.AbstractValue.t;
must_be_valid : PulseBasicInterface.Trace.t * PulseBasicInterface.Invalidation.must_be_valid_reason option;
}
| ReportableError of {
astate : 'astate;
diagnostic : 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 (>>=) : ('a, 'e) Core_kernel__Result.t -> ('a -> ('b, 'e) Core_kernel__Result.t) -> ('b, 'e) Core_kernel__Result.t
val (>>|) : ('a, 'e) Core_kernel__Result.t -> ('a -> 'b) -> ('b, 'e) Core_kernel__Result.t
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 PulseDomainInterface.AccessResult.t -> ('a -> 'b PulseDomainInterface.AccessResult.t list) -> 'b PulseDomainInterface.AccessResult.t list

monadic "bind" but not really that turns an AccessResult.t into a list of AccessResult.ts (not really because the first type is not an AccessResult.t list but just an AccessResult.t)

val let<+> : 'a PulseDomainInterface.AccessResult.t -> ('a -> 'abductive_domain_t) -> 'abductive_domain_t execution_domain_base_t PulseDomainInterface.AccessResult.t list

monadic "map" but even less really that turns an AccessResult.t into an analysis result