Module Soteria_rust_lib.Trace

module Terminal = Soteria.Terminal
type t = {
  1. op : string option;
    (*

    Current operation being performed, only if relevant

    *)
  2. loc : Charon.Meta.span_data option;
    (*

    Current code location if known

    *)
  3. stack : Charon.Meta.span_data Soteria.Terminal.Call_trace.t;
    (*

    Current call stack

    *)
}

Represents the current position in analysis.

val pp : Stdlib.Format.formatter -> t -> unit
val move_to : Charon.Meta.span_data -> t -> t
val move_to_opt : Charon.Meta.span_data option -> t -> t
val set_op : string -> t -> t
val push_to_stack : loc:Charon.Meta.span_data -> msg:string -> t -> t
val loc_or_default : t -> Charon.Meta.span_data
val empty : t
val rename : ?rev:bool -> int -> string -> t -> t