Module Debugger_utils

Miscellaneous types and functions for debugger-related purposes

val location_to_display_location : Gillian.Utils.Location.t -> Gillian.Utils.Location.t

Converts a GIL location (column number starts from 0) to a VSCode location (column number starts from 1)

type stop_reason =
  1. | Step
    (*

    The step has been completed

    *)
  2. | ReachedStart
    (*

    The start of the program has been reached (when executing backwards)

    *)
  3. | ReachedEnd
    (*

    The end of the program has been reached

    *)
  4. | Breakpoint
    (*

    A breakpoint has been reached

    *)
  5. | ExecutionError
    (*

    An error in execution has occurred

    *)

Explains why the debugger has stopped

val stop_reason_to_yojson : stop_reason -> Yojson.Safe.t
val stop_reason_of_yojson : Yojson.Safe.t -> stop_reason Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> stop_reason Ppx_deriving_yojson_runtime.error_or
type frame = {
  1. index : int;
    (*

    The index of the frame in the stack

    *)
  2. name : string;
    (*

    The name of the frame

    *)
  3. source_path : string;
    (*

    The path to the source file of the relevant code

    *)
  4. start_line : int;
    (*

    The line number of the start of the relevant code

    *)
  5. start_column : int;
    (*

    The column number of the start of the relevant code

    *)
  6. end_line : int;
    (*

    The line number of the end of the relevant code

    *)
  7. end_column : int;
    (*

    The column number of the end of the relevant code

    *)
}

Describes a frame on the stack of execution

val make_frame : index:int -> name:string -> source_path:string -> start_line:int -> start_column:int -> end_line:int -> end_column:int -> frame
type 'memory astate = {
  1. store : (string * Gillian.Gil_syntax.Expr.t) list;
  2. memory : 'memory;
  3. pfs : Gillian.Symbolic.Pure_context.t option;
  4. types : Gillian.Symbolic.Type_env.t option;
  5. preds : Engine.Preds.t option;
}
val make_astate : ?store:(string * Gillian.Gil_syntax.Expr.t) list -> memory:'a -> ?pfs:Gillian.Symbolic.Pure_context.t -> ?types:Gillian.Symbolic.Type_env.t -> ?preds:Engine.Preds.t -> unit -> 'a astate
val proc_id_prefix : string
val proc_id_prefix_len : int
val proc_name_of_id : string -> string option
type exception_info = {
  1. id : string;
  2. description : string option;
}

Describes an exception

module Variable : sig ... end

Representation of variables for the debugger

module Exec_map : sig ... end

A map of execution of a function (symbolic or otherwise).

module Match_map : sig ... end

A map of a matching.