Frama-C API - `Trace`

Execution trace, mapping execution stacks to sets of events occurring at this point

type t

type data = private {

}

val empty : t

val is_empty : t -> bool

val add_event : t -> Mt_cil.stack_elt -> event -> t

val add_states : t -> before:Mt_memory.Types.functions_states -> after:Mt_memory.Types.functions_states -> t

val add_prefix : Mt_cil.stack_elt -> t -> t

val find_at_stmt : t -> Frama_c_kernel.Cil_types.stmt -> (Mt_cil.stack_elt * t) list

val subtrace_at_call : t -> Mt_cil.stack_elt -> t

val at_root : t -> data option

val at_call : t -> Mt_cil.stack_elt -> data option

val union : t -> t -> t

val iter : t -> (Mt_cil.Stack.t -> event -> unit) -> unit

val iter' : t -> (event -> unit) -> unit

val fold : t -> (Mt_cil.Stack.t -> event -> 'a -> 'a) -> 'a -> 'a

val fold' : t -> (event -> 'a -> 'a) -> 'a -> 'a

val exists : t -> (Mt_cil.Stack.t -> event -> bool) -> bool

val find_events : (event -> bool) -> t -> events_set

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

val no_deep_call : t -> bool

Frama-C API - Trace