47 else if(expr.
id()==ID_address_of)
54 else if(expr.
id()==ID_symbol &&
65 else if(expr.
id() != ID_symbol)
75 if(expr.type().id() != ID_array)
95 if(new_offset.type() != array_size_type)
98 if(subtype_size.
type() != array_size_type)
100 new_offset =
div_exprt(new_offset, subtype_size);
122 if(expr.
id()==ID_byte_extract_big_endian ||
123 expr.
id()==ID_byte_extract_little_endian)
126 if(be.
op().
id()==ID_symbol &&
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
The type of an expression.
exprt size_of_expr(const typet &type, const namespacet &ns)
static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
Rewrite index/member expressions in byte_extract to offset.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
void replace_nondet(exprt &)
const exprt & root_object() const
The trinary if-then-else operator.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
virtual void do_simplify(exprt &)
bool get_bool(const irep_namet &name) const
virtual void dereference(exprt &, statet &, const bool write)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Expression classes for byte-level operators.
division (integer and real)
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
irep_idt byte_extract_id()
split an expression into a base object and a (byte) offset
const exprt & size() const
bitvector_typet index_type()
void process_array_expr(exprt &)
Given an expression, find the root object and the offset into it.
void clean_expr(exprt &, statet &, bool write)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
const exprt & get_original_expr() const
#define Forall_operands(it, expr)
const typet & subtype() const
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
void make_typecast(const typet &_type)
Expression providing an SSA-renamed symbol of expressions.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
bitvector_typet char_type()