Frama-C:
Plug-ins:
Libraries:

Frama-C API - CfgNode

Definitions for multithread cfg

include Frama_c_kernel.Datatype.S_with_collections with type t = node
include Frama_c_kernel.Datatype.S with type t = node
include Frama_c_kernel.Datatype.S_no_copy with type t = node
include Frama_c_kernel.Datatype.Ty with type t = node
type t = node
val datatype_name : string

Unique name of the datatype.

val datatype_descr : t Frama_c_kernel.Descr.t

Datatype descriptor.

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val mem_project : (Frama_c_kernel.Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

module Set : Frama_c_kernel.Datatype.Set with type elt = t
module Map : Frama_c_kernel.Datatype.Map with type key = t
val dead : t

Node with cfgn_kind set to NDead. We always reuse this node, as it is never displayed (and it has no successor, thus causing no problem in the dataflow analysis)

val new_node : Eva.Callstack.t -> t

Fresh node generator. The initial content of the node is unspecified. The nodes are guaranteed to be different from dummy and dead

val node_kind_stmt : node_kind -> Frama_c_kernel.Cil_types.stmt list
val node_stmt : t -> Frama_c_kernel.Cil_types.stmt list
val node_first_loc : t -> Frama_c_kernel.Filepath.position option
val node_kind_succs : node_kind -> t list
val node_succs : t -> t list
val has_concur_accesses : t -> bool

Is there a variable access at this node

val must_be_in_cfg : keep:var_access_kind -> t -> bool

Should we keep a node in the cfg considering the concurrent accesses it performs. We keep all accesses with a level equal or above keep. Note that in the current cfg construction model, nodes are labelled with ConcurrentAccess or SharedVarNonConcurrentAccess very late. Thus, must_be_in_cfg must not be called with keep not equal to NotReallySharedVar before that.

val pretty_kinds_node_list : node list Frama_c_kernel.Pretty_utils.formatter
val iter : ?f_before:(t -> unit) -> ?f_after:(t -> unit) -> t -> unit

Iteration on all the nodes of an automata reachable from the node passed as argument. The order of visit is unspecified. Each node is visited exactly once. The function f_before is called before the children of the node are visited (except in case of cycles), while f_after is called only after all the children have been visited

val iter_with_prevs : ?f_before:(prevs:t list -> t -> unit) -> ?f_after:(prevs:t list -> t -> unit) -> t -> unit

Same iterator as above, except that the function also receives as argument the path between the initial node and the visited node (starting from the visited node)