Pulselib.PulseBaseStackmodule type S = sig ... endValues are ValueOrigin.t, which should always be Unknown for program variables, and always be not Unknown for logical variables, as we record what was loaded into each logical variable. For example, after n$1 = *&p, n$1 should have p as its value origin.
include S with type value = Pulselib.PulseBasicInterface.ValueOrigin.tinclude IStdlib.PrettyPrintable.PPMonoMap
with type key = IR.Var.t
with type value = Pulselib.PulseBasicInterface.ValueOrigin.tinclude IStdlib.PrettyPrintable.MonoMap
with type key = IR.Var.t
with type value = Pulselib.PulseBasicInterface.ValueOrigin.ttype key = IR.Var.ttype value = Pulselib.PulseBasicInterface.ValueOrigin.tval empty : tval is_empty : t -> boolval cardinal : t -> intval is_singleton_or_more :
t ->
(key * value) IStdlib.IContainer.singleton_or_moreinclude IStdlib.PrettyPrintable.PrintableType with type t := tval pp : IStdlib.PrettyPrintable.F.formatter -> t -> unitval pp_key : IStdlib.PrettyPrintable.F.formatter -> key -> unitval yojson_of_t : t -> Yojson.Safe.tval canonicalize :
get_var_repr:
(Pulselib.PulseBasicInterface.AbstractValue.t ->
Pulselib.PulseBasicInterface.AbstractValue.t) ->
t ->
t Pulselib.PulseBasicInterface.SatUnsat.treplace each address in the stack by its canonical representative according to the current equality relation, represented by get_var_repr