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

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_than >	instructions
	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, edget >	edgest

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	(	const goto_programt::targett &	head,
		const goto_programt::targett &	latch,
		const loop_templatet< goto_programt::targett, goto_programt::target_less_than > &	instructions
	)

goto_programt::targett dfcc_loop_nesting_graph_nodet::head

Loop head instruction.

Definition at line 37 of file dfcc_loop_nesting_graph.h.

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.

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

/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp