gillian » Gillian » Debugger » Utils » Match_map » Make_builder » Verification » SAInterpreter

Module Verification.SAInterpreter

module Call_stack : General.Call_stack.S

type vt = Symbolic.Values.t

Value type

type st = Symbolic.Subst.t

Subst type

type store_t = Engine.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 : 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) General.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

type result_t = (state_t, state_vt, err_t) Engine.Exec_res.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