33 if(expr.
id()==ID_member)
36 else if(expr.
id()==ID_if)
48 else if(expr.
id()==ID_index)
70 if(expr.
id()==ID_member)
75 else if(expr.
id()==ID_if)
81 else if(expr.
id()==ID_index)
85 else if(expr.
id()==ID_symbol)
100 if(expr.
id()==ID_byte_extract_little_endian ||
101 expr.
id()==ID_byte_extract_big_endian)
112 result.
id()==ID_address_of)
134 typet dest_type_subtype;
136 if(expr_type.
id()==ID_array && !keep_array)
137 dest_type_subtype=expr_type.
subtype();
139 dest_type_subtype=expr_type;
143 else if(expr.
id()==ID_index ||
144 expr.
id()==ID_member)
157 else if(expr.
id()==ID_dereference)
166 else if(expr.
id()==ID_if)
181 else if(expr.
id()==ID_symbol ||
182 expr.
id()==ID_string_constant ||
183 expr.
id()==ID_label ||
191 if(
ns.
follow(result.
type()).
id()==ID_array && !keep_array)
196 if(expr.
id()==ID_symbol &&
201 offset = *offset_opt;
219 else if(expr.
id() == ID_typecast)
227 typet dest_type_subtype;
229 if(expr_type.id() == ID_array && !keep_array)
230 dest_type_subtype = expr_type.
subtype();
232 dest_type_subtype = expr_type;
238 "goto_symext::address_arithmetic does not handle " + expr.
id_string());
241 INVARIANT((expr_type.id()==ID_array && !keep_array) ||
243 "either non-persistent array or pointer to result");
254 if(expr.
id()==ID_dereference)
257 bool expr_is_not_null =
false;
262 if(!expr_function.
empty())
284 symex_dereference_state,
303 else if(expr.
id()==ID_index &&
327 else if(expr.
id()==ID_index &&
333 else if(expr.
id()==ID_address_of)
346 else if(expr.
id()==ID_typecast)
351 if(tc_op.
id()==ID_address_of &&
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
The type of an expression, extends irept.
Semantic type conversion.
pointer_typet pointer_type(const typet &subtype)
goto_programt::const_targett pc
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
static bool is_index_member_symbol_if(const exprt &expr)
Thrown when we encounter an instruction, parameters to an instruction etc.
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
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
void get_original_name(exprt &expr) const
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.
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Expression classes for byte-level operators.
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Operator to dereference a pointer.
exprt address_arithmetic(const exprt &, statet &, guardt &, bool keep_array)
Evaluate an ID_address_of expression.
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Split an expression into a base object and a (byte) offset.
void dereference_rec(exprt &, statet &, guardt &, bool write)
std::vector< threadt > threads
The plus expression Associativity is not specified.
virtual void dereference(exprt &, statet &, bool write)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bitvector_typet index_type()
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Operator to return the address of an object.
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
void dereference_rec_address_of(exprt &, statet &, guardt &)
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 & struct_op() const
void trigger_auto_object(const exprt &, statet &)
call_stackt & call_stack()
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
source_locationt & add_source_location()
const source_locationt & source_location() const
#define UNREACHABLE
This should be used to mark dead code.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
const std::string & id_string() const
#define Forall_operands(it, expr)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const typet & subtype() const
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Wrapper for a function dereferencing pointer expressions using a value set.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
bitvector_typet char_type()
Symbolic Execution of ANSI-C.
irep_idt byte_extract_id()
symex_targett::sourcet source