lexical_loops.h File Reference

Compute lexical loops in a goto_function. More...

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

Include dependency graph for lexical_loops.h:

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

Go to the source code of this file.

Classes
class	lexical_loops_templatet< P, T, C >
	Main driver for working out if a class (normally goto_programt) has any lexical loops. More...

Typedefs
typedef lexical_loops_templatet< const goto_programt, goto_programt::const_targett, goto_programt::target_less_than >	lexical_loopst

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

Detailed Description

Compute lexical loops in a goto_function.

A lexical loop is a block of GOTO program instructions with a single entry edge at the top and a single backedge leading from bottom to top, where "top" and "bottom" refer to program order. The loop may have holes: instructions which sit in between the top and bottom in program order, but which can't reach the loop backedge. Lexical loops are a subset of the natural loops, which are cheaper to compute and include most natural loops generated from typical C code.

Example of a lexical loop:

1: x = x + 1
   IF x < 5 GOTO 2
   done = true (*)
   GOTO 3 (*)
2: i = i + 1
   IF i < 10 GOTO 1
3: RETURN x

Assuming there are no GOTOs outside the loop targeting label 2, this is a lexical loop because the header (1) is the only entry point and the only back-edge is the final conditional GOTO. The instructions marked with a (*) are not in the loop; they are on a path that always leaves the loop (once the IF x < 5 test is failed we are certainly leaving the loop).

Definition in file lexical_loops.h.

Typedef Documentation

lexical_loopst

typedef lexical_loops_templatet< const goto_programt, goto_programt::const_targett, goto_programt::target_less_than> lexical_loopst

Definition at line 109 of file lexical_loops.h.

Function Documentation

show_lexical_loops()

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

inline

Definition at line 193 of file lexical_loops.h.