gillian » Gillian » General » Call_stack » Make

Module Call_stack.Make

Parameters

moduleVal : Val.S

moduleStore : Store.S with type vt = Val.t

Signature

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 : 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: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