package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

Kind of access to zones

Sourcetype rw =

Sourcemodule RW : sig ... end

Multithread events

Sourcetype event =

| CreateThread of Eva__.Thread.t
| StartThread of Eva__.Thread.t
| SuspendThread of Eva__.Thread.t
| CancelThread of Eva__.Thread.t
| ThreadExit of Mt_memory.Types.value
| MutexLock of Eva__.Mutex.t
| MutexRelease of Eva__.Mutex.t
| CreateQueue of Eva__.Mqueue.t * int option
| 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
*)
| 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
*)
| VarAccess of rw * Frama_c_kernel.Locations.Zone.t
(*
Access to some shared variables
*)
| Dummy of string * Mt_memory.Types.value list

Sourcemodule Event : sig ... end

Maps from statements to multithread events, together with the context in which they occur

Sourcemodule EventsSet : sig ... end

Sourcetype events_set = EventsSet.t

Sourcemodule 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

Sourcetype presence_flag =

Sourcemodule 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