cprover
|
Program Transformation. More...
#include "goto_program.h"
#include <ostream>
#include <iomanip>
#include <util/std_expr.h>
#include <langapi/language_util.h>
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 goto_programt::instructiont &i) |
Program Transformation.
Definition in file goto_program.cpp.
std::string as_string | ( | const class namespacet & | ns, |
const goto_programt::instructiont & | i | ||
) |
Definition at line 398 of file goto_program.cpp.
References ASSERT, ASSIGN, ASSUME, ATOMIC_BEGIN, ATOMIC_END, CATCH, goto_programt::instructiont::code, comment(), DEAD, DECL, END_FUNCTION, END_THREAD, from_expr(), goto_programt::instructiont::function, FUNCTION_CALL, source_locationt::get_comment(), GOTO, goto_programt::instructiont::guard, id2string(), goto_programt::instructiont::is_assume(), exprt::is_true(), LOCATION, NO_INSTRUCTION_TYPE, OTHER, RETURN, SKIP, goto_programt::instructiont::source_location, START_THREAD, goto_programt::instructiont::targets, THROW, to_string(), and goto_programt::instructiont::type.
Referenced by id2string(), name2string(), and show_state_header().
std::list<exprt> expressions_read | ( | const goto_programt::instructiont & | instruction | ) |
Definition at line 261 of file goto_program.cpp.
References code_function_callt::arguments(), ASSERT, ASSIGN, ASSUME, goto_programt::instructiont::code, forall_expr, FUNCTION_CALL, GOTO, goto_programt::instructiont::guard, irept::is_not_nil(), code_assignt::lhs(), code_function_callt::lhs(), parse_lhs_read(), RETURN, code_returnt::return_value(), code_assignt::rhs(), to_code_assign(), to_code_function_call(), to_code_return(), and goto_programt::instructiont::type.
Referenced by objects_read(), and uninitialized_domaint::transform().
std::list<exprt> expressions_written | ( | const goto_programt::instructiont & | instruction | ) |
Definition at line 306 of file goto_program.cpp.
References ASSIGN, goto_programt::instructiont::code, FUNCTION_CALL, irept::is_not_nil(), code_assignt::lhs(), code_function_callt::lhs(), to_code_assign(), to_code_function_call(), and goto_programt::instructiont::type.
Referenced by objects_written(), and uninitialized_domaint::transform().
Definition at line 334 of file goto_program.cpp.
References forall_operands, irept::id(), exprt::op0(), and exprt::operands().
Referenced by uninitializedt::add_assertions(), uninitializedt::get_tracking(), and objects_read().
std::list<exprt> objects_read | ( | const goto_programt::instructiont & | instruction | ) |
Definition at line 358 of file goto_program.cpp.
References expressions_read(), and objects_read().
Definition at line 371 of file goto_program.cpp.
References irept::id(), exprt::op1(), exprt::op2(), and exprt::operands().
Referenced by uninitializedt::add_assertions(), and objects_written().
std::list<exprt> objects_written | ( | const goto_programt::instructiont & | instruction | ) |
Definition at line 385 of file goto_program.cpp.
References expressions_written(), and objects_written().
Definition at line 234 of file goto_program.cpp.
References irept::id(), exprt::op0(), exprt::op1(), exprt::op2(), and exprt::operands().
Referenced by expressions_read().