cprover
field_sensitivity.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-sensitive SSA
4 
5 Author: Michael Tautschnig
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
10 #define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
11 
12 #include <cstddef>
13 
14 #include <util/nodiscard.h>
15 
16 class exprt;
17 class ssa_exprt;
18 class namespacet;
19 class goto_symex_statet;
20 class symex_targett;
21 
83 {
84 public:
87  explicit field_sensitivityt(std::size_t max_array_size)
88  : max_field_sensitivity_array_size(max_array_size)
89  {
90  }
91 
101  void field_assignments(
102  const namespacet &ns,
103  goto_symex_statet &state,
104  const ssa_exprt &lhs,
105  symex_targett &target,
106  bool allow_pointer_unsoundness);
107 
121  NODISCARD
122  exprt
123  apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
124  const;
126  exprt apply(
127  const namespacet &ns,
128  goto_symex_statet &state,
129  ssa_exprt expr,
130  bool write) const;
131 
141  const namespacet &ns,
142  goto_symex_statet &state,
143  const ssa_exprt &ssa_expr) const;
144 
152  bool is_divisible(const ssa_exprt &expr) const;
153 
154 private:
156  bool run_apply = true;
157 
159 
161  const namespacet &ns,
162  goto_symex_statet &state,
163  const exprt &lhs_fs,
164  const exprt &lhs,
165  symex_targett &target,
166  bool allow_pointer_unsoundness);
167 };
168 
169 #endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
Base class for all expressions.
Definition: expr.h:54
Control granularity of object accesses.
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.
field_sensitivityt(std::size_t max_array_size)
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.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:25
#define NODISCARD
Definition: nodiscard.h:22