Mt_cfg (frama-c-eva.Mthread.Mt

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 Mt_cfg_types.CfgNode.must_be_in_cfg.

val dot_fprint_graph : 
  Stdlib.Format.formatter ->
  Mt_cfg_types.cfg ->
  (Frama_c_kernel.Cil_types.stmt -> string) ->
  unit

Memory accesses in a cfg

val cfg_accesses : 
  Mt_thread.thread ->
  Mt_cfg_types.cfg ->
  Mt_cfg_types.AccessesByZoneNode.map

Dataflow on a cfg

val update_cfg_contexts : 
  Mt_thread.analysis_state ->
  Mt_thread.thread_state ->
  unit