Pulselib.PulseModelsGenericArrayBackedCollection
val matchers : PulseModelsImport.matcher list
val eval :
Pulselib.PulseDomainInterface.PathContext.t ->
PulseOperationResult.Import.access_mode ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
(Pulselib.PulseDomainInterface.AbductiveDomain.t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t))
Pulselib.PulseDomainInterface.AccessResult.t
val access : Pulselib.PulseBasicInterface.Access.t
val field : IR.Fieldname.t
val size_field : IR.Fieldname.t
val element :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
(Pulselib.PulseDomainInterface.AbductiveDomain.t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t))
Pulselib.PulseDomainInterface.AccessResult.t
val eval_element :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
(Pulselib.PulseDomainInterface.AbductiveDomain.t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t))
Pulselib.PulseDomainInterface.AccessResult.t
val eval_pointer_to_last_element :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
(Pulselib.PulseDomainInterface.AbductiveDomain.t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t))
Pulselib.PulseDomainInterface.AccessResult.t
val size :
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
desc:string ->
PulseModelsImport.model_no_non_disj
val increase_size :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
desc:string ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
Pulselib.PulseDomainInterface.AbductiveDomain.t PulseOperationResult.t
val decrease_size :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
desc:string ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
Pulselib.PulseDomainInterface.AbductiveDomain.t PulseOperationResult.t
val empty :
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
desc:string ->
PulseModelsImport.model_no_non_disj
val default_constructor :
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
desc:string ->
PulseModelsImport.model_no_non_disj
val to_internal_size_deref :
Pulselib.PulseDomainInterface.PathContext.t ->
PulseOperationResult.Import.access_mode ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
(Pulselib.PulseDomainInterface.AbductiveDomain.t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t))
Pulselib.PulseDomainInterface.AccessResult.t
val assign_size_constant :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
constant:IR.IntLit.t ->
desc:string ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
Pulselib.PulseDomainInterface.AbductiveDomain.t PulseOperationResult.t
module Iterator : sig ... end