34 if(expr.
id()==ID_member)
37 else if(expr.
id()==ID_if)
49 else if(expr.
id()==ID_index)
71 if(expr.
id()==ID_member)
76 else if(expr.
id()==ID_if)
82 else if(expr.
id()==ID_index)
86 else if(expr.
id()==ID_symbol)
101 if(expr.
id()==ID_byte_extract_little_endian ||
102 expr.
id()==ID_byte_extract_big_endian)
113 result.
id()==ID_address_of)
135 typet dest_type_subtype;
137 if(expr_type.
id()==ID_array && !keep_array)
138 dest_type_subtype=expr_type.
subtype();
140 dest_type_subtype=expr_type;
144 else if(expr.
id()==ID_index ||
145 expr.
id()==ID_member)
160 else if(expr.
id()==ID_dereference)
169 else if(expr.
id()==ID_if)
184 else if(expr.
id()==ID_symbol ||
185 expr.
id()==ID_string_constant ||
186 expr.
id()==ID_label ||
194 if(
ns.
follow(result.
type()).
id()==ID_array && !keep_array)
199 if(expr.
id()==ID_symbol &&
221 throw "goto_symext::address_arithmetic does not handle "+expr.
id_string();
224 assert((expr_type.
id()==ID_array && !keep_array) ||
236 if(expr.
id()==ID_dereference)
239 throw "dereference takes one operand";
254 symex_dereference_state,
272 else if(expr.
id()==ID_index &&
296 else if(expr.
id()==ID_index &&
302 else if(expr.
id()==ID_address_of)
312 else if(expr.
id()==ID_typecast)
317 if(tc_op.
id()==ID_address_of &&
virtual void do_simplify(exprt &expr)
The type of an expression.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const typet & follow(const typet &src) const
const ssa_exprt get_l1_object() const
pointer_typet pointer_type(const typet &subtype)
void dereference_rec(exprt &expr, statet &state, guardt &guard, const bool write)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
virtual void dereference(exprt &expr, statet &state, const bool write)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
static bool is_index_member_symbol_if(const exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const exprt & root_object() const
The trinary if-then-else operator.
bool get_bool(const irep_namet &name) const
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Expression classes for byte-level operators.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Operator to dereference a pointer.
void trigger_auto_object(const exprt &expr, statet &state)
irep_idt byte_extract_id()
split an expression into a base object and a (byte) offset
bitvector_typet index_type()
Operator to return the address of an object.
void dereference_rec_address_of(exprt &expr, statet &state, guardt &guard)
mp_integer compute_pointer_offset(const exprt &expr, const namespacet &ns)
symbol_tablet & new_symbol_table
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
Base class for all expressions.
const exprt & struct_op() const
call_stackt & call_stack()
source_locationt & add_source_location()
const source_locationt & source_location() const
const std::string & id_string() const
#define Forall_operands(it, expr)
const typet & subtype() const
exprt address_arithmetic(const exprt &expr, statet &state, guardt &guard, bool keep_array)
Evaluate an ID_address_of expression.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet char_type()
Symbolic Execution of ANSI-C.