goto_program.h File Reference

#include <cassert>
#include <ostream>
#include <set>
#include <vector>
#include <irep2/irep2_utils.h>
#include <util/irep/location.h>
#include <util/symtab/namespace.h>
#include <util/irep/std_code.h>

Include dependency graph for goto_program.h:

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

Go to the source code of this file.

Classes
class	goto_programt
	A generic container class for a control flow graph for one function, in the form of a goto-program. More...
class	goto_programt::instructiont
	Container for an instruction of the goto-program. More...
struct	goto_programt::instructiont::loop_contract_datat
struct	const_target_hash
struct	pointee_address_equalt
	Functor to check whether iterators from different collections point at the same object. More...

Macros
#define	forall_goto_program_instructions(it, program)
#define	Forall_goto_program_instructions(it, program)

Enumerations
enum	goto_program_instruction_typet {   NO_INSTRUCTION_TYPE = 0 , GOTO = 1 , ASSUME = 2 , ASSERT = 3 ,   OTHER = 4 , SKIP = 5 , LOCATION = 8 , END_FUNCTION = 9 ,   ATOMIC_BEGIN = 10 , ATOMIC_END = 11 , RETURN = 12 , ASSIGN = 13 ,   DECL = 14 , DEAD = 15 , FUNCTION_CALL = 16 , THROW = 17 ,   CATCH = 18 , LOOP_INVARIANT = 21 }

Functions
std::ostream &	operator<< (std::ostream &, goto_program_instruction_typet)
bool	operator< (const goto_programt::const_targett i1, const goto_programt::const_targett i2)

Macro Definition Documentation

Forall_goto_program_instructions

#define Forall_goto_program_instructions	(		it,
			program )

Value:

  for (goto_programt::instructionst::iterator it =                             \
         (program).instructions.begin();                                       \
       it != (program).instructions.end();                                     \
       it++)

forall_goto_program_instructions

#define forall_goto_program_instructions	(		it,
			program )

Value:

  for (goto_programt::instructionst::const_iterator it =                       \
         (program).instructions.begin();                                       \
       it != (program).instructions.end();                                     \
       it++)

Enumeration Type Documentation

goto_program_instruction_typet

enum goto_program_instruction_typet

Enumerator
NO_INSTRUCTION_TYPE
GOTO
ASSUME
ASSERT
OTHER
SKIP
LOCATION
END_FUNCTION
ATOMIC_BEGIN
ATOMIC_END
RETURN
ASSIGN
DECL
DEAD
FUNCTION_CALL
THROW
CATCH
LOOP_INVARIANT

Function Documentation

operator<()

bool operator<	(	const goto_programt::const_targett	i1,
		const goto_programt::const_targett	i2 )

operator<<()

std::ostream & operator<<	(	std::ostream &	out,
		goto_program_instruction_typet	t )