Frama-C:
Plug-ins:
Libraries:

Frama-C API - Mt_cfg_types

type thread

Live threads/taken mutexes at a given point of execution

type context = {
  1. started_threads : Mt_types.ThreadPresence.t;
  2. locked_mutexes : Mt_types.MutexPresence.t;
}
module Context : sig ... end
type var_access_kind =
  1. | NotReallySharedVar
    (*

    Accesses that have been computed as possibly concurrent by the naive analysis, but that are in fact non-concurrent

    *)
  2. | SharedVarNonConcurrentAccess
    (*

    Accesses to a variable that is accessed concurrently, but this particular access is non-concurrent (the competing threads are not yet or no longer running)

    *)
  3. | ConcurrentAccess
    (*

    Really concurrent access

    *)
type cfg_concur = {
  1. concur_accesses : Mt_shared_vars_types.SetZoneAccess.t;
    (*

    Var accesses at this statement

    *)
  2. var_access_kind : var_access_kind;
    (*

    Does this node contains a concurrent access? We do not distinguish the information by zone accessed, as this only used to display the cfg, not to compute information. This information is *not* correctly computed when the cfg is created, and must be updated later using XXX

    *)
}
module CfgConcur : sig ... end
type node_value_state = {
  1. state_before : Mt_memory.Types.state;
  2. state_after : Mt_memory.Types.state;
}
module NodeValueState : sig ... end
type node = {
  1. cfgn_id : int;
  2. mutable cfgn_stack : Eva.Callstack.t;
  3. mutable cfgn_var_access : cfg_concur;
  4. mutable cfgn_kind : node_kind;
  5. mutable cfgn_preds : node list;
  6. mutable cfgn_value_state : node_value_state;
  7. mutable cfgn_context : context;
}
and cfg = node

Alias for nodes. A cfg is represented by its start node, but it is useful to distinguish between the two in signatures

module CfgNode : sig ... end

Definitions for multithread cfg

module SetNodeIdAccess : sig ... end