Go to the documentation of this file.
25 if(expr.
id()==ID_member)
29 if(op.
type().
id() == ID_union_tag || op.
type().
id() == ID_union)
32 else if(expr.
id()==ID_union)
49 if(expr.
id()==ID_index)
54 else if(expr.
id()==ID_member)
56 else if(expr.
id()==ID_symbol)
60 else if(expr.
id()==ID_dereference)
68 if(expr.
id()==ID_address_of)
80 if(expr.
id()==ID_member)
84 if(op.
type().
id() == ID_union_tag || op.
type().
id() == ID_union)
91 else if(expr.
id()==ID_union)
108 if(it->has_condition())
110 exprt c = it->get_condition();
112 it->set_condition(c);
#define Forall_goto_program_instructions(it, program)
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
#define Forall_operands(it, expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Union constructor from single element.
Base class for all expressions.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
irep_idt byte_update_id()
bitvector_typet index_type()
irep_idt byte_extract_id()
typet & type()
Return the type of the expression.
Expression classes for byte-level operators.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
#define forall_operands(it, expr)
const exprt & struct_op() const
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 irep_idt & id() const
#define Forall_goto_functions(it, functions)
::goto_functiont goto_functiont
A side_effect_exprt that returns a non-deterministically chosen value.
static bool have_to_rewrite_union(const exprt &expr)
A collection of goto functions.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
void rewrite_union_address_of(exprt &expr)
goto_functionst goto_functions
GOTO functions.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
API to expression classes.
const source_locationt & source_location() const