Module S.SAInterpreter

Value type

Subst type

type store_t = SStore.t
type state_t = state
type state_err_t = SPState.err_t
val pp_state_err_t : Ppx_deriving_runtime.Format.formatter -> state_err_t -> Ppx_deriving_runtime.unit
val show_state_err_t : state_err_t -> Ppx_deriving_runtime.string
type state_vt
val state_vt_to_yojson : state_vt -> Yojson.Safe.t
val state_vt_of_yojson : Yojson.Safe.t -> state_vt Ppx_deriving_yojson_runtime.error_or
val pp_state_vt : Ppx_deriving_runtime.Format.formatter -> state_vt -> Ppx_deriving_runtime.unit
val show_state_vt : state_vt -> Ppx_deriving_runtime.string
type heap_t = heap_t
type init_data

Data necessary to initialize the state; language-dependent

type annot = annot

Command annotation; language-dependent

module Val : Gillian.General.Val.S with type t = vt
module Store : Gillian.General.Store.S with type t = store_t and type vt = vt
type invariant_frames = (string * state_t) list
val pp_err_t : Ppx_deriving_runtime.Format.formatter -> err_t -> Ppx_deriving_runtime.unit
val show_err_t : err_t -> Ppx_deriving_runtime.string
val err_t_to_yojson : err_t -> Yojson.Safe.t
val err_t_of_yojson : Yojson.Safe.t -> err_t Ppx_deriving_yojson_runtime.error_or
module CConf : sig ... end

Type of configurations: state, call stack, previous index, previous loop ids, current index, branching

type conf_t =
  1. | BConfErr of err_t list
  2. | BConfCont of state_t
type result_t = (state_t, state_vt, err_t) Exec_res.t

The result of execution

In the symbolic case, this is the result of one branch of execution

type 'result cont_func_f = ?selector:conf_selector -> unit -> 'result cont_func

To support the step-by-step behaviour of the debugger, execution is split into thunks; each invocation executes one GIL command. By supplying a branch path, or an ID and branch case, a particular branch of execution can be selected.

and 'result cont_func =
  1. | Finished of 'result list
  2. | Continue of {
    1. report_id : Gillian.Logging.Report_id.t option;
    2. branch_path : Gillian.Gil_syntax.Branch_case.path;
    3. new_branch_cases : Gillian.Gil_syntax.Branch_case.t list;
    4. cont_func : 'result cont_func_f;
    }
  3. | EndOfBranch of 'result * 'result cont_func_f
module Logging : sig ... end

Types and functions for logging to the database

val reset_call_graph : unit -> unit
val evaluate_lcmds : annot MP.prog -> Gillian.Gil_syntax.LCmd.t list -> ?annot:annot option -> state_t -> (state_t, state_err_t) Res_list.t

Evaluates a list of logical commands, in the context of a given state

val init_evaluate_proc : (result_t -> 'a) -> annot MP.prog -> string -> string list -> state_t -> 'a cont_func

Begins execution of a proc, given parameters and initial state

val evaluate_proc : (result_t -> 'a) -> annot MP.prog -> string -> string list -> state_t -> 'a list

As with init_evaluate_proc, but immediately executes the proc to completion

val check_leaks : result_t -> result_t