34 if(expr.
id() == ID_index || expr.
id() == ID_dereference)
51 codet havoc(ID_havoc_object);
64 code_assignt{expr, std::move(rhs), location}, location));
Operator to return the address of an object.
A goto_instruction_codet representing an assignment in the program.
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.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
virtual void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest)
Append goto instructions to havoc a single expression expr
const havoc_utils_can_forward_propagatet is_constant
virtual void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the underlying object of expr
void append_full_havoc_code(const source_locationt location, goto_programt &dest)
Append goto instructions to havoc the full assigns set.
virtual void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the value of expr
const irep_idt & id() const
A side_effect_exprt that returns a non-deterministically chosen value.
Utilities for building havoc code for expressions.
API to expression classes for Pointers.