CBMC
|
A graph node that stores information about a natural loop. More...
#include <dfcc_loop_nesting_graph.h>
Public Member Functions | |
dfcc_loop_nesting_graph_nodet (const goto_programt::targett &head, const goto_programt::targett &latch, const loop_templatet< goto_programt::targett, goto_programt::target_less_than > &instructions) | |
Public Member Functions inherited from graph_nodet< empty_edget > | |
void | add_in (node_indext n) |
void | add_out (node_indext n) |
void | erase_in (node_indext n) |
void | erase_out (node_indext n) |
std::string | pretty (const node_indext &idx) const |
virtual | ~graph_nodet () |
Public Attributes | |
goto_programt::targett | head |
Loop head instruction. More... | |
goto_programt::targett | latch |
Loop latch instruction. More... | |
loop_templatet< goto_programt::targett, goto_programt::target_less_than > | instructions |
Set of loop instructions. More... | |
Public Attributes inherited from graph_nodet< empty_edget > | |
edgest | in |
edgest | out |
Additional Inherited Members | |
Public Types inherited from graph_nodet< empty_edget > | |
typedef std::size_t | node_indext |
typedef empty_edget | edget |
typedef std::map< node_indext, edget > | edgest |
A graph node that stores information about a natural loop.
Definition at line 26 of file dfcc_loop_nesting_graph.h.
dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet | ( | const goto_programt::targett & | head, |
const goto_programt::targett & | latch, | ||
const loop_templatet< goto_programt::targett, goto_programt::target_less_than > & | instructions | ||
) |
Definition at line 17 of file dfcc_loop_nesting_graph.cpp.
goto_programt::targett dfcc_loop_nesting_graph_nodet::head |
Loop head instruction.
Definition at line 37 of file dfcc_loop_nesting_graph.h.
loop_templatet<goto_programt::targett, goto_programt::target_less_than> dfcc_loop_nesting_graph_nodet::instructions |
Set of loop instructions.
Definition at line 44 of file dfcc_loop_nesting_graph.h.
goto_programt::targett dfcc_loop_nesting_graph_nodet::latch |
Loop latch instruction.
Definition at line 40 of file dfcc_loop_nesting_graph.h.