cprover
field_sensitivity.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-sensitive SSA
4
5Author: 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
16class exprt;
17class ssa_exprt;
18class namespacet;
20class symex_targett;
21
83{
84public:
87 explicit field_sensitivityt(std::size_t max_array_size)
88 : max_field_sensitivity_array_size(max_array_size)
89 {
90 }
91
102 const namespacet &ns,
103 goto_symex_statet &state,
104 const ssa_exprt &lhs,
105 symex_targett &target,
106 bool allow_pointer_unsoundness);
107
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
154private:
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