100 for(
auto &instruction : goto_function.body.instructions)
104 if(instruction.has_condition())
106 exprt c = instruction.get_condition();
108 instruction.set_condition(
c);
Expression classes for byte-level operators.
bitvector_typet c_index_type()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class for all expressions.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
goto_functionst goto_functions
GOTO functions.
const irep_idt & id() const
const exprt & struct_op() const
A side_effect_exprt that returns a non-deterministically chosen value.
Union constructor from single element.
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
static bool have_to_rewrite_union(const exprt &expr)
void rewrite_union_address_of(exprt &expr)
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
byte_update_exprt make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
Construct a byte_update_exprt with endianness and byte width matching the current configuration.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.