Lifter (gillian.Debugger_lifter.Gil_fallback_lifter.Make.TLLifter.Gil.Lifter)

type t

The lifter's state

type memory_error

type tl_ast

type init_data

type pc_err

type memory

type cmd_report

type annot

type Stdlib.Effect.t +=

| Step : (Gillian.Logging.Report_id.t option * Gillian.Gil_syntax.Branch_case.t option * Gillian.Gil_syntax.Branch_case.path) -> cmd_report Debugger_lifter__.Lifter_intf.Types.executed_cmd_data Stdlib.Effect.t

val init : 
  proc_name:string ->
  all_procs:string list ->
  tl_ast option ->
  (annot, int) Gillian.Gil_syntax.Prog.t ->
  (t
   * (unit ->
   Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason))
    option

Given a proc name, a tl_ast, and the data from the first executed GIL command, initialise the lifter's state and handle the first command.

Returns None if lifting is unsupported (i.e. if tl_ast is None).

val init_exn : 
  proc_name:string ->
  all_procs:string list ->
  tl_ast option ->
  (annot, int) Gillian.Gil_syntax.Prog.t ->
  t
  * (unit ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason)

Exception-raising version of init.

val dump : t -> Yojson.Safe.t

Gives a JSON representation of the lifter's state.

Used for debugging problems with the lifter.

val step_over : 
  t ->
  Gillian.Logging.Report_id.t ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val step_in : 
  t ->
  Gillian.Logging.Report_id.t ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val step_out : 
  t ->
  Gillian.Logging.Report_id.t ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val step_back : 
  t ->
  Gillian.Logging.Report_id.t ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val step_branch : 
  t ->
  Gillian.Logging.Report_id.t ->
  Debugger_utils.Exec_map.Packaged.branch_case option ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val continue : 
  t ->
  Gillian.Logging.Report_id.t ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val continue_back : 
  t ->
  Gillian.Logging.Report_id.t ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val get_gil_map : t -> Debugger_utils.Exec_map.Packaged.t

Gets the non-lifted execution map of GIL commands.

In most cases, it's recommended to use a Gil_fallback_lifter, and just defer this call to the GIL lifter.

val get_lifted_map : t -> Debugger_utils.Exec_map.Packaged.t option

Gets the lifted execution map.

Returns None if lifting is not supported.

val get_lifted_map_exn : t -> Debugger_utils.Exec_map.Packaged.t

Exception-raising version of get_lifted_map.

val get_matches_at_id : 
  Gillian.Logging.Report_id.t ->
  t ->
  Gillian.Debugger.Utils.Exec_map.matching list

Gives a list of matches that occurred at the specified command.

val memory_error_to_exception_info : 
  (memory_error, annot, tl_ast)
    Debugger_lifter__.Lifter_intf.Types.memory_error_info ->
  Gillian.Debugger.Utils.exception_info

val add_variables : 
  store:(string * Gillian.Gil_syntax.Expr.t) list ->
  memory:memory ->
  is_gil_file:bool ->
  get_new_scope_id:(unit -> int) ->
  Gillian.Debugger.Utils.Variable.ts ->
  Gillian.Debugger.Utils.Variable.scope list

val parse_and_compile_files : 
  entrypoint:string ->
  string list ->
  ((annot, tl_ast, init_data)
     Gillian.Command_line.ParserAndCompiler.compiled_progs
   * string,
    pc_err)
    Stdlib.result

val init_manual : 
  string ->
  string list ->
  t
  * (cmd_report Debugger_lifter__.Lifter_intf.Types.executed_cmd_data option ->
  unit ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason)

A version of init that allows manually supplying exec_data instead of triggering the Step effect - this is used when Gil is not the primary lifter.

val handle_cmd : 
  Gillian.Logging.Report_id.t ->
  Gillian.Gil_syntax.Branch_case.t option ->
  cmd_report Debugger_lifter__.Lifter_intf.Types.executed_cmd_data ->
  t ->
  unit

val path_of_id : 
  Gillian.Logging.Report_id.t ->
  t ->
  Gillian.Gil_syntax.Branch_case.path

val should_skip_cmd : 
  cmd_report Debugger_lifter__.Lifter_intf.Types.executed_cmd_data ->
  t ->
  bool

val cases_at_id : 
  Gillian.Logging.Report_id.t ->
  t ->
  Gillian.Gil_syntax.Branch_case.t list