Module Jsil_syntax.LCmd

module SSubst = Gillian.Symbolic.Subst

Logic Commmands *

type t =
  1. | If of Expr.t * t list * t list
    (*

    If-then-else

    *)
  2. | Branch of Expr.t
    (*

    branching on a FO formual

    *)
  3. | Macro of string * Expr.t list
    (*

    Macro

    *)
  4. | Assert of Expr.t
    (*

    Assert

    *)
  5. | Assume of Expr.t
    (*

    Assume

    *)
  6. | AssumeType of Expr.t * Type.t
    (*

    Assume Type

    *)
  7. | FreshSVar of string
  8. | SL of SLCmd.t

JSIL logic commands.

val pp : t Fmt.t