cprover
|
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>
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) |
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) |
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< 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 &) |
Concrete Goto Program.
Definition in file goto_program.h.
#define forall_goto_program_instructions | ( | it, | |
program | |||
) |
Definition at line 1196 of file goto_program.h.
#define Forall_goto_program_instructions | ( | it, | |
program | |||
) |
Definition at line 1201 of file goto_program.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 | |
INCOMPLETE_GOTO |
Definition at line 31 of file goto_program.h.
std::string as_string | ( | const namespacet & | ns, |
const irep_idt & | function, | ||
const goto_programt::instructiont & | |||
) |
std::list<exprt> expressions_read | ( | const goto_programt::instructiont & | ) |
Definition at line 273 of file goto_program.cpp.
std::list<exprt> expressions_written | ( | const goto_programt::instructiont & | ) |
Definition at line 329 of file goto_program.cpp.
void for_each_instruction | ( | GotoFunctionT && | goto_function, |
HandlerT | handler | ||
) |
Definition at line 1189 of file goto_program.h.
void for_each_instruction_if | ( | GotoFunctionT && | goto_function, |
PredicateT | predicate, | ||
HandlerT | handler | ||
) |
Definition at line 1173 of file goto_program.h.
std::list<exprt> objects_read | ( | const goto_programt::instructiont & | ) |
Definition at line 397 of file goto_program.cpp.
std::list<exprt> objects_written | ( | const goto_programt::instructiont & | ) |
Definition at line 424 of file goto_program.cpp.
|
inline |
Definition at line 1206 of file goto_program.h.
|
inline |
Definition at line 1213 of file goto_program.h.
std::ostream& operator<< | ( | std::ostream & | , |
goto_program_instruction_typet | |||
) |
Outputs a string representation of a goto_program_instruction_typet
Definition at line 1115 of file goto_program.cpp.
|
inline |
Definition at line 1141 of file goto_program.h.