Module Pulselib.PulseBaseMemory

module Access : sig ... end
module AccessSet : IStdlib.IStd.Caml.Set.S with type AccessSet.elt = Access.t
module AddrTrace : sig ... end
module Edges : IStdlib.RecencyMap.S with type key = Access.t and type value = AddrTrace.t
include IStdlib.PrettyPrintable.PPMonoMap with type key = PulseBasicInterface.AbstractValue.t and type value = Edges.t
include IStdlib.PrettyPrintable.MonoMap
type key
type value
type t
val empty : t
val is_empty : t -> bool
val mem : key -> t -> bool
val add : key -> value -> t -> t
val update : key -> (value option -> value option) -> t -> t
val singleton : key -> value -> t
val remove : key -> t -> t
val merge : (key -> value option -> value option -> value option) -> t -> t -> t
val union : (key -> value -> value -> value option) -> t -> t -> t
val compare : (value -> value -> int) -> t -> t -> int
val equal : (value -> value -> bool) -> t -> t -> bool
val iter : (key -> value -> unit) -> t -> unit
val fold : (key -> value -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (key -> value -> bool) -> t -> bool
val exists : (key -> value -> bool) -> t -> bool
val filter : (key -> value -> bool) -> t -> t
val filter_map : (key -> value -> value option) -> t -> t
val partition : (key -> value -> bool) -> t -> t * t
val cardinal : t -> int
val bindings : t -> (key * value) list
val min_binding : t -> key * value
val min_binding_opt : t -> (key * value) option
val max_binding : t -> key * value
val max_binding_opt : t -> (key * value) option
val choose : t -> key * value
val choose_opt : t -> (key * value) option
val split : key -> t -> t * value option * t
val find : key -> t -> value
val find_opt : key -> t -> value option
val find_first : (key -> bool) -> t -> key * value
val find_first_opt : (key -> bool) -> t -> (key * value) option
val find_last : (key -> bool) -> t -> key * value
val find_last_opt : (key -> bool) -> t -> (key * value) option
val map : (value -> value) -> t -> t
val mapi : (key -> value -> value) -> t -> t
val is_singleton_or_more : t -> (key * 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:(key -> 'a -> value -> 'a * value) -> 'a * t
val of_seq : (key * value) Stdlib.Seq.t -> t
include IStdlib.PrettyPrintable.PrintableType with type t := t
type t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val pp_key : IStdlib.PrettyPrintable.F.formatter -> key -> unit
val compare : t -> t -> int
val equal : t -> t -> bool
val register_address : PulseBasicInterface.AbstractValue.t -> t -> t
val add_edge : PulseBasicInterface.AbstractValue.t -> Access.t -> AddrTrace.t -> t -> t
val find_edge_opt : PulseBasicInterface.AbstractValue.t -> Access.t -> t -> AddrTrace.t option
val has_edge : PulseBasicInterface.AbstractValue.t -> Access.t -> t -> bool
val yojson_of_t : t -> Yojson.Safe.t
val is_allocated : t -> PulseBasicInterface.AbstractValue.t -> bool

whether the address has a non-empty set of edges

val canonicalize : get_var_repr:(PulseBasicInterface.AbstractValue.t -> PulseBasicInterface.AbstractValue.t) -> t -> t 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 : (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.AbstractValue.t) -> t -> t PulseBasicInterface.SatUnsat.t