gillian » Gillian » Gil_syntax » Branch_case

Module Gil_syntax.Branch_case

type t' =

1. | GuardedGoto of bool
   (*

   Effectively if/else; either true or false case

   *)
2. | LCmd
   (*

   Logical command

   *)
3. | SpecExec of Flag.t
   (*

   Spec execution

   *)
4. | LAction
   (*

   Logical action

   *)
5. | LActionFail
   (*

   Failed logical action

   *)

val t'_to_yojson : t' -> Yojson.Safe.t

val t'_of_yojson : Yojson.Safe.t -> t' Ppx_deriving_yojson_runtime.error_or

val pp_t' :
  Ppx_deriving_runtime.Format.formatter ->
  t' ->
  Ppx_deriving_runtime.unit

val show_t' : t' -> Ppx_deriving_runtime.string

type t = t' * int

val to_yojson : t -> Yojson.Safe.t

val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or

val pp :
  Ppx_deriving_runtime.Format.formatter ->
  t ->
  Ppx_deriving_runtime.unit

val show : t -> Ppx_deriving_runtime.string

type path = t list

A list of branch cases describes the path of execution.

Every termination of a symbolic execution is uniquely identified by its branch path.

val path_to_yojson : path -> Yojson.Safe.t

val path_of_yojson : Yojson.Safe.t -> path Ppx_deriving_yojson_runtime.error_or

val pp_path :
  Ppx_deriving_runtime.Format.formatter ->
  path ->
  Ppx_deriving_runtime.unit

val show_path : path -> Ppx_deriving_runtime.string

val pp_short : Stdlib.Format.formatter -> t -> unit