cprover
value_set_pointer_abstract_object.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_POINTER_ABSTRACT_OBJECT_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_POINTER_ABSTRACT_OBJECT_H
14 
17 
19  public value_set_tag
20 {
21 public:
24 
27 
29  const exprt &expr,
30  const abstract_environmentt &environment,
31  const namespacet &ns);
32 
34  exprt to_constant() const override
35  {
36  verify();
37  return values.size() == 1 ? (*values.begin())->to_constant()
39  }
40 
43  const abstract_object_sett &get_values() const override
44  {
45  return values;
46  }
47 
50  void set_values(const abstract_object_sett &other_values);
51 
54  static const size_t max_value_set_size = 10;
55 
57  const abstract_environmentt &env,
58  const namespacet &ns) const override;
59 
61  abstract_environmentt &environment,
62  const namespacet &ns,
63  const std::stack<exprt> &stack,
64  const abstract_object_pointert &new_value,
65  bool merging_write) const override;
66 
67  void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
68  const override;
69 
70 protected:
71  CLONE
72 
75 
76 private:
84  const abstract_object_sett &new_values,
85  const abstract_environmentt &environment) const;
86 
93  resolve_values(const abstract_object_sett &new_values) const;
94 
95  // data
97 };
98 
99 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_POINTER_ABSTRACT_OBJECT_H
#define CLONE
sharing_ptrt< class abstract_objectt > abstract_object_pointert
an unordered set of value objects
The base of all pointer abstractions.
const_iterator begin() const
value_sett::size_type size() const
virtual exprt to_constant() const
Converts to a constant expression if possible.
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
Base class for all expressions.
Definition: expr.h:54
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The type of an expression, extends irept.
Definition: type.h:28
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
exprt to_constant() const override
Converts to a constant expression if possible.
static const size_t max_value_set_size
The threshold size for value-sets: past this threshold the object is either converted to interval or ...
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
const abstract_object_sett & get_values() const override
Getter for the set of stored abstract objects.
abstract_object_pointert resolve_new_values(const abstract_object_sett &new_values, const abstract_environmentt &environment) const
Update the set of stored values to new_values.
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
Evaluate reading the pointer's value.
abstract_object_pointert write_dereference(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &new_value, bool merging_write) const override
Evaluate writing to a pointer's value.