|
CBMC
|
#include "goto_rw.h"#include <util/arith_tools.h>#include <util/bitvector_expr.h>#include <util/byte_operators.h>#include <util/endianness_map.h>#include <util/expr_util.h>#include <util/namespace.h>#include <util/pointer_expr.h>#include <util/pointer_offset_size.h>#include <util/simplify_expr.h>#include <goto-programs/goto_functions.h>#include <langapi/language_util.h>#include <pointer-analysis/goto_program_dereference.h>#include <memory>
Include dependency graph for goto_rw.cpp:Go to the source code of this file.
Functions | |
| static void | goto_rw_assign (const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &rhs, rw_range_sett &rw_set) |
| static void | goto_rw_other (const irep_idt &function, goto_programt::const_targett target, const codet &code, rw_range_sett &rw_set) |
| static void | goto_rw (const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set) |
| void | goto_rw (const irep_idt &function, goto_programt::const_targett target, rw_range_sett &rw_set) |
| void | goto_rw (const irep_idt &function, 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 | ( | const goto_functionst & | goto_functions, |
| const irep_idt & | function, | ||
| rw_range_sett & | rw_set | ||
| ) |
Definition at line 944 of file goto_rw.cpp.
| void goto_rw | ( | const irep_idt & | function, |
| const goto_programt & | goto_program, | ||
| rw_range_sett & | rw_set | ||
| ) |
Definition at line 935 of file goto_rw.cpp.
|
static |
Definition at line 845 of file goto_rw.cpp.
| void goto_rw | ( | const irep_idt & | function, |
| goto_programt::const_targett | target, | ||
| rw_range_sett & | rw_set | ||
| ) |
Definition at line 867 of file goto_rw.cpp.
|
static |
Definition at line 778 of file goto_rw.cpp.
|
static |
Definition at line 790 of file goto_rw.cpp.