gillian » Gillian » Gil_syntax » Asrt

Module Gil_syntax.Asrt

type atom =

1. | Emp
   (*

   Empty heap

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

   Predicates

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

   Pure formula

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

   Typing assertion

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

   Core assertion

   *)
6. | Wand of{
   1. lhs : string * Expr.t list;
   2. rhs : string * 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 map : (Expr.t -> Expr.t) -> t -> t

• deprecated

  Use Visitors.endo instead

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 -> 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 -> 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 -> 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:Expr.t -> subst_with: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