cprover
Loading...
Searching...
No Matches
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.
goto_programt::targett latch
 Loop latch instruction.
loop_templatet< goto_programt::targett, goto_programt::target_less_thaninstructions
 Set of loop instructions.
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: