Module G_interpreter.Make

Parameters

module Val : Val.S
module ESubst : ESubst.S with type vt = Val.t and type t = Val.et
module Store : Store.S with type vt = Val.t
module State : State.S with type vt = Val.t and type st = ESubst.t and type store_t = Store.t

Signature

type vt = Val.t

Value type

type st = ESubst.t

Subst type

type store_t = Store.t
type state_t = State.t
type state_err_t = State.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 = 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 = State.heap_t
type init_data = State.init_data

Data necessary to initialize the state; language-dependent

type annot = PC.Annot.t

Command annotation; language-dependent

module Val : General.Val.S with type t = vt
module Store : General.Store.S with type t = store_t and type vt = vt
type invariant_frames = (string * state_t) list
type err_t = (vt, state_err_t) Exec_err.t
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

The result of execution

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

type conf_selector =
  1. | Path of Gil_syntax.Branch_case.path
  2. | IdCase of Logging.Report_id.t * Gil_syntax.Branch_case.t option
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 : Logging.Report_id.t option;
    2. branch_path : Gil_syntax.Branch_case.path;
    3. new_branch_cases : 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 call_graph : Utils.Call_graph.t
val reset_call_graph : unit -> unit
val evaluate_lcmds : annot Engine.MP.prog -> Gil_syntax.LCmd.t list -> ?annot:annot option -> state_t -> (state_t, state_err_t) Engine.Res_list.t

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

val init_evaluate_proc : (result_t -> 'a) -> annot Engine.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 Engine.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