43 for(
auto it = goto_function.body.instructions.begin();
44 it != goto_function.body.instructions.end();
50 auto &
a_lhs = it->assign_lhs();
51 auto &
a_rhs = it->assign_rhs_nonconst();
68 const typet &
pt =
ct.parameters()[0].type();
69 const typet &st =
ct.parameters()[1].type();
78 goto_function.body.insert_before_swap(it,
call);
90 const typet &
pt =
ct.parameters()[0].type();
91 const typet &st =
ct.parameters()[1].type();
92 const typet &
vt =
ct.parameters()[2].type();
100 goto_function.body.insert_before_swap(it);
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
goto_instruction_codet representation of a function call statement.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
void visit_pre(std::function< void(exprt &)>)
typet & type()
Return the type of the expression.
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
The trinary if-then-else operator.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
const std::string & id2string(const irep_idt &d)
void mm_io(const exprt &mm_io_r, const exprt &mm_io_r_value, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
static std::set< dereference_exprt > collect_deref_expr(const exprt &src)
Perform Memory-mapped I/O instrumentation.
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt integer_address(const exprt &pointer)
Various predicates over pointers in programs.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
#define CHECK_RETURN(CONDITION)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.