24 const std::function<
void()> &havoc_code_impl)
27 const auto skip_target =
32 if(expr.
id() == ID_dereference)
43 if(expr.
id() == ID_dereference)
53 codet havoc(ID_havoc_object);
69 t->code_nonconst().add_source_location() = source_location;
79 for(
const auto &expr : modifies)
81 if(expr.
id() == ID_index || expr.
id() == ID_dereference)
87 source_location, address_of_expr, dest);
unsignedbv_typet unsigned_int_type()
Operator to return the address of an object.
Data structure for representing an arbitrary statement in a program.
Base class for all expressions.
source_locationt & add_source_location()
typet & type()
Return the type of the expression.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
A side_effect_exprt that returns a non-deterministically chosen value.
A predicate that indicates that an address range is ok to write.
void append_object_havoc_code_for_expr(const source_locationt source_location, const exprt &expr, goto_programt &dest)
void append_safe_havoc_code_for_expr(const source_locationt source_location, const exprt &expr, goto_programt &dest, const std::function< void()> &havoc_code_impl)
void append_havoc_code(const source_locationt source_location, const modifiest &modifies, goto_programt &dest)
void append_scalar_havoc_code_for_expr(const source_locationt source_location, const exprt &expr, goto_programt &dest)
Utilities for building havoc code for expressions.
std::set< exprt > modifiest
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.