goto_program.h File Reference

Concrete Goto Program. More...

#include <iosfwd>
#include <set>
#include <limits>
#include <sstream>
#include <string>
#include <util/invariant.h>
#include <util/namespace.h>
#include <util/source_location.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/symbol_table.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 the GOTO intermediate representation of one function. More...
class	goto_programt::instructiont
	This class represents an instruction in the GOTO intermediate representation. More...
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, START_THREAD = 6, END_THREAD = 7,   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, INCOMPLETE_GOTO = 19 }
	The type of an instruction in a GOTO program. More...

Functions
std::ostream &	operator<< (std::ostream &, goto_program_instruction_typet)
	Outputs a string representation of a goto_program_instruction_typet More...
bool	order_const_target (const goto_programt::const_targett i1, const goto_programt::const_targett i2)
bool	operator< (const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
bool	operator< (const goto_programt::targett &i1, const goto_programt::targett &i2)
std::list< exprt >	objects_read (const goto_programt::instructiont &)
std::list< exprt >	objects_written (const goto_programt::instructiont &)
std::list< exprt >	expressions_read (const goto_programt::instructiont &)
std::list< exprt >	expressions_written (const goto_programt::instructiont &)
std::string	as_string (const namespacet &ns, const goto_programt::instructiont &)

Detailed Description

Concrete Goto Program.

Definition in file goto_program.h.

Macro Definition Documentation

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++)

Definition at line 804 of file goto_program.h.

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++)

Definition at line 809 of file goto_program.h.

Enumeration Type Documentation

goto_program_instruction_typet

enum goto_program_instruction_typet

The type of an instruction in a GOTO program.

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

Definition at line 31 of file goto_program.h.

Function Documentation

as_string()

std::string as_string	(	const namespacet &	ns,
		const goto_programt::instructiont &
	)

expressions_read()

std::list<exprt> expressions_read

(

const goto_programt::instructiont &

)

Definition at line 266 of file goto_program.cpp.

expressions_written()

std::list<exprt> expressions_written

(

const goto_programt::instructiont &

)

Definition at line 311 of file goto_program.cpp.

objects_read()

std::list<exprt> objects_read

(

const goto_programt::instructiont &

)

Definition at line 363 of file goto_program.cpp.

objects_written()

std::list<exprt> objects_written

(

const goto_programt::instructiont &

)

Definition at line 390 of file goto_program.cpp.

operator<() [1/2]

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

inline

Definition at line 814 of file goto_program.h.

operator<() [2/2]

bool operator< ( const goto_programt::targett &  i1, const goto_programt::targett &  i2  )

inline

Definition at line 821 of file goto_program.h.

operator<<()

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

Outputs a string representation of a goto_program_instruction_typet

Definition at line 864 of file goto_program.cpp.

order_const_target()

bool order_const_target ( const goto_programt::const_targett  i1, const goto_programt::const_targett  i2  )

inline

Definition at line 773 of file goto_program.h.