Memory (infer.Pulselib.PulseAbductiveDomain.Memory)

val add_edge : 
  PathContext.t ->
  (Pulselib.PulseBasicInterface.AbstractValue.t
   * Pulselib.PulseBasicInterface.ValueHistory.t) ->
  PulseAccess.t ->
  (Pulselib.PulseBasicInterface.AbstractValue.t
   * Pulselib.PulseBasicInterface.ValueHistory.t) ->
  IBase.Location.t ->
  t ->
  t

val eval_edge : 
  (Pulselib.PulseBasicInterface.AbstractValue.t
   * Pulselib.PulseBasicInterface.ValueHistory.t) ->
  PulseAccess.t ->
  t ->
  t
  * (Pulselib.PulseBasicInterface.AbstractValue.t
     * Pulselib.PulseBasicInterface.ValueHistory.t)

eval_edge (addr,hist) access astate follows the edge addr --access--> . in memory and returns what it points to or creates a fresh value if that edge didn't exist.

val fold_edges : 
  ?pre_or_post:[ `Pre | `Post ] ->
  Pulselib.PulseBasicInterface.AbstractValue.t ->
  (t,
    PulseAccess.t
    * (Pulselib.PulseBasicInterface.AbstractValue.t
       * Pulselib.PulseBasicInterface.ValueHistory.t),
    _)
    IStdlib.IStd.Container.fold

pre_or_post defaults to `Post

val find_edge_opt : 
  Pulselib.PulseBasicInterface.AbstractValue.t ->
  PulseAccess.t ->
  t ->
  (Pulselib.PulseBasicInterface.AbstractValue.t
   * Pulselib.PulseBasicInterface.ValueHistory.t)
    option

val exists_edge : 
  ?pre_or_post:[ `Pre | `Post ] ->
  Pulselib.PulseBasicInterface.AbstractValue.t ->
  t ->
  f:
    ((PulseAccess.t
      * (Pulselib.PulseBasicInterface.AbstractValue.t
         * Pulselib.PulseBasicInterface.ValueHistory.t)) ->
      bool) ->
  bool

pre_or_post defaults to `Post

val fold_merge_edges : 
  [ `Pre | `Post ] ->
  (t
   * (Pulselib.PulseBasicInterface.AbstractValue.t
      * Pulselib.PulseBasicInterface.ValueHistory.t)
       option) ->
  (t
   * (Pulselib.PulseBasicInterface.AbstractValue.t
      * Pulselib.PulseBasicInterface.ValueHistory.t)
       option) ->
  init:'acc ->
  f:
    ('acc ->
      Pulselib.PulseBasicInterface.Access.t ->
      PulseBaseMemory.Edges.value option ->
      PulseBaseMemory.Edges.value option ->
      'acc * PulseBaseMemory.Edges.value option) ->
  'acc * PulseBaseMemory.value

merge the stacks of the given astates into one and set the stack of the first abstract state to be the merged stack