Frama-C:
Plug-ins:
Libraries:

Frama-C API - Mt_shared_vars_types

module SetZoneAccess : sig ... end

Sets of zone accesses (used in cfg nodes)

Type of a full access operation to a variable : read or write, statement at which the access takes place, thread that does the operation

module SetStmtIdAccess : sig ... end

More than one full access to a variable. The boolean indicates whether all accesses are dummy ones, ie present just to ensure convergence of the algorithm

module AccessesByZone : sig ... end

Maps from zones to variables accesses

type access_kind =
  1. | AccessRead
  2. | AccessWrite

Kind of access: read or write.

type protection =
  1. | Unprotected
  2. | MaybeProtected of Mutex.t
  3. | Protected of Mutex.t

Protection of an access: unprotected, maybe protected by a mutex, fully protected by a mutex.