24 std::set<dereference_exprt> &dest)
26 if(src.
id()==ID_dereference)
29 for(
const auto & op : src.
operands())
39 for(goto_programt::instructionst::iterator it=
40 goto_function.body.instructions.begin();
41 it!=goto_function.body.instructions.end();
44 std::set<dereference_exprt> deref_expr_w, deref_expr_r;
53 if(deref_expr_r.size()==1)
74 goto_function.body.insert_before_swap(it);
75 it->make_function_call(fc);
77 it->function=
function;
84 if(a.lhs().id()==ID_dereference)
100 goto_function.body.insert_before_swap(it);
101 it->make_function_call(fc);
103 it->function=
function;
128 mm_io(mm_io_r, mm_io_w, f.second, ns);
The type of an expression.
exprt size_of_expr(const typet &type, const namespacet &ns)
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
const std::string & id2string(const irep_idt &d)
void collect_deref_expr(const exprt &src, std::set< dereference_exprt > &dest)
const irep_idt & get_identifier() const
The trinary if-then-else operator.
symbol_tablet symbol_table
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
const code_assignt & to_code_assign(const codet &code)
Perform Memory-mapped I/O instrumentation.
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Operator to dereference a pointer.
exprt integer_address(const exprt &pointer)
goto_function_templatet< goto_programt > goto_functiont
function_mapt function_map
Various predicates over pointers in programs.
Base class for all expressions.
const parameterst & parameters() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const source_locationt & source_location() const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
bool has_symbol(const irep_idt &name) const
Expression to hold a symbol (variable)
#define RETURN_VALUE_SUFFIX
void mm_io(const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
goto_functionst goto_functions
const typet & return_type() const