Module PulseAbductiveDomain.Stack

stack operations like BaseStack but that also take care of propagating facts to the precondition

val add : IR.Var.t -> BaseStack.value -> t -> t
val remove_vars : IR.Var.t list -> t -> t
val fold : (IR.Var.t -> BaseStack.value -> 'a -> 'a) -> t -> 'a -> 'a
val find_opt : IR.Var.t -> t -> BaseStack.value option
val eval : IBase.Location.t -> PulseBasicInterface.ValueHistory.t -> IR.Var.t -> t -> t * (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t)

return the value of the variable in the stack or create a fresh one if needed

val mem : IR.Var.t -> t -> bool
val exists : (IR.Var.t -> BaseStack.value -> bool) -> t -> bool
val keys : t -> IR.Var.t list