Frama-C:
Plug-ins:
Libraries:

Frama-C API - Mt_types

Kind of access to zones

type rw =
  1. | Read
  2. | Write of Frama_c_kernel.Locations.location
  3. | ReadPos of Eva__.Position.t
  4. | WritePos of Eva__.Position.t
module RW : sig ... end

Multithread events

type event =
  1. | CreateThread of Eva__.Thread.t
  2. | StartThread of Eva__.Thread.t
  3. | SuspendThread of Eva__.Thread.t
  4. | CancelThread of Eva__.Thread.t
  5. | ThreadExit of Mt_memory.Types.value
  6. | MutexLock of Eva__.Mutex.t
  7. | MutexRelease of Eva__.Mutex.t
  8. | CreateQueue of Eva__.Mqueue.t * int option
  9. | SendMsg of Eva__.Mqueue.t * Mt_memory.Types.slice * int
    (*

    SendMsg(q, (msg, size))

    • q: the queue
    • msg: content of the message
    • size: size of the message
    *)
  10. | ReceiveMsg of Eva__.Mqueue.t * Mt_memory.Types.pointer * int
    (*

    ReceiveMsg(q, ptr, size)

    • q: the queue
    • ptr: loc to which the message must be written
    • size: max size to read
    *)
  11. | VarAccess of rw * Frama_c_kernel.Locations.Zone.t
    (*

    Access to some shared variables

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