Module Debugger_lifter

Interface for lifting execution of GIL commands to a target language

type match_result = Gillian.Debugger.Utils.Match_map.match_result =
  1. | Success
  2. | Failure
val match_result_to_yojson : match_result -> Yojson.Safe.t
val match_result_of_yojson : Yojson.Safe.t -> match_result Ppx_deriving_yojson_runtime.error_or
type ('err, 'annot, 'ast) memory_error_info = {
  1. error : 'err;
    (*

    The memory error that needs to be lifted

    *)
  2. command : (int Gillian.Gil_syntax.Cmd.t * 'annot) option;
    (*

    The command where it happened

    *)
  3. tl_ast : 'ast option;
    (*

    If the program was compiled from the target language, we keep the tl ast around

    *)
}
type 'cmd_report executed_cmd_data = {
  1. is_breakpoint : bool;
  2. next_kind : (Gillian.Gil_syntax.Branch_case.t, unit) Gillian.Debugger.Utils.Exec_map.next_kind;
  3. id : Gillian.Logging.Report_id.t;
  4. cmd_report : 'cmd_report;
  5. matches : Gillian.Debugger.Utils.Exec_map.matching list;
  6. errors : string list;
  7. branch_path : Gillian.Gil_syntax.Branch_case.path;
}
val executed_cmd_data_to_yojson : 'cmd_report. ('cmd_report -> Yojson.Safe.t) -> 'cmd_report executed_cmd_data -> Yojson.Safe.t
val executed_cmd_data_of_yojson : 'cmd_report. (Yojson.Safe.t -> 'cmd_report Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'cmd_report executed_cmd_data Ppx_deriving_yojson_runtime.error_or
type handle_cmd_result =
  1. | Stop of Gillian.Logging.Report_id.t option
  2. | ExecNext of Gillian.Logging.Report_id.t option * Gillian.Gil_syntax.Branch_case.t option
val handle_cmd_result_to_yojson : handle_cmd_result -> Yojson.Safe.t
val handle_cmd_result_of_yojson : Yojson.Safe.t -> handle_cmd_result Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> handle_cmd_result Ppx_deriving_yojson_runtime.error_or
type Stdlib.Effect.t +=
  1. | IsBreakpoint : (string * int list) -> bool Stdlib.Effect.t
module type S = sig ... end
val make_executed_cmd_data : ?is_breakpoint:bool -> (Gillian.Gil_syntax.Branch_case.t, unit) Gillian.Debugger.Utils.Exec_map.next_kind -> Gillian.Logging.Report_id.t -> 'cmd_report -> ?matches:Gillian.Debugger.Utils.Exec_map.matching list -> ?errors:string list -> Gillian.Gil_syntax.Branch_case.path -> 'cmd_report executed_cmd_data
module Gil_lifter : sig ... end

A basic "GIL-to-GIL" lifter implementation.

module Gil_fallback_lifter : sig ... end

A Lifter implementation that acts as a proxy to another lifter (TLLifter), while also keeping a Gil_lifter updated alongside.