goto_program.h File Reference

#include "goto_instruction_code.h"
#include <iosfwd>
#include <set>
#include <limits>
#include <string>
#include <util/deprecate.h>
#include <util/invariant.h>
#include <util/namespace.h>
#include <util/source_location.h>

Include dependency graph for goto_program.h:

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,   SET_RETURN_VALUE = 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)
template<typename GotoFunctionT , typename PredicateT , typename HandlerT >
void	for_each_instruction_if (GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)
template<typename GotoFunctionT , typename HandlerT >
void	for_each_instruction (GotoFunctionT &&goto_function, HandlerT handler)
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 irep_idt &function, 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 1229 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 1234 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
SET_RETURN_VALUE
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 irep_idt &	function,
		const goto_programt::instructiont &
	)

expressions_read()

std::list<exprt> expressions_read

(

const goto_programt::instructiont &

)

Definition at line 360 of file goto_program.cpp.

expressions_written()

std::list<exprt> expressions_written

(

const goto_programt::instructiont &

)

Definition at line 409 of file goto_program.cpp.

for_each_instruction()

template<typename GotoFunctionT , typename HandlerT >

void for_each_instruction	(	GotoFunctionT &&	goto_function,
		HandlerT	handler
	)

Definition at line 1222 of file goto_program.h.

for_each_instruction_if()

template<typename GotoFunctionT , typename PredicateT , typename HandlerT >

void for_each_instruction_if	(	GotoFunctionT &&	goto_function,
		PredicateT	predicate,
		HandlerT	handler
	)

Definition at line 1206 of file goto_program.h.

objects_read()

std::list<exprt> objects_read

(

const goto_programt::instructiont &

)

Definition at line 473 of file goto_program.cpp.

objects_written()

std::list<exprt> objects_written

(

const goto_programt::instructiont &

)

Definition at line 500 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 1239 of file goto_program.h.

operator<() [2/2]

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

inline

Definition at line 1246 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 1170 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 1174 of file goto_program.h.