Module Imandra_util.TEF

Trace Event Format

type json = Yojson.Safe.t
val enable : unit -> unit
val enabled : unit -> bool
val tef_endpoint : unit -> string

Obtain the endpoint for TEF tracing

type event_type =
| B

begin

| E

end

| I

instant

| C

counter

| P

sample

| A_b

async: begin 'b'

| A_n

async: snapshot 'n'

| A_e

async: end 'e'

| F_s

flow: start 's'

| F_t

flow: step 't'

| F_f

flow: end 'f'

| N

object: created

| O

object: shapshot

| D

object: destroyed

| M

metadata

type 'a emit_fun = ?⁠buf:Stdlib.Buffer.t -> ?⁠cat:string list -> ?⁠pid:int -> ?⁠tid:int -> ?⁠args:(string * json) list -> ?⁠name:string -> 'a

An emitter function.

parameter cat

list of categories for filtering the event

parameter name

the name of this event

parameter pid

the process ID

parameter tid

the thread ID

parameter arguments

list of arguments for the event, with a name for each

val emit : (event_type -> unit) emit_fun
val begin_ : (?⁠stack:string list -> unit -> unit) emit_fun
val exit : (?⁠stack:string list -> unit -> unit) emit_fun
val with_ : ((unit -> 'a) -> 'a) emit_fun
val with1 : (('a -> 'b) -> 'a -> 'b) emit_fun
val with2 : (('a -> 'b -> 'c) -> 'a -> 'b -> 'c) emit_fun
val with3 : (('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd) emit_fun
val obj_new : (id:string -> unit -> unit) emit_fun
val obj_snap : (snapshot:string -> id:string -> unit -> unit) emit_fun
val obj_delete : (id:string -> unit -> unit) emit_fun
val obj_with : (id:string -> (unit -> 'a) -> 'a) emit_fun
val obj_with1 : (id:string -> ('a -> 'b) -> 'a -> 'b) emit_fun
val a_begin : (id:string -> unit -> unit) emit_fun
val a_exit : (id:string -> unit -> unit) emit_fun
val a_snap : (id:string -> unit -> unit) emit_fun
val a_with : (id:string -> (unit -> 'a) -> 'a) emit_fun
val a_with1 : (id:string -> ('a -> 'b) -> 'a -> 'b) emit_fun
val f_begin : (id:string -> unit -> unit) emit_fun
val f_exit : (id:string -> unit -> unit) emit_fun
val f_snap : (id:string -> unit -> unit) emit_fun
val instant : (?⁠stack:string list -> unit -> unit) emit_fun
val counter : (cs:(string * int) list -> unit -> unit) emit_fun
val meta : (unit -> unit) emit_fun
val end_trace : unit -> unit

Call to end the trace and close the json file