27 if(expr.
id()==ID_member)
32 if(op_type.
id()==ID_union)
35 else if(expr.
id()==ID_union)
54 if(expr.
id()==ID_index)
59 else if(expr.
id()==ID_member)
61 else if(expr.
id()==ID_symbol)
65 else if(expr.
id()==ID_dereference)
75 if(expr.
id()==ID_address_of)
87 if(expr.
id()==ID_member)
92 if(op_type.
id()==ID_union)
99 else if(expr.
id()==ID_union)
The type of an expression.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
symbol_tablet symbol_table
Symbol table.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
const irep_idt & id() const
Expression classes for byte-level operators.
union constructor from single element
API to expression classes.
irep_idt byte_extract_id()
::goto_functiont goto_functiont
void rewrite_union_address_of(exprt &expr, const namespacet &ns)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
A side effect that returns a non-deterministically chosen value.
#define forall_operands(it, expr)
const typet & follow(const typet &) const
bitvector_typet index_type()
Base class for all expressions.
const exprt & struct_op() const
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
#define Forall_operands(it, expr)
#define Forall_goto_program_instructions(it, program)
void rewrite_union(exprt &expr, const namespacet &ns)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
goto_functionst goto_functions
GOTO functions.
static bool have_to_rewrite_union(const exprt &expr, const namespacet &ns)
irep_idt byte_update_id()