Make (gillian.Debugger.Symbolic

Parameters

module ID : Engine.Init_data.S

module PC : Gillian.Command_line.ParserAndCompiler.S with type init_data = ID.t

module V : 
  Engine.Verifier.S
    with type SPState.init_data = ID.t
     and type annot = PC.Annot.t

module Lifter : 
  Gillian.Debugger.Lifter.S
    with type memory = V.SAInterpreter.heap_t
     and type memory_error = V.SPState.m_err_t
     and type tl_ast = PC.tl_ast
     and type cmd_report = V.SAInterpreter.Logging.ConfigReport.t
     and type annot = PC.Annot.t
     and type init_data = PC.init_data
     and type pc_err = PC.err

Signature

type tl_ast

type t

module Inspect : sig ... end

val launch : string -> string option -> (t, string) Stdlib.result

val jump_to_id : 
  Gillian.Logging.Report_id.t ->
  t ->
  (unit, string) Stdlib.result

val step_in : t -> Gillian.Debugger.Utils.stop_reason

val step : ?reverse:bool -> t -> Gillian.Debugger.Utils.stop_reason

val step_specific : 
  Debugger_utils.Exec_map.Packaged.branch_case option ->
  Gillian.Logging.Report_id.t ->
  t ->
  (Gillian.Debugger.Utils.stop_reason, string) Stdlib.result

val step_out : t -> Gillian.Debugger.Utils.stop_reason

val run : 
  ?reverse:bool ->
  ?launch:bool ->
  t ->
  Gillian.Debugger.Utils.stop_reason

val start_proc : 
  string ->
  t ->
  (Gillian.Debugger.Utils.stop_reason, string) Stdlib.result

val terminate : t -> unit

val get_frames : t -> Gillian.Debugger.Utils.frame list

val get_scopes : t -> Gillian.Debugger.Utils.Variable.scope list

val get_variables : int -> t -> Gillian.Debugger.Utils.Variable.t list

val get_exception_info : t -> Gillian.Debugger.Utils.exception_info

val set_breakpoints : string option -> int list -> t -> unit