18#define ENABLE_ARRAY_FIELD_SENSITIVITY
44 *it =
apply(ns, state, std::move(*it), write);
57#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
84 tmp.set_expression(member);
86 return state.
rename(std::move(
tmp), ns).get();
88 return std::move(
tmp);
91#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
109 bool was_l2 = !
tmp.get_level_2().empty();
135 tmp.set_expression(index);
137 return state.
rename(std::move(
tmp), ns).get();
139 return std::move(
tmp);
166 fields.reserve(components.size());
170 for(
const auto &
comp : components)
173 bool was_l2 = !
tmp.get_level_2().empty();
174 tmp.remove_level_2();
186#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
208 bool was_l2 = !
tmp.get_level_2().empty();
209 tmp.remove_level_2();
210 tmp.set_expression(index);
231 bool allow_pointer_unsoundness)
238 ns, state,
lhs_fs, lhs, target, allow_pointer_unsoundness);
258 bool allow_pointer_unsoundness)
274 allow_pointer_unsoundness)
293 components.empty() ||
294 (
lhs_fs.has_operands() &&
lhs_fs.operands().size() == components.size()));
296 exprt::operandst::const_iterator
fs_it =
lhs_fs.operands().begin();
297 for(
const auto &
comp : components)
307#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
317 exprt::operandst::const_iterator
fs_it =
lhs_fs.operands().begin();
329 else if(
lhs_fs.has_operands())
334 exprt::operandst::const_iterator
fs_it =
lhs_fs.operands().begin();
338 ns, state, *
fs_it, op, target, allow_pointer_unsoundness);
353#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Array constructor from list of elements.
typet index_type() const
The type of the index expressions into any instance of this type.
const exprt & size() const
Base class for all expressions.
std::vector< exprt > operandst
bool has_operands() const
Return true if there is at least one operand.
typet & type()
Return the type of the expression.
bool run_apply
whether or not to invoke field_sensitivityt::apply
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
void field_assignments(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &lhs, symex_targett &target, bool allow_pointer_unsoundness)
Assign to the individual fields of a non-expanded symbol lhs.
void field_assignments_rec(const namespacet &ns, goto_symex_statet &state, const exprt &lhs_fs, const exprt &lhs, symex_targett &target, bool allow_pointer_unsoundness)
Assign to the individual fields lhs_fs of a non-expanded symbol lhs.
exprt get_fields(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &ssa_expr) const
Compute an expression representing the individual components of a field-sensitive SSA representation ...
const std::size_t max_field_sensitivity_array_size
NODISCARD exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
Central data structure: state.
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...
NODISCARD renamedt< ssa_exprt, L2 > assignment(ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
symex_targett::sourcet source
const irep_idt & id() const
Extract member of struct or union.
const exprt & struct_op() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Expression providing an SSA-renamed symbol of expressions.
const exprt & get_original_expr() const
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
const componentst & components() const
std::vector< componentt > componentst
const irep_idt & get_identifier() const
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The interface of the target container for symbolic execution to record its symbolic steps into.
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)=0
Write to a local variable.
#define Forall_operands(it, expr)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(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.
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Generate Equation using Symbolic Execution.