Go to the documentation of this file.
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);
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Base class for all expressions.
Utilities for building havoc code for expressions.
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)
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
std::set< exprt > modifiest
typet & type()
Return the type of the expression.
void append_scalar_havoc_code_for_expr(const source_locationt source_location, const exprt &expr, goto_programt &dest)
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
API to expression classes for Pointers.
void append_object_havoc_code_for_expr(const source_locationt source_location, const exprt &expr, goto_programt &dest)
unsignedbv_typet unsigned_int_type()
const irep_idt & id() const
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
A side_effect_exprt that returns a non-deterministically chosen value.
A predicate that indicates that an address range is ok to write.
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
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.
void append_havoc_code(const source_locationt source_location, const modifiest &modifies, goto_programt &dest)
Operator to return the address of an object.
source_locationt & add_source_location()
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
instructionst::iterator targett
Data structure for representing an arbitrary statement in a program.