PulseAbductiveDomain.Memory
Safe 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.fold
pre_or_post
defaults to `Post
val find_edge_opt :
Pulselib.PulseBasicInterface.AbstractValue.t ->
PulseAccess.t ->
t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t)
option
val exists_edge :
?pre_or_post:[ `Pre | `Post ] ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
t ->
f:
((PulseAccess.t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t)) ->
bool) ->
bool
pre_or_post
defaults to `Post