PulseModelsGenericArrayBackedCollection (infer.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