Module Mthread.Mt_types

Kind of access to zones

type rw =
  1. | Read
  2. | Write of Frama_c_kernel.Locations.location
module RW : sig ... end

Multithread events

type event =
  1. | ThreadExit of Mt_memory.Types.value
  2. | VarAccess of rw * Frama_c_kernel.Locations.Zone.t
    (*

    Access to some shared variables

    *)
  3. | 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

type presence_flag =
  1. | NotPresent
  2. | Present
  3. | MaybePresent
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