gillian » Gillian » Gil_syntax » Cmd

Module Gil_syntax.Cmd

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

Optional bindings for procedure calls

type function_call = {

1. var_name : string;
2. fun_name : Expr.t;
3. args : Expr.t list;
4. bindings : logic_bindings_t option;

}

type 'label t =

1. | Skip
   (*

   Skip

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

   Variable Assignment

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

   Action

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

   Logic commands

   *)
5. | Goto of 'label
   (*

   Unconditional goto

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

   Conditional goto

   *)
7. | Call of function_call * 'label option
   (*

   Procedure call

   *)
8. | Par of function_call list
   (*

   Parallel composition

   *)
9. | ECall of string * Expr.t * Expr.t list * 'label option
   (*

   External Procedure call

   *)
10. | Apply of string * Expr.t * 'label option
    (*

    Application-style procedure call

    *)
11. | Arguments of string
    (*

    Arguments of the currently executing function

    *)
12. | PhiAssignment of (string * Expr.t list) list
    (*

    PHI-assignment

    *)
13. | ReturnNormal
    (*

    Normal return

    *)
14. | ReturnError
    (*

    Error return

    *)
15. | Fail of string * 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

val call :
  ?bindings:logic_bindings_t ->
  ?error:'label ->
  string ->
  Expr.t ->
  Expr.t list ->
  'label t