185 "goto_symext::address_arithmetic does not handle " + expr.
id_string());
191 "either non-persistent array or pointer to result");
241 assign.assign_symbol(
281 .is_safe_dereference(to_check, state.
source.
pc);
318 "simplify re-introduced dereferencing");
360 expr = std::move(
tmp2);
493 ns, state, state.
rename<
L1>(std::move(e),
ns).get(),
false);
500 expr = state.
rename<
L1>(std::move(expr),
ns).get();
525 "simplify re-introduced dereferencing");
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)
pointer_typet pointer_type(const typet &subtype)
bitvector_typet char_type()
bitvector_typet c_index_type()
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Expression in which some part is missing and can be substituted for another expression.
Base class for all expressions.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
sharing_mapt< exprt, symbol_exprt, false, irep_hash > dereference_cache
This is used for eliminating repeated complicated dereferences.
Central data structure: state.
call_stackt & call_stack()
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.
field_sensitivityt field_sensitivity
symex_targett::sourcet source
std::vector< threadt > threads
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
path_storaget & path_storage
Symbolic execution paths to be resumed later.
symex_target_equationt & target
The equation that this execution is building up.
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 trigger_auto_object(const exprt &, statet &)
void lift_lets(statet &, exprt &)
Execute any let expressions in expr using symex_assignt::assign_symbol.
exprt address_arithmetic(const exprt &, statet &, bool keep_array)
Transforms an lvalue expression by replacing any dereference operations it contains with explicit ref...
virtual void do_simplify(exprt &expr)
symbol_exprt cache_dereference(exprt &dereference_result, statet &state)
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...
void dereference_rec(exprt &expr, statet &state, bool write, bool is_in_quantifier)
If expr is a dereference_exprt, replace it with explicit references to the objects it may point to.
The trinary if-then-else operator.
const std::string & id_string() const
const irep_idt & id() const
message_handlert & get_message_handler()
Split an expression into a base object and a (byte) offset.
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Map function identifiers to local_safe_pointerst instances.
The plus expression Associativity is not specified.
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
std::optional< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
Expression to hold a symbol (variable)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Functor for symex assignment.
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
Semantic type conversion.
The type of an expression, extends irept.
Thrown when we encounter an instruction, parameters to an instruction etc.
Wrapper for a function dereferencing pointer expressions using a value set.
#define Forall_operands(it, expr)
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
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.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
std::optional< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
@ L1_WITH_CONSTANT_PROPAGATION
exprt get_original_name(exprt expr)
Undo all levels of renaming.
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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.
bool can_cast_expr< binding_exprt >(const exprt &base)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool can_cast_expr< let_exprt >(const exprt &base)
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.
goto_programt::const_targett pc
Symbolic Execution of assignments.
static exprt apply_to_objects_in_dereference(exprt e, const std::function< exprt(exprt)> &f)
Symbolic Execution of ANSI-C.
const type_with_subtypet & to_type_with_subtype(const typet &type)
ssize_t write(int fildes, const void *buf, size_t nbyte)