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 &&
141 if(expr.
id() == ID_side_effect && expr.
get(ID_statement) == ID_nondet)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
The type of an expression, extends irept.
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)
Check types for equality across all levels of hierarchy.
The trinary if-then-else operator.
typet & type()
Return the type of the expression.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
virtual void do_simplify(exprt &)
bool get_bool(const irep_namet &name) const
symex_nondet_generatort build_symex_nondet
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.
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
const irep_idt & get(const irep_namet &name) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static void replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
Split an expression into a base object and a (byte) offset.
const exprt & size() const
virtual void dereference(exprt &, statet &, bool write)
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)
Expression to hold a nondeterministic choice.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
const exprt & root_object() const
const exprt & get_original_expr() const
const source_locationt & source_location() const
#define Forall_operands(it, expr)
bool is_zero() const
Return whether the expression is a constant representing 0.
source_locationt & add_source_location()
const typet & subtype() const
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Expression providing an SSA-renamed symbol of expressions.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
bitvector_typet char_type()
Functor generating fresh nondet symbols.
irep_idt byte_extract_id()