cprover
|
Perform Memory-mapped I/O instrumentation. More...
#include "mm_io.h"
#include <util/pointer_predicates.h>
#include <util/pointer_offset_size.h>
#include <util/replace_expr.h>
#include "remove_returns.h"
Go to the source code of this file.
Functions | |
void | collect_deref_expr (const exprt &src, std::set< dereference_exprt > &dest) |
void | mm_io (const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns) |
void | mm_io (const symbol_tablet &symbol_table, goto_functionst &goto_functions) |
void | mm_io (goto_modelt &model) |
Perform Memory-mapped I/O instrumentation.
Definition in file mm_io.cpp.
void collect_deref_expr | ( | const exprt & | src, |
std::set< dereference_exprt > & | dest | ||
) |
Definition at line 22 of file mm_io.cpp.
References irept::id(), exprt::operands(), and to_dereference_expr().
Referenced by mm_io().
void mm_io | ( | const exprt & | mm_io_r, |
const exprt & | mm_io_w, | ||
goto_functionst::goto_functiont & | goto_function, | ||
const namespacet & | ns | ||
) |
Definition at line 33 of file mm_io.cpp.
References code_function_callt::arguments(), collect_deref_expr(), code_function_callt::function(), symbol_exprt::get_identifier(), id2string(), integer_address(), irept::is_not_nil(), code_typet::parameters(), dereference_exprt::pointer(), replace_expr(), code_typet::return_type(), RETURN_VALUE_SUFFIX, size_of_expr(), exprt::source_location(), to_code_assign(), to_code_type(), to_dereference_expr(), to_symbol_expr(), and exprt::type().
Referenced by mm_io(), jdiff_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), and cbmc_parse_optionst::process_goto_program().
void mm_io | ( | const symbol_tablet & | symbol_table, |
goto_functionst & | goto_functions | ||
) |
Definition at line 111 of file mm_io.cpp.
References CPROVER_PREFIX, goto_functionst::function_map, symbol_table_baset::lookup(), mm_io(), and symbolt::symbol_expr().
void mm_io | ( | goto_modelt & | model | ) |
Definition at line 133 of file mm_io.cpp.
References goto_modelt::goto_functions, mm_io(), and goto_modelt::symbol_table.