Frama-C API - Mt_cfg_types
Live threads/taken mutexes at a given point of execution
type context = {
started_threads : Mt_types.ThreadPresence.t;
locked_mutexes : Mt_types.MutexPresence.t;
}
module Context : sig ... end
type cfg_concur = {
concur_accesses : Mt_shared_vars_types.SetZoneAccess.t;
(*Var accesses at this statement
*)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 upated later using XXX
*)
}
module CfgConcur : sig ... end
module NodeValueState : sig ... end
type node = {
cfgn_id : int;
mutable cfgn_stack : Eva.Callstack.t;
mutable cfgn_var_access : cfg_concur;
mutable cfgn_kind : node_kind;
mutable cfgn_preds : node list;
mutable cfgn_value_state : node_value_state;
mutable cfgn_context : context;
}
and node_kind =
| NMT of Frama_c_kernel.Cil_types.stmt * Mt_types.events_set * node
| NInstr of Frama_c_kernel.Cil_types.stmt * node
| NCall of Frama_c_kernel.Cil_types.stmt * Frama_c_kernel.Kernel_function.t list * node list
| NWholeCall of Frama_c_kernel.Kernel_function.t * Frama_c_kernel.Cil_types.stmt list * Mt_types.events_set * node
| NWhile of Frama_c_kernel.Cil_types.stmt * node
| NIf of Frama_c_kernel.Cil_types.stmt * node * node
| NSwitch of Frama_c_kernel.Cil_types.stmt * Frama_c_kernel.Cil_types.exp * node list
| NJump of jump_type * node
| NStart of Frama_c_kernel.Kernel_function.t * node
| NEOP
| NDead
and jump_type =
| JBreak of Frama_c_kernel.Cil_types.stmt
| JContinue of Frama_c_kernel.Cil_types.stmt
| JGoto of Frama_c_kernel.Cil_types.stmt
| JReturn of Frama_c_kernel.Cil_types.stmt
| JExit of Frama_c_kernel.Cil_types.stmt
| JBlock of Frama_c_kernel.Cil_types.stmt
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 NodeIdAccess : Frama_c_kernel.Datatype.S with type t = Mt_types.rw * node * thread
module SetNodeIdAccess : sig ... end
module AccessesByZoneNode : Frama_c_kernel.Lmap_bitwise.Location_map_bitwise with type v = SetNodeIdAccess.t