PulseAbductiveDomain.MemorySafe version of PulseBaseMemory
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.foldpre_or_post defaults to `Post
val find_edge_opt :
Pulselib.PulseBasicInterface.AbstractValue.t ->
PulseAccess.t ->
t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t)
optionval exists_edge :
?pre_or_post:[ `Pre | `Post ] ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
t ->
f:
((PulseAccess.t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t)) ->
bool) ->
boolpre_or_post defaults to `Post