Jsil_syntax.Cmd
module Expr = Gillian.Gil_syntax.Expr
JSIL Commmands *
type t =
| Basic of BCmd.t
JSIL basic commands
*)| Logic of LCmd.t
JSIL Logic commands
*)| Goto of int
Unconditional goto
*)| GuardedGoto of Expr.t * int * int
Conditional goto
*)| Call of string
* Expr.t
* Expr.t list
* int option
* (string * (string * Expr.t) list) option
Procedure call
*)| ECall of string * Expr.t * Expr.t list * int option
External Procedure call
*)| Apply of string * Expr.t * int option
Application-style procedure call
*)| Arguments of string
Arguments of the current function
*)| PhiAssignment of (string * Expr.t list) list
PHI assignment
*)| ReturnNormal
Normal return
*)| ReturnError
Error return
*)val pp_logic_bindings :
Stdlib.Format.formatter ->
(string * (string * Expr.t) list) ->
unit
val pp : Stdlib.Format.formatter -> t -> unit