goto_program.h File Reference

Concrete Goto Program. More...

#include <util/invariant.h>
#include <util/source_location.h>
#include "goto_instruction_code.h"
#include <limits>
#include <list>
#include <set>
#include <string>

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	goto_programt::instructiont::target_less_than
	A total order over targett and const_targett. 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
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)
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 1228 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 1233 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 30 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 &

instruction

)

Definition at line 362 of file goto_program.cpp.

expressions_written()

std::list< exprt > expressions_written

(

const goto_programt::instructiont &

instruction

)

Definition at line 411 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 1221 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 1205 of file goto_program.h.

objects_read()

std::list< exprt > objects_read

(

const goto_programt::instructiont &

instruction

)

Definition at line 475 of file goto_program.cpp.

objects_written()

std::list< exprt > objects_written

(

const goto_programt::instructiont &

instruction

)

Definition at line 502 of file goto_program.cpp.

operator<<()

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

Outputs a string representation of a goto_program_instruction_typet

Definition at line 1172 of file goto_program.cpp.