Mthread.Mt_cfg
val make_cfg : Mt_thread.thread_state -> Mt_cfg_types.cfg
val remove_superfluous_nodes :
keep:Mt_cfg_types.var_access_kind ->
Mt_cfg_types.cfg ->
Mt_cfg_types.cfg
Remove 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) ->
unit
val cfg_accesses :
Mt_thread.thread ->
Mt_cfg_types.cfg ->
Mt_cfg_types.AccessesByZoneNode.map
val update_cfg_contexts :
Mt_thread.analysis_state ->
Mt_thread.thread_state ->
unit