natural_loops.h File Reference

#include <stack>
#include <iosfwd>
#include <set>
#include <goto-programs/goto_model.h>
#include "cfg_dominators.h"
#include "loop_analysis.h"

Include dependency graph for natural_loops.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	natural_loops_templatet< P, T >
	Main driver for working out if a class (normally goto_programt) has any natural loops. More...
class	natural_loopst
	A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett> More...

Typedefs
typedef natural_loops_templatet< goto_programt, goto_programt::targett >	natural_loops_mutablet

Functions
void	show_natural_loops (const goto_modelt &goto_model, std::ostream &out)

Detailed Description

Compute natural loops in a goto_function.

A natural loop is when the nodes and edges of a graph make one self-encapsulating circle with no incoming edges from external nodes. For example A -> B -> C -> D -> A is a natural loop, but if B has an incoming edge from X, then it isn't a natural loop, because X is an external node. Outgoing edges don't affect the natural-ness of a loop.

/ref cfg_dominators_templatet provides the dominator analysis used to determine if a nodes children can only be reached through itself and is thus part of a natural loop.

Definition in file natural_loops.h.

Typedef Documentation

natural_loops_mutablet

typedef natural_loops_templatet<goto_programt, goto_programt::targett> natural_loops_mutablet

Definition at line 90 of file natural_loops.h.

Function Documentation

show_natural_loops()

void show_natural_loops ( const goto_modelt &  goto_model, std::ostream &  out  )

inline

Definition at line 92 of file natural_loops.h.