Parameter External.Call_stack

type vt = Val.t
type store_t = Store.t

A call stack is a list records, each of which contains 1) identifier of the current procedure (string) 2) arguments of the current procedure (list of values) 3) calling store 4) a list of loop invariant identifiers 5) variable that should hold the return value 6) index of the calling procedure from whence the procedure was called 7) normal continuation index in the calling procedure 8) optional error continuation index in the calling procedure

type stack_element = {
  1. pid : string;
  2. arguments : vt list;
  3. store : store_t option;
  4. loop_ids : string list;
  5. ret_var : Gillian.Gil_syntax.Var.t;
  6. call_index : int;
  7. continue_index : int;
  8. error_index : int option;
}
val stack_element_to_yojson : stack_element -> Yojson.Safe.t
val stack_element_of_yojson : Yojson.Safe.t -> stack_element Ppx_deriving_yojson_runtime.error_or
type t = stack_element list
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val empty : t
val push : t -> pid:string -> arguments:vt list -> ?store:store_t -> loop_ids:string list -> ret_var:Gillian.Gil_syntax.Var.t -> call_index:int -> continue_index:int -> ?error_index:int -> unit -> t
val get_cur_proc_id : t -> string

Get current procedure identifier

  • parameter cs

    Target call stack

  • returns

    Identifier of the procedure currently being executed

val get_cur_args : t -> vt list

Get current arguments

  • parameter cs

    Target call stack

  • returns

    Arguments of the procedure currently being executed

val get_loop_ids : t -> string list

Get current loop identifiers

  • parameter cs

    Target call stack

  • returns

    List of current loop identifiers

val copy : t -> t

Call stack copy

  • parameter cs

    Target call stack

  • returns

    Copy of the given call stack

val get_cur_procs : t -> string list
  • parameter cs

    Target call stack

  • returns

    All the procedure names in order in the callstack

val recursive_depth : t -> string -> int

Call stack recursive depth

  • parameter cs

    Target call stack

  • parameter pid

    Identified of the target procedure

  • returns

    The number of times the pid been recursively called

val pp : Stdlib.Format.formatter -> t -> unit

Call stack pretty printer

  • parameter fmt

    Formatter

  • parameter cs

    Call stack to pretty print

  • returns

    unit