cprover
|
#include "goto_rw.h"
#include <limits>
#include <algorithm>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/pointer_offset_size.h>
#include <util/byte_operators.h>
#include <util/endianness_map.h>
#include <util/arith_tools.h>
#include <util/simplify_expr.h>
#include <goto-programs/goto_functions.h>
#include <pointer-analysis/goto_program_dereference.h>
Go to the source code of this file.
Functions | |
void | goto_rw (goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set) |
void | goto_rw (goto_programt::const_targett target, const code_function_callt &function_call, rw_range_sett &rw_set) |
void | goto_rw (goto_programt::const_targett target, rw_range_sett &rw_set) |
void | goto_rw (const goto_programt &goto_program, rw_range_sett &rw_set) |
void | goto_rw (const goto_functionst &goto_functions, const irep_idt &function, rw_range_sett &rw_set) |
void goto_rw | ( | goto_programt::const_targett | target, |
const code_assignt & | assign, | ||
rw_range_sett & | rw_set | ||
) |
Definition at line 678 of file goto_rw.cpp.
References rw_range_sett::get_objects_rec(), code_assignt::lhs(), rw_range_sett::LHS_W, rw_range_sett::READ, and code_assignt::rhs().
Referenced by dep_graph_domaint::data_dependencies(), goto_rw(), rd_range_domaint::transform(), and rd_range_domaint::transform_assign().
void goto_rw | ( | goto_programt::const_targett | target, |
const code_function_callt & | function_call, | ||
rw_range_sett & | rw_set | ||
) |
Definition at line 686 of file goto_rw.cpp.
References code_function_callt::arguments(), forall_expr, code_function_callt::function(), rw_range_sett::get_objects_rec(), irept::is_not_nil(), code_function_callt::lhs(), rw_range_sett::LHS_W, and rw_range_sett::READ.
void goto_rw | ( | goto_programt::const_targett | target, |
rw_range_sett & | rw_set | ||
) |
Definition at line 705 of file goto_rw.cpp.
References ASSERT, ASSIGN, ASSUME, ATOMIC_BEGIN, ATOMIC_END, CATCH, DEAD, DECL, END_FUNCTION, END_THREAD, forall_expr, FUNCTION_CALL, rw_range_sett::get_objects_rec(), GOTO, goto_rw(), code_returnt::has_return_value(), rw_range_sett::LHS_W, LOCATION, NO_INSTRUCTION_TYPE, OTHER, rw_range_sett::READ, RETURN, code_returnt::return_value(), SKIP, START_THREAD, code_declt::symbol(), code_deadt::symbol(), THROW, to_code_assign(), to_code_dead(), to_code_decl(), to_code_function_call(), to_code_return(), and exprt::type().
void goto_rw | ( | const goto_programt & | goto_program, |
rw_range_sett & | rw_set | ||
) |
Definition at line 782 of file goto_rw.cpp.
References forall_goto_program_instructions, and goto_rw().
void goto_rw | ( | const goto_functionst & | goto_functions, |
const irep_idt & | function, | ||
rw_range_sett & | rw_set | ||
) |
Definition at line 788 of file goto_rw.cpp.
References goto_functions_templatet< bodyT >::function_map, and goto_rw().