Module Gil_syntax.Asrt

GIL Assertions

type atom =
  1. | Emp
    (*

    Empty heap

    *)
  2. | Pred of string * Gillian.Gil_syntax.Expr.t list
    (*

    Predicates

    *)
  3. | Pure of Gillian.Gil_syntax.Expr.t
    (*

    Pure formula

    *)
  4. | Types of (Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Type.t) list
    (*

    Typing assertion

    *)
  5. | CorePred of string * Gillian.Gil_syntax.Expr.t list * Gillian.Gil_syntax.Expr.t list
    (*

    Core assertion

    *)
  6. | Wand of {
    1. lhs : string * Gillian.Gil_syntax.Expr.t list;
    2. rhs : string * Gillian.Gil_syntax.Expr.t list;
    }
    (*

    Magic wand of the form P(...) -* Q(...)

    *)
val atom_to_yojson : atom -> Yojson.Safe.t
val atom_of_yojson : Yojson.Safe.t -> atom Ppx_deriving_yojson_runtime.error_or
val equal_atom : atom -> atom -> Ppx_deriving_runtime.bool
type t = atom list
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val equal : t -> t -> Ppx_deriving_runtime.bool
val compare : atom -> atom -> int

Comparison of assertions

val prioritise : atom -> atom -> int

Sorting of assertions

module Set : Stdlib.Set.S with type elt := t

Sets of assertions

val lvars : t -> Utils.Prelude.SS.t

Get all the logical variables in a

val pvars : t -> Utils.Prelude.SS.t

Get all the program variables in a

val alocs : t -> Utils.Prelude.SS.t

Get all the abstract locations in a

val clocs : t -> Utils.Prelude.SS.t

Get all the concrete locations in a

val locs : t -> Utils.Prelude.SS.t

Get all locations in a

val pred_names : t -> string list

Returns a list with the names of the predicates that occur in a

val pure_asrts : t -> Gillian.Gil_syntax.Expr.t list

Returns a list with the pure assertions that occur in a

val is_pure_asrt : atom -> bool

Check if a is a pure assertion

val make_pure : t -> Gillian.Gil_syntax.Expr.t

Eliminate Emp assertions. Pure assertions are converted to a single formula. This function expects its argument to be a PURE assertion.

val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer

val pp_atom : Stdlib.Format.formatter -> atom -> unit
val full_pp : Stdlib.Format.formatter -> t -> unit

Full pretty-printer

val pp_atom_full : Stdlib.Format.formatter -> atom -> unit
val subst_clocs : (string -> Gillian.Gil_syntax.Expr.t) -> t -> t

subst_clocs subst a Substitutes expressions of the form Lit (Loc l) with subst l in a

val subst_expr_for_expr : to_subst:Gillian.Gil_syntax.Expr.t -> subst_with:Gillian.Gil_syntax.Expr.t -> t -> t

subst_expr_for_expr ~to_subst ~subst_with a substitutes every occurence of the expression to_subst with the expression subst_with in a

val pvars_to_lvars : t -> t

Move pvars to lvars