PulseModelsImport.Basic
val continue : 'a -> 'a PulseOperationResult.Import.execution_domain_base_t
val ok_continue :
'a ->
('a PulseOperationResult.Import.execution_domain_base_t, 'b)
PulseOperationResult.Import.pulse_result
list
val map_continue :
('a, 'b) PulseOperationResult.Import.pulse_result ->
('a PulseOperationResult.Import.execution_domain_base_t, 'b)
PulseOperationResult.Import.pulse_result
val shallow_copy_value :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
Pulselib.PulseBasicInterface.ValueHistory.event ->
IR.Ident.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
Pulselib.PulseDomainInterface.AbductiveDomain.t
PulseOperationResult.Import.execution_domain_base_t
Pulselib.PulseDomainInterface.AccessResult.t
list
val shallow_copy :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
Pulselib.PulseBasicInterface.ValueHistory.event ->
IR.Ident.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
Pulselib.PulseDomainInterface.AbductiveDomain.t
PulseOperationResult.Import.execution_domain_base_t
Pulselib.PulseDomainInterface.AccessResult.t
list
val shallow_copy_model :
string ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
model_no_non_disj
val deep_copy :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
value:
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
desc:string ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
(Pulselib.PulseDomainInterface.AbductiveDomain.t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t))
PulseOperationResult.t
val alloc_value_address :
IR.Typ.t ->
desc:string ->
model_data ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
(Pulselib.PulseDomainInterface.AbductiveDomain.t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t))
PulseOperationResult.t
val early_exit : model_no_non_disj
val return_int : desc:string -> int64 -> model_no_non_disj
val nondet : desc:string -> model_no_non_disj
val skip : model_no_non_disj
val id_first_arg :
desc:string ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
model_no_non_disj
val free_or_delete :
[< `Delete | `Free ] ->
Pulselib.PulseBasicInterface.Invalidation.t ->
Pulselib.PulseBasicInterface.ValueOrigin.t
Absint.ProcnameDispatcher.Call.FuncArg.t ->
model
val alloc_not_null :
?desc:string ->
Pulselib.PulseBasicInterface.Attribute.allocator ->
IR.Exp.t option ->
initialize:bool ->
model_data ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
Pulselib.PulseDomainInterface.AbductiveDomain.t PulseOperationResult.t
val alloc_no_leak_not_null :
?desc:string ->
IR.Exp.t option ->
initialize:bool ->
model_data ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
Pulselib.PulseDomainInterface.AbductiveDomain.t PulseOperationResult.t
val call_constructor :
IR.Typ.name ->
IR.Typ.t list ->
Pulselib.PulseBasicInterface.ValueOrigin.t
Absint.ProcnameDispatcher.Call.FuncArg.t
list ->
IR.Exp.t ->
model_data ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
Pulselib.PulseDomainInterface.NonDisjDomain.t ->
Pulselib.PulseDomainInterface.ExecutionDomain.t
Pulselib.PulseDomainInterface.AccessResult.t
list
* Pulselib.PulseDomainInterface.NonDisjDomain.t
val unknown_call :
string ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t)
Absint.ProcnameDispatcher.Call.FuncArg.t
list ->
model_no_non_disj
val matchers : matcher list