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 <util/magic.h>
13 
14 class exprt;
15 class ssa_exprt;
16 class namespacet;
17 class goto_symex_statet;
18 class symex_targett;
19 
81 {
82 public:
85  explicit field_sensitivityt(std::size_t max_array_size)
86  : max_field_sensitivity_array_size(max_array_size)
87  {
88  }
89 
99  void field_assignments(
100  const namespacet &ns,
101  goto_symex_statet &state,
102  const ssa_exprt &lhs,
103  symex_targett &target,
104  bool allow_pointer_unsoundness);
105 
119  exprt
120  apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
121  const;
122 
132  const namespacet &ns,
133  goto_symex_statet &state,
134  const ssa_exprt &ssa_expr) const;
135 
143  bool is_divisible(const ssa_exprt &expr) const;
144 
145 private:
147  bool run_apply = true;
148 
150 
152  const namespacet &ns,
153  goto_symex_statet &state,
154  const exprt &lhs_fs,
155  const exprt &lhs,
156  symex_targett &target,
157  bool allow_pointer_unsoundness);
158 };
159 
160 #endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:45
exprt
Base class for all expressions.
Definition: expr.h:52
field_sensitivityt
Control granularity of object accesses.
Definition: field_sensitivity.h:80
field_sensitivityt::apply
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
Definition: field_sensitivity.cpp:21
field_sensitivityt::max_field_sensitivity_array_size
const std::size_t max_field_sensitivity_array_size
Definition: field_sensitivity.h:149
magic.h
Magic numbers used throughout the codebase.
field_sensitivityt::run_apply
bool run_apply
whether or not to invoke field_sensitivityt::apply
Definition: field_sensitivity.h:147
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:16
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
field_sensitivityt::field_sensitivityt
field_sensitivityt(std::size_t max_array_size)
Definition: field_sensitivity.h:85
field_sensitivityt::field_assignments
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.
Definition: field_sensitivity.cpp:219
field_sensitivityt::is_divisible
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
Definition: field_sensitivity.cpp:341
field_sensitivityt::field_assignments_rec
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.
Definition: field_sensitivity.cpp:245
field_sensitivityt::get_fields
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 ...
Definition: field_sensitivity.cpp:147
symex_targett
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:25