Go to the documentation of this file.
9 #ifndef CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
10 #define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
104 bool allow_pointer_unsoundness);
157 bool allow_pointer_unsoundness);
160 #endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
Central data structure: state.
Base class for all expressions.
Control granularity of object accesses.
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
const std::size_t max_field_sensitivity_array_size
Magic numbers used throughout the codebase.
bool run_apply
whether or not to invoke field_sensitivityt::apply
Expression providing an SSA-renamed symbol of expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
field_sensitivityt(std::size_t max_array_size)
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.
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_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 ...
The interface of the target container for symbolic execution to record its symbolic steps into.