Trace (frama-c-eva.Mthread.Mt

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