Go to the documentation of this file.
47 if(expr.
id()==ID_byte_extract_little_endian ||
48 expr.
id()==ID_byte_extract_big_endian)
58 if(be.
op().
type().
id() == ID_array && result.
id() == ID_address_of)
64 t->
id() == ID_array && expr.
type() != *t;
80 typet dest_type_subtype;
82 if(expr_type.
id()==ID_array && !keep_array)
83 dest_type_subtype=expr_type.
subtype();
85 dest_type_subtype=expr_type;
89 else if(expr.
id()==ID_index ||
103 else if(expr.
id()==ID_dereference)
112 else if(expr.
id()==ID_if)
127 else if(expr.
id()==ID_symbol ||
128 expr.
id()==ID_string_constant ||
129 expr.
id()==ID_label ||
137 if(result.
type().
id() == ID_array && !keep_array)
142 if(expr.
id()==ID_symbol &&
147 offset = *offset_opt;
165 else if(expr.
id() == ID_typecast)
173 typet dest_type_subtype;
175 if(expr_type.
id() == ID_array && !keep_array)
176 dest_type_subtype = expr_type.
subtype();
178 dest_type_subtype = expr_type;
184 "goto_symext::address_arithmetic does not handle " + expr.
id_string());
188 (expr_type.
id() == ID_array && !keep_array) ||
190 "either non-persistent array or pointer to result");
204 if(expr.
id()==ID_dereference)
206 bool expr_is_not_null =
false;
211 if(!expr_function.
empty())
217 .is_safe_dereference(to_check, state.
source.
pc);
254 "simplify re-introduced dereferencing");
265 symex_dereference_state,
279 expr.
id() == ID_index &&
to_index_expr(expr).array().
id() == ID_member &&
299 else if(expr.
id()==ID_index &&
305 else if(expr.
id()==ID_address_of)
316 else if(expr.
id()==ID_typecast)
322 tc_op.
id() == ID_address_of &&
350 if(
auto deref = expr_try_dynamic_cast<dereference_exprt>(e))
352 deref->op() = f(std::move(deref->op()));
407 ns, state, state.
rename<
L1>(std::move(e),
ns).get(),
false);
414 expr = state.
rename<
L1>(std::move(expr),
ns).get();
439 "simplify re-introduced dereferencing");
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void dereference_rec(exprt &, statet &, bool write)
If expr is a dereference_exprt, replace it with explicit references to the objects it may point to.
const typet & subtype() const
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
#define Forall_operands(it, expr)
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
The type of an expression, extends irept.
exprt address_arithmetic(const exprt &, statet &, bool keep_array)
Transforms an lvalue expression by replacing any dereference operations it contains with explicit ref...
goto_programt::const_targett pc
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Operator to dereference a pointer.
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Central data structure: state.
Thrown when we encounter an instruction, parameters to an instruction etc.
The trinary if-then-else operator.
Split an expression into a base object and a (byte) offset.
The plus expression Associativity is not specified.
Base class for all expressions.
symex_targett::sourcet source
void trigger_auto_object(const exprt &, statet &)
Symbolic Execution of ANSI-C.
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
bitvector_typet index_type()
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
irep_idt byte_extract_id()
typet & type()
Return the type of the expression.
bool get_bool(const irep_namet &name) const
std::vector< threadt > threads
Expression classes for byte-level operators.
call_stackt & call_stack()
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
virtual void dereference(exprt &, statet &, bool write)
Replace all dereference operations within expr with explicit references to the objects they may refer...
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
#define PRECONDITION(CONDITION)
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
const std::string & id_string() const
pointer_typet pointer_type(const typet &subtype)
exprt get_original_name(exprt expr)
Undo all levels of renaming.
const irep_idt & id() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const exprt & root_object() const
@ L1_WITH_CONSTANT_PROPAGATION
virtual void do_simplify(exprt &expr)
field_sensitivityt field_sensitivity
bitvector_typet char_type()
Wrapper for a function dereferencing pointer expressions using a value set.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Deprecated expression utility functions.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
static exprt apply_to_objects_in_dereference(exprt e, const std::function< exprt(exprt)> &f)
Forward depth-first search iterators These iterators' copy operations are expensive,...
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Map function identifiers to local_safe_pointerst instances.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const symex_configt symex_config
The configuration to use for this symbolic execution.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
Operator to return the address of an object.
source_locationt & add_source_location()
bool run_validation_checks
Should the additional validation checks be run? If this flag is set the checks for renaming (both lev...
Semantic type conversion.
const source_locationt & source_location() const