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
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 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 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_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 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