Module Pulselib__PulseAbductiveDomain.Memory
memory operations like BaseMemory but that also take care of propagating facts to the precondition
module Access = BaseMemory.Accessmodule Edges = BaseMemory.Edgesval add_edge : (Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t) -> Access.t -> (Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t) -> IBase.Location.t -> t -> tval eval_edge : (Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t) -> Access.t -> t -> t * (Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t)eval_edge (addr,hist) access astatefollows the edgeaddr --access--> .in memory and returns what it points to or creates a fresh value if that edge didn't exist.
val find_opt : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> BaseMemory.Edges.t optionval find_edge_opt : Pulselib.PulseBasicInterface.AbstractValue.t -> Access.t -> t -> (Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t) option