cprover
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< exprtobjects_read (const goto_programt::instructiont &)
 
std::list< exprtobjects_written (const goto_programt::instructiont &)
 
std::list< exprtexpressions_read (const goto_programt::instructiont &)
 
std::list< exprtexpressions_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

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 264 of file goto_program.cpp.

◆ expressions_written()

std::list<exprt> expressions_written ( const goto_programt::instructiont )

Definition at line 309 of file goto_program.cpp.

◆ objects_read()

std::list<exprt> objects_read ( const goto_programt::instructiont )

Definition at line 361 of file goto_program.cpp.

◆ objects_written()

std::list<exprt> objects_written ( const goto_programt::instructiont )

Definition at line 388 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 760 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.