77 expr =
ode.root_object();
85 if(!
ode.offset().is_zero())
164 be.op()=
ode.root_object();
165 be.offset()=
ode.offset();
222 it.next_sibling_or_parent();
228 it.next_sibling_or_parent();
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet char_type()
bitvector_typet c_index_type()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Expression in which some part is missing and can be substituted for another expression.
Base class for all expressions.
std::vector< exprt > operandst
depth_iteratort depth_end()
depth_iteratort depth_begin()
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
Central data structure: state.
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...
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
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...
path_storaget & path_storage
Symbolic execution paths to be resumed later.
symex_target_equationt & target
The equation that this execution is building up.
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
shadow_memoryt shadow_memory
Shadow memory instrumentation API.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
void lift_lets(statet &, exprt &)
Execute any let expressions in expr using symex_assignt::assign_symbol.
virtual void do_simplify(exprt &expr)
messaget log
The messaget to write log messages to.
const symex_configt symex_config
The configuration to use for this symbolic execution.
virtual void dereference(exprt &, statet &, bool write)
Replace all dereference operations within expr with explicit references to the objects they may refer...
std::vector< symbol_exprt > instruction_local_symbols
Variables that should be killed at the end of the current symex_step invocation.
void process_array_expr(statet &, exprt &)
Given an expression, find the root object and the offset into it.
The trinary if-then-else operator.
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
message_handlert & get_message_handler()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Split an expression into a base object and a (byte) offset.
symex_nondet_generatort build_symex_nondet
Counter for nondet objects, which require unique names.
Expression providing an SSA-renamed symbol of expressions.
Functor for symex assignment.
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
Functor generating fresh nondet symbols.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Wrapper for a function dereferencing pointer expressions using a value set.
#define Forall_operands(it, expr)
Forward depth-first search iterators These iterators' copy operations are expensive,...
Storage of symbolic execution paths to resume.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
bool simplify(exprt &expr, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
bool is_ssa_expr(const exprt &expr)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Symbolic Execution of assignments.
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.
static void replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
Rewrite index/member expressions in byte_extract to offset.
Symbolic Execution of ANSI-C.
ssize_t write(int fildes, const void *buf, size_t nbyte)