cprover
|
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>
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) |
Goto Program Template.
Definition in file goto_program_template.h.
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.
std::ostream& operator<< | ( | std::ostream & | , |
goto_program_instruction_typet | |||
) |
Definition at line 16 of file goto_program_template.cpp.
References ASSERT, ASSIGN, ASSUME, ATOMIC_BEGIN, ATOMIC_END, DEAD, DECL, END_FUNCTION, END_THREAD, FUNCTION_CALL, GOTO, LOCATION, NO_INSTRUCTION_TYPE, OTHER, RETURN, SKIP, and START_THREAD.
|
inline |
Definition at line 778 of file goto_program_template.h.