Go to the documentation of this file.
28 std::set<dereference_exprt> &dest)
31 if(e.
id() == ID_dereference)
42 for(goto_programt::instructionst::iterator it=
43 goto_function.body.instructions.begin();
44 it!=goto_function.body.instructions.end();
47 std::set<dereference_exprt> deref_expr_w, deref_expr_r;
51 auto &a_lhs = it->assign_lhs();
52 auto &a_rhs = it->assign_rhs_nonconst();
57 if(deref_expr_r.size()==1)
76 goto_function.body.insert_before_swap(it);
84 if(a_lhs.id() == ID_dereference)
99 goto_function.body.insert_before_swap(it);
118 auto maybe_symbol=symbol_table.
lookup(id_r);
120 mm_io_r=maybe_symbol->symbol_expr();
122 maybe_symbol=symbol_table.
lookup(id_w);
127 mm_io(mm_io_r, mm_io_w, f.second, ns);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
void mm_io(const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Operator to dereference a pointer.
The trinary if-then-else operator.
Various predicates over pointers in programs.
Base class for all expressions.
function_mapt function_map
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
typet & type()
Return the type of the expression.
codet representation of a function call statement.
void collect_deref_expr(const exprt &src, std::set< dereference_exprt > &dest)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Perform Memory-mapped I/O instrumentation.
const irep_idt & get_identifier() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
API to expression classes for Pointers.
exprt integer_address(const exprt &pointer)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const parameterst & parameters() const
Replace function returns by assignments to global variables.
::goto_functiont goto_functiont
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
void visit_pre(std::function< void(exprt &)>)
symbol_exprt return_value_symbol(const irep_idt &identifier, const namespacet &ns)
produces the symbol that is used to store the return value of the function with the given identifier
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Semantic type conversion.
symbol_tablet symbol_table
Symbol table.