Module Jsil_syntax.SLCmd

module SSubst = Gillian.Symbolic.Subst

Separation Logic Commmands *

type folding_info = string * (string * Expr.t) list
type unfold_info = (string * string) list
type t =
  1. | Fold of string * Expr.t list * folding_info option
    (*

    Fold

    *)
  2. | Unfold of string * Expr.t list * unfold_info option * bool
    (*

    Unfold

    *)
  3. | GUnfold of string
    (*

    Global Unfold

    *)
  4. | ApplyLem of string * Expr.t list * string list
    (*

    Apply lemma

    *)
  5. | SepAssert of Asrt.t * string list
    (*

    Assert

    *)
  6. | Invariant of Asrt.t * string list
    (*

    Invariant

    *)

JSIL Separation Logic commands.

val pp_folding_info : (string * (string * Expr.t) list) option Fmt.t
val pp_unfold_info : (string * string) list option Fmt.t
val pp : Stdlib.Format.formatter -> t -> unit