Frama-C API - Mt_types
Kind of access to zones
module RW : Frama_c_kernel.Datatype.S with type t = rw
Multithread events
type event =
| ThreadExit of Mt_memory.Types.value
| VarAccess of rw * Frama_c_kernel.Locations.Zone.t
(*Access to some shared variables
*)| Dummy of string * Mt_memory.Types.value list
module Event : sig ... end
Maps from statements to multithread events, together with the context in which they occur
module EventsSet : sig ... end
type events_set = EventsSet.t
module Trace : sig ... end
Execution trace, mapping execution stacks to sets of events occurring at this point
Live threads/taken mutexes at a given point of execution
module type Presence = sig ... end
module ThreadPresence : Presence with type key = Eva__.Thread.t and module KeySet = Eva__Private.Thread.Set
module MutexPresence : Presence with type key = Eva__.Mutex.t and module KeySet = Eva__Private.Mutex.Set