PulseBaseMemory (infer.Pulselib.PulseBaseMemory)

module type S = sig ... end

include S
  with type key := Pulselib.PulseBasicInterface.AbstractValue.t
   and type out_of_map_t :=
         Pulselib.PulseBasicInterface.AbstractValue.t
         * Pulselib.PulseBasicInterface.ValueHistory.t
   and type in_map_t :=
         Pulselib.PulseBasicInterface.AbstractValue.t
         * Pulselib.PulseBasicInterface.ValueHistory.t

module Access : 
  Pulselib.PulseBasicInterface.Access.S
    with type key := Pulselib.PulseBasicInterface.AbstractValue.t

module Edges : sig ... end

include IStdlib.PrettyPrintable.PPMonoMap
  with type key := Pulselib.PulseBasicInterface.AbstractValue.t
   and type value = Edges.t

include IStdlib.PrettyPrintable.MonoMap
  with type key := Pulselib.PulseBasicInterface.AbstractValue.t
  with type value = Edges.t

type value = Edges.t

type t

val empty : t

val is_empty : t -> bool

val mem : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> bool

val add : Pulselib.PulseBasicInterface.AbstractValue.t -> value -> t -> t

val update : 
  Pulselib.PulseBasicInterface.AbstractValue.t ->
  (value option -> value option) ->
  t ->
  t

val singleton : Pulselib.PulseBasicInterface.AbstractValue.t -> value -> t

val remove : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> t

val merge : 
  (Pulselib.PulseBasicInterface.AbstractValue.t ->
    value option ->
    value option ->
    value option) ->
  t ->
  t ->
  t

val union : 
  (Pulselib.PulseBasicInterface.AbstractValue.t ->
    value ->
    value ->
    value option) ->
  t ->
  t ->
  t

val iter : 
  (Pulselib.PulseBasicInterface.AbstractValue.t -> value -> unit) ->
  t ->
  unit

val fold : 
  (Pulselib.PulseBasicInterface.AbstractValue.t -> value -> 'a -> 'a) ->
  t ->
  'a ->
  'a

val for_all : 
  (Pulselib.PulseBasicInterface.AbstractValue.t -> value -> bool) ->
  t ->
  bool

val exists : 
  (Pulselib.PulseBasicInterface.AbstractValue.t -> value -> bool) ->
  t ->
  bool

val filter : 
  (Pulselib.PulseBasicInterface.AbstractValue.t -> value -> bool) ->
  t ->
  t

val filter_map : 
  (Pulselib.PulseBasicInterface.AbstractValue.t -> value -> value option) ->
  t ->
  t

val partition : 
  (Pulselib.PulseBasicInterface.AbstractValue.t -> value -> bool) ->
  t ->
  t * t

val cardinal : t -> int

val bindings : t -> (Pulselib.PulseBasicInterface.AbstractValue.t * value) list

val min_binding : t -> Pulselib.PulseBasicInterface.AbstractValue.t * value

val min_binding_opt : 
  t ->
  (Pulselib.PulseBasicInterface.AbstractValue.t * value) option

val max_binding : t -> Pulselib.PulseBasicInterface.AbstractValue.t * value

val max_binding_opt : 
  t ->
  (Pulselib.PulseBasicInterface.AbstractValue.t * value) option

val choose : t -> Pulselib.PulseBasicInterface.AbstractValue.t * value

val choose_opt : 
  t ->
  (Pulselib.PulseBasicInterface.AbstractValue.t * value) option

val split : 
  Pulselib.PulseBasicInterface.AbstractValue.t ->
  t ->
  t * value option * t

val find : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> value

val find_opt : 
  Pulselib.PulseBasicInterface.AbstractValue.t ->
  t ->
  value option

val find_first : 
  (Pulselib.PulseBasicInterface.AbstractValue.t -> bool) ->
  t ->
  Pulselib.PulseBasicInterface.AbstractValue.t * value

val find_first_opt : 
  (Pulselib.PulseBasicInterface.AbstractValue.t -> bool) ->
  t ->
  (Pulselib.PulseBasicInterface.AbstractValue.t * value) option

val find_last : 
  (Pulselib.PulseBasicInterface.AbstractValue.t -> bool) ->
  t ->
  Pulselib.PulseBasicInterface.AbstractValue.t * value

val find_last_opt : 
  (Pulselib.PulseBasicInterface.AbstractValue.t -> bool) ->
  t ->
  (Pulselib.PulseBasicInterface.AbstractValue.t * value) option

val map : (value -> value) -> t -> t

val mapi : 
  (Pulselib.PulseBasicInterface.AbstractValue.t -> value -> value) ->
  t ->
  t

val is_singleton_or_more : 
  t ->
  (Pulselib.PulseBasicInterface.AbstractValue.t * value)
    IStdlib.IContainer.singleton_or_more

val fold_map : t -> init:'a -> f:('a -> value -> 'a * value) -> 'a * t

val fold_mapi : 
  t ->
  init:'a ->
  f:(Pulselib.PulseBasicInterface.AbstractValue.t -> 'a -> value -> 'a * value) ->
  'a * t

val of_seq : 
  (Pulselib.PulseBasicInterface.AbstractValue.t * value) Stdlib.Seq.t ->
  t

val to_seq : 
  t ->
  (Pulselib.PulseBasicInterface.AbstractValue.t * value) Stdlib.Seq.t

include IStdlib.PrettyPrintable.PrintableType with type t := t

val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit

val pp_key : 
  IStdlib.PrettyPrintable.F.formatter ->
  Pulselib.PulseBasicInterface.AbstractValue.t ->
  unit

val compare : t -> t -> int

val equal : t -> t -> bool

val register_address : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> t

val add_edge : 
  Pulselib.PulseBasicInterface.AbstractValue.t ->
  Access.t ->
  (Pulselib.PulseBasicInterface.AbstractValue.t
   * Pulselib.PulseBasicInterface.ValueHistory.t) ->
  t ->
  t

val find_edge_opt : 
  ?get_var_repr:
    (Pulselib.PulseBasicInterface.AbstractValue.t ->
      Pulselib.PulseBasicInterface.AbstractValue.t) ->
  Pulselib.PulseBasicInterface.AbstractValue.t ->
  Access.t ->
  t ->
  (Pulselib.PulseBasicInterface.AbstractValue.t
   * Pulselib.PulseBasicInterface.ValueHistory.t)
    option

val has_edge : 
  Pulselib.PulseBasicInterface.AbstractValue.t ->
  Access.t ->
  t ->
  bool

val is_allocated : t -> Pulselib.PulseBasicInterface.AbstractValue.t -> bool

whether the address has a non-empty set of edges

val yojson_of_t : t -> Yojson.Safe.t

val canonicalize : 
  get_var_repr:
    (Pulselib.PulseBasicInterface.AbstractValue.t ->
      Pulselib.PulseBasicInterface.AbstractValue.t) ->
  t ->
  t Pulselib.PulseBasicInterface.SatUnsat.t

replace each address in the heap by its canonical representative according to the current equality relation, represented by get_var_repr; also remove addresses that point to empty edges

val subst_var : 
  for_summary:bool ->
  (Pulselib.PulseBasicInterface.AbstractValue.t
   * Pulselib.PulseBasicInterface.AbstractValue.t) ->
  t ->
  t Pulselib.PulseBasicInterface.SatUnsat.t