Module Gil_syntax.Cmd

GIL Commands

type logic_bindings_t = string * (string * Gillian.Gil_syntax.Expr.t) list

Optional bindings for procedure calls

type 'label t =
  1. | Skip
    (*

    Skip

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

    Variable Assignment

    *)
  3. | LAction of string * string * Gillian.Gil_syntax.Expr.t list
    (*

    Action

    *)
  4. | Logic of Gillian.Gil_syntax.LCmd.t
    (*

    Logic commands

    *)
  5. | Goto of 'label
    (*

    Unconditional goto

    *)
  6. | GuardedGoto of Gillian.Gil_syntax.Expr.t * 'label * 'label
    (*

    Conditional goto

    *)
  7. | Call of string * Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t list * 'label option * logic_bindings_t option
    (*

    Procedure call

    *)
  8. | ECall of string * Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t list * 'label option
    (*

    External Procedure call

    *)
  9. | Apply of string * Gillian.Gil_syntax.Expr.t * 'label option
    (*

    Application-style procedure call

    *)
  10. | Arguments of string
    (*

    Arguments of the currently executing function

    *)
  11. | PhiAssignment of (string * Gillian.Gil_syntax.Expr.t list) list
    (*

    PHI-assignment

    *)
  12. | ReturnNormal
    (*

    Normal return

    *)
  13. | ReturnError
    (*

    Error return

    *)
  14. | Fail of string * Gillian.Gil_syntax.Expr.t list
    (*

    Failure

    *)
val to_yojson : ('label -> Yojson.Safe.t) -> 'label t -> Yojson.Safe.t
val of_yojson : (Yojson.Safe.t -> 'label Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'label t Ppx_deriving_yojson_runtime.error_or
val equal : ('label -> 'label -> Ppx_deriving_runtime.bool) -> 'label t -> 'label t -> Ppx_deriving_runtime.bool
val pp : pp_label:'a Fmt.t -> Stdlib.Format.formatter -> 'a t -> unit

Pretty-printer

val pp_labeled : Stdlib.Format.formatter -> string t -> unit

Pretty-printer for labelled programs

val pp_indexed : Stdlib.Format.formatter -> int t -> unit

Pretty-printer for integer-indexed programs

val successors : int t -> int -> int list

Possible successors of an command (in integer indexing)

val pvars : 'a t -> Utils.Containers.SS.t

Program variable collector

val lvars : 'a t -> Utils.Containers.SS.t

Logical variable collector

val locs : 'a t -> Utils.Containers.SS.t

Location collector