CBMC
|
Program Transformation. More...
#include "goto_program.h"
#include <util/expr_iterator.h>
#include <util/find_symbols.h>
#include <util/format_expr.h>
#include <util/format_type.h>
#include <util/invariant.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/symbol.h>
#include <util/validate.h>
#include <langapi/language_util.h>
#include "validate_code.h"
#include <iomanip>
#include <map>
Go to the source code of this file.
Functions | |
void | parse_lhs_read (const exprt &src, std::list< exprt > &dest) |
std::list< exprt > | expressions_read (const goto_programt::instructiont &instruction) |
std::list< exprt > | expressions_written (const goto_programt::instructiont &instruction) |
void | objects_read (const exprt &src, std::list< exprt > &dest) |
std::list< exprt > | objects_read (const goto_programt::instructiont &instruction) |
void | objects_written (const exprt &src, std::list< exprt > &dest) |
std::list< exprt > | objects_written (const goto_programt::instructiont &instruction) |
std::string | as_string (const class namespacet &ns, const irep_idt &function, const goto_programt::instructiont &i) |
std::ostream & | operator<< (std::ostream &out, goto_program_instruction_typet t) |
Outputs a string representation of a goto_program_instruction_typet More... | |
Program Transformation.
Definition in file goto_program.cpp.
std::string as_string | ( | const class namespacet & | ns, |
const irep_idt & | function, | ||
const goto_programt::instructiont & | i | ||
) |
Definition at line 515 of file goto_program.cpp.
std::list<exprt> expressions_read | ( | const goto_programt::instructiont & | instruction | ) |
Definition at line 362 of file goto_program.cpp.
std::list<exprt> expressions_written | ( | const goto_programt::instructiont & | instruction | ) |
Definition at line 411 of file goto_program.cpp.
Definition at line 451 of file goto_program.cpp.
std::list<exprt> objects_read | ( | const goto_programt::instructiont & | instruction | ) |
Definition at line 475 of file goto_program.cpp.
Definition at line 488 of file goto_program.cpp.
std::list<exprt> objects_written | ( | const goto_programt::instructiont & | instruction | ) |
Definition at line 502 of file goto_program.cpp.
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.
Definition at line 337 of file goto_program.cpp.