Frama-C API - Mt_cfg
val make_cfg : Mt_thread.thread_state -> Mt_cfg_types.cfgval remove_superfluous_nodes : keep:Mt_cfg_types.var_access_kind -> Mt_cfg_types.cfg -> Mt_cfg_types.cfgRemove nodes without multi-thread contents in the automata given by the start node, and returns the new start node. Nodes that are concurrent according to keep and
fgNode.must_be_in_cfg
.
val dot_fprint_graph : Stdlib.Format.formatter -> Mt_cfg_types.cfg -> (Frama_c_kernel.Cil_types.stmt -> string) -> unitMemory accesses in a cfg
val cfg_accesses : Mt_thread.thread -> Mt_cfg_types.cfg -> Mt_cfg_types.AccessesByZoneNode.mapDataflow on a cfg
val update_cfg_contexts : Mt_thread.analysis_state -> Mt_thread.thread_state -> unit