Module Mthread.Mt_cfgSource

Sourceval 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

.

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

Memory accesses in a cfg

Dataflow on a cfg

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