Module Jsil_syntax.Asrt

module SSubst = Gillian.Symbolic.Subst
type t =
  1. | Emp
    (*

    Empty heap

    *)
  2. | Star of t * t
    (*

    Separating conjunction

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

    Heap cell assertion

    *)
  4. | MetaData of Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t
    (*

    MetaData

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

    Predicates

    *)
  6. | EmptyFields of Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t
    (*

    emptyFields assertion

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

    Pure formula

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

    Typing assertion

    *)

JSIL logic assertions.

val compare : t -> t -> int
module MyAssertion : sig ... end
module Set : sig ... end
val pp : Stdlib.Format.formatter -> t -> unit
val full_pp : Stdlib.Format.formatter -> t -> unit
val pp_list : t list Fmt.t
val star : t list -> t