Go to the documentation of this file.
56 else if(expr.
id()==ID_address_of)
63 else if(expr.
id()==ID_symbol &&
65 to_ssa_expr(expr).get_original_expr().
id()==ID_index)
74 else if(expr.
id() != ID_symbol)
84 if(expr.
type().
id() == ID_empty)
89 if(expr.
type().
id() != ID_array)
106 const typet &array_size_type = prev_array_type.
size().
type();
114 subtype_size_opt.value(), array_size_type);
115 new_offset =
div_exprt(new_offset, subtype_size);
151 if(expr.
id()==ID_byte_extract_big_endian ||
152 expr.
id()==ID_byte_extract_little_endian)
155 if(be.
op().
id()==ID_symbol &&
170 if(expr.
id() == ID_side_effect && expr.
get(ID_statement) == ID_nondet)
184 let_value = state.
rename(std::move(let_value),
ns).get();
194 value_assignment_guard);
204 if(it->id() == ID_let)
207 exprt &replaced_expr = it.mutate();
213 replaced_expr = replaced_let.
where();
215 it.next_sibling_or_parent();
217 else if(it->id() == ID_exists || it->id() == ID_forall)
221 it.next_sibling_or_parent();
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
Functor generating fresh nondet symbols.
static exprt conditional_cast(const exprt &expr, const typet &type)
const typet & subtype() const
Symbolic Execution of assignments.
std::vector< symbol_exprt > instruction_local_symbols
Variables that should be killed at the end of the current symex_step invocation.
#define Forall_operands(it, expr)
symex_nondet_generatort build_symex_nondet
Counter for nondet objects, which require unique names.
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...
static void replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
depth_iteratort depth_begin()
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
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.
symex_target_equationt & target
The equation that this execution is building up.
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Central data structure: state.
The trinary if-then-else operator.
Split an expression into a base object and a (byte) offset.
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Base class for all expressions.
void lift_let(statet &state, const let_exprt &let_expr)
Execute a single let expression, which should not have any nested let expressions (use lift_lets inst...
Functor for symex assignment.
Symbolic Execution of ANSI-C.
bitvector_typet index_type()
const exprt & get_original_expr() const
Expression providing an SSA-renamed symbol of expressions.
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
irep_idt byte_extract_id()
typet & type()
Return the type of the expression.
exprt & value()
convenience accessor for the value of a single binding
bool get_bool(const irep_namet &name) const
Expression classes for byte-level operators.
void process_array_expr(statet &, exprt &)
Given an expression, find the root object and the offset into it.
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.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
Rewrite index/member expressions in byte_extract to offset.
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
bool simplify(exprt &expr, const namespacet &ns)
const irep_idt & id() const
std::vector< exprt > operandst
const exprt & root_object() const
virtual void do_simplify(exprt &expr)
bitvector_typet char_type()
Wrapper for a function dereferencing pointer expressions using a value set.
bool is_zero() const
Return whether the expression is a constant representing 0.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
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,...
const irep_idt & get(const irep_namet &name) const
void lift_lets(statet &, exprt &)
Execute any let expressions in expr using symex_assignt::assign_symbol.
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.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
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...
depth_iteratort depth_end()
exprt & where()
convenience accessor for binding().where()
const source_locationt & source_location() const
Expression in which some part is missing and can be substituted for another expression.
static void process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
Given an expression, find the root object and the offset into it.