cprover
value_set_abstract_object.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: diffblue
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
14 
17 
19  public value_set_tag
20 {
21 public:
23  explicit value_set_abstract_objectt(const typet &type);
24 
26  value_set_abstract_objectt(const typet &type, bool top, bool bottom);
27 
29  const exprt &expr,
30  const abstract_environmentt &environment,
31  const namespacet &ns);
32 
34  index_range_implementation(const namespacet &ns) const override;
35 
37 
39  exprt to_constant() const override;
40  constant_interval_exprt to_interval() const override;
41 
44  const abstract_object_sett &get_values() const override
45  {
46  return values;
47  }
48 
51  void set_values(const abstract_object_sett &other_values);
52 
55  static const size_t max_value_set_size = 10;
56 
61  abstract_environmentt &environment,
62  const namespacet &ns,
63  const std::stack<exprt> &stack,
64  const exprt &specifier,
65  const abstract_object_pointert &value,
66  bool merging_write) const override;
67 
68  void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
69  const override;
70 
71 protected:
72  CLONE
73 
76 
77 private:
85  const abstract_object_sett &new_values,
86  const abstract_environmentt &environment) const;
87 
94  resolve_values(const abstract_object_sett &new_values) const;
95 
96  // data
98 
99  void set_top_internal() override;
100 };
101 
102 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
value_set_abstract_objectt::values
abstract_object_sett values
Definition: value_set_abstract_object.h:97
value_set_abstract_objectt::merge
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
Definition: value_set_abstract_object.cpp:237
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
value_set_tag
Definition: abstract_object_set.h:92
typet
The type of an expression, extends irept.
Definition: type.h:28
abstract_objectt::type
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Definition: abstract_object.cpp:53
abstract_object_sett
Definition: abstract_object_set.h:19
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
value_set_abstract_objectt::to_interval
constant_interval_exprt to_interval() const override
Definition: value_set_abstract_object.cpp:180
CLONE
#define CLONE
Definition: abstract_object.h:47
value_set_abstract_objectt::write
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of an abstract object.
Definition: value_set_abstract_object.cpp:185
constant_interval_exprt
Represents an interval of values.
Definition: interval.h:56
value_set_abstract_objectt::max_value_set_size
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 ...
Definition: value_set_abstract_object.h:55
value_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
Definition: abstract_value_object.h:130
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
value_set_abstract_objectt
Definition: value_set_abstract_object.h:20
abstract_value_objectt
Definition: abstract_value_object.h:240
value_set_abstract_objectt::resolve_new_values
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.
Definition: value_set_abstract_object.cpp:202
abstract_object_set.h
an unordered set of value objects
value_set_abstract_objectt::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Definition: value_set_abstract_object.cpp:282
value_set_abstract_objectt::index_range_implementation
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
Definition: value_set_abstract_object.cpp:143
value_set_abstract_objectt::get_values
const abstract_object_sett & get_values() const override
Getter for the set of stored abstract objects.
Definition: value_set_abstract_object.h:44
abstract_objectt::bottom
bool bottom
Definition: abstract_object.h:362
value_set_abstract_objectt::set_values
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
Definition: value_set_abstract_object.cpp:265
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
value_set_abstract_objectt::value_range_implementation
value_range_implementation_ptrt value_range_implementation() const override
Definition: value_set_abstract_object.cpp:161
value_set_abstract_objectt::value_set_abstract_objectt
value_set_abstract_objectt(const typet &type)
Definition: value_set_abstract_object.cpp:114
value_set_abstract_objectt::set_top_internal
void set_top_internal() override
Definition: value_set_abstract_object.cpp:259
abstract_objectt::top
bool top
Definition: abstract_object.h:363
index_range_implementation_ptrt
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
Definition: abstract_value_object.h:25
value_set_abstract_objectt::to_constant
exprt to_constant() const override
Converts to a constant expression if possible.
Definition: value_set_abstract_object.cpp:166
value_set_abstract_objectt::resolve_values
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
Definition: value_set_abstract_object.cpp:210
abstract_value_object.h
Common behaviour for abstract objects modelling values - constants, intervals, etc.