9#ifndef CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
10#define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
23 :
exprt(ID_field_sensitive_ssa, ssa.
type(),
std::move(fields))
25 add(ID_expression, ssa);
37 return base.
id() == ID_field_sensitive_ssa;
125 std::size_t max_array_size,
151 bool allow_pointer_unsoundness)
const;
192 bool disjoined_fields_only)
const;
216 const exprt &ssa_rhs,
218 bool allow_pointer_unsoundness)
const;
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
field_sensitive_ssa_exprt(const ssa_exprt &ssa, exprt::operandst &&fields)
const ssa_exprt & get_object_ssa() const
exprt simplify_opt(exprt e, const value_sett &value_set, const namespacet &ns) const
const bool should_simplify
const std::size_t max_field_sensitivity_array_size
field_sensitivityt(std::size_t max_array_size, bool should_simplify, const irep_idt &language_mode)
exprt get_fields(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &ssa_expr, bool disjoined_fields_only) const
Compute an expression representing the individual components of a field-sensitive SSA representation ...
void field_assignments_rec(const namespacet &ns, goto_symex_statet &state, const exprt &lhs_fs, const exprt &ssa_rhs, symex_targett &target, bool allow_pointer_unsoundness) const
Assign to the individual fields lhs_fs of a non-expanded symbol lhs.
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
void field_assignments(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &lhs, const exprt &rhs, symex_targett &target, bool allow_pointer_unsoundness) const
Assign to the individual fields of a non-expanded symbol lhs.
const irep_idt & language_mode
bool is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
Central data structure: state.
const irept & find(const irep_idt &name) const
const irep_idt & id() const
irept & add(const irep_idt &name)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Expression providing an SSA-renamed symbol of expressions.
The interface of the target container for symbolic execution to record its symbolic steps into.
State type in value_set_domaint, used in value-set analysis and goto-symex.
bool can_cast_expr< field_sensitive_ssa_exprt >(const exprt &base)
const field_sensitive_ssa_exprt & to_field_sensitive_ssa_expr(const exprt &expr)
#define PRECONDITION(CONDITION)