CBMC
dfcc_loop_nesting_graph_nodet Struct Reference

A graph node that stores information about a natural loop. More...

#include <dfcc_loop_nesting_graph.h>

+ Inheritance diagram for dfcc_loop_nesting_graph_nodet:
+ Collaboration diagram for dfcc_loop_nesting_graph_nodet:

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_thaninstructions
 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, edgetedgest
 

Detailed Description

A graph node that stores information about a natural loop.

Definition at line 26 of file dfcc_loop_nesting_graph.h.

Constructor & Destructor Documentation

◆ dfcc_loop_nesting_graph_nodet()

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.

Member Data Documentation

◆ head

goto_programt::targett dfcc_loop_nesting_graph_nodet::head

Loop head instruction.

Definition at line 37 of file dfcc_loop_nesting_graph.h.

◆ instructions

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.

◆ latch

goto_programt::targett dfcc_loop_nesting_graph_nodet::latch

Loop latch instruction.

Definition at line 40 of file dfcc_loop_nesting_graph.h.


The documentation for this struct was generated from the following files: