Module Gil_syntax.Branch_case

Reasons for a branch in execution.

These are used to reason about execution when using the debugger.

Note: most of these haven't yet been properly reasoned about, so they won't be very informative.

type t =
  1. | GuardedGoto of bool
    (*

    Effectively if/else; either true or false case

    *)
  2. | LCmd of int
    (*

    Logical command

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

    Spec execution

    *)
  4. | LAction of int
    (*

    Logical action

    *)
  5. | LActionFail of int
    (*

    Failed logical action

    *)
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