Concrete Goto Program. More...

#include <util/invariant.h>
#include <util/source_location.h>
#include "goto_instruction_code.h"
#include <iosfwd>
#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` More...

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 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 & 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 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 & 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.

Classes

Macros

Enumerations

Functions