CBMC
|
Control Flow Graph. More...
#include <util/dense_integer_map.h>
#include <util/graph.h>
#include <util/std_expr.h>
#include "goto_functions.h"
Go to the source code of this file.
Classes | |
class | empty_cfg_nodet |
struct | cfg_base_nodet< T, I > |
class | cfg_instruction_to_dense_integert< T > |
Functor to convert cfg nodes into dense integers, used by cfg_baset. More... | |
class | cfg_instruction_to_dense_integert< goto_programt::const_targett > |
GOTO-instruction to location number functor. More... | |
class | cfg_baset< T, P, I > |
A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO program. More... | |
class | cfg_baset< T, P, I >::entry_mapt |
class | concurrent_cfg_baset< T, P, I > |
class | procedure_local_cfg_baset< T, P, I > |
class | procedure_local_concurrent_cfg_baset< T, P, I > |
Control Flow Graph.
Definition in file cfg.h.