Module Engine.Wands

module Subst = Gillian.Symbolic.Subst
module L = Logging
type wand = {
  1. lhs : string * Gillian.Gil_syntax.Expr.t list;
  2. rhs : string * Gillian.Gil_syntax.Expr.t list;
}
val wand_to_yojson : wand -> Yojson.Safe.t
val wand_of_yojson : Yojson.Safe.t -> wand Ppx_deriving_yojson_runtime.error_or
type query = {
  1. lname : string;
  2. rname : string;
  3. largs : Gillian.Gil_syntax.Expr.t list;
  4. r_ins : Gillian.Gil_syntax.Expr.t list;
  5. r_outs : Gillian.Gil_syntax.Expr.t option list;
}
val query_ins_outs : query -> Gillian.Gil_syntax.Expr.t list * Gillian.Gil_syntax.Expr.t option list
val make_query : pred_defs:MP.preds_tbl_t -> subst:(Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t option) -> wand -> query option

The in-parameters of a magic wand of the form P(_) -* Q(_) are:

  • all the parameters of P
  • the in parameters of Q
val pp_query : Stdlib.Format.formatter -> query -> unit
type t = wand list Stdlib.ref
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val sure_is_nonempty : 'a list Stdlib.ref -> bool
val length : 'a list Stdlib.ref -> int

Returns the number of wand assertions

val init : wand list -> t
val to_list : 'a Stdlib.ref -> 'a
val copy : 'a Stdlib.ref -> 'a Stdlib.ref
val is_empty : 'a list Stdlib.ref -> bool
val substitution_in_place : Subst.t -> wand list Stdlib.ref -> unit
val pp_wand : Stdlib.Format.formatter -> wand -> unit
val pp : Stdlib.Format.formatter -> wand list Stdlib.ref -> unit
val extend : 'a list Stdlib.ref -> 'a -> unit
val get_lvars : wand list Stdlib.ref -> Utils.Prelude.SS.t
val get_alocs : wand list Stdlib.ref -> Utils.Prelude.SS.t
val to_assertions : t -> Gillian.Gil_syntax.Asrt.t list
val wand_ins_outs : pred_defs:MP.preds_tbl_t -> wand -> Gillian.Gil_syntax.Expr.t list * Gillian.Gil_syntax.Expr.t list
val pop_nth : int -> 'a list Stdlib.ref -> 'a option
module Consume_wand : sig ... end
val consume_wand : pred_defs:MP.preds_tbl_t -> semantic_eq:(Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t -> bool) -> t -> query -> wand option