Module `PulseAbductiveDomain.Memory`

memory operations like BaseMemory but that also take care of propagating facts to the precondition

module Access = BaseMemory.Access

module Edges = BaseMemory.Edges

val add_edge : (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> Access.t -> (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> IBase.Location.t -> t -> t
val eval_edge : (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> Access.t -> t -> t * (PulseBasicInterface.AbstractValue.t * 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 find_opt : PulseBasicInterface.AbstractValue.t -> t -> BaseMemory.Edges.t option
val find_edge_opt : PulseBasicInterface.AbstractValue.t -> Access.t -> t -> (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) option