cprover
goto_program_template.h File Reference

Goto Program Template. More...

#include <cassert>
#include <iosfwd>
#include <set>
#include <limits>
#include <sstream>
#include <string>
#include <util/namespace.h>
#include <util/symbol_table.h>
#include <util/source_location.h>
#include <util/std_expr.h>
#include <langapi/language_util.h>
#include <iomanip>
Include dependency graph for goto_program_template.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  goto_program_templatet< codeT, guardT >
 A generic container class for the GOTO intermediate representation of one function. More...
 
class  goto_program_templatet< codeT, guardT >::instructiont
 This class represents an instruction in the GOTO intermediate representation. More...
 
struct  const_target_hash_templatet< codeT, guardT >
 

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
}
 The type of an instruction in a GOTO program. More...
 

Functions

std::ostream & operator<< (std::ostream &, goto_program_instruction_typet)
 
template<class codeT , class guardT >
bool order_const_target (const typename goto_program_templatet< codeT, guardT >::const_targett i1, const typename goto_program_templatet< codeT, guardT >::const_targett i2)
 

Detailed Description

Goto Program Template.

Definition in file goto_program_template.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 

Definition at line 28 of file goto_program_template.h.

Function Documentation

◆ operator<<()

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

◆ order_const_target()

template<class codeT , class guardT >
bool order_const_target ( const typename goto_program_templatet< codeT, guardT >::const_targett  i1,
const typename goto_program_templatet< codeT, guardT >::const_targett  i2 
)
inline

Definition at line 778 of file goto_program_template.h.