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 
33  index_range_ptrt index_range(const namespacet &ns) const override;
34 
36  exprt to_constant() const override
37  {
38  verify();
39  return values.size() == 1 ? (*values.begin())->to_constant()
41  }
42 
48  const exprt &expr,
49  const std::vector<abstract_object_pointert> &operands,
50  const abstract_environmentt &environment,
51  const namespacet &ns) const override;
52 
55  const abstract_object_sett &get_values() const override
56  {
57  return values;
58  }
59 
62  void set_values(const abstract_object_sett &other_values);
63 
66  static const size_t max_value_set_size = 10;
67 
72  abstract_environmentt &environment,
73  const namespacet &ns,
74  const std::stack<exprt> &stack,
75  const exprt &specifier,
76  const abstract_object_pointert &value,
77  bool merging_write) const override;
78 
79  void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
80  const override;
81 
82 protected:
83  CLONE
84 
87 
88 private:
90  const typet &type,
91  const std::vector<abstract_object_sett> &operands,
92  const abstract_environmentt &env,
93  const namespacet &ns) const;
94 
102  const abstract_object_sett &new_values,
103  const abstract_environmentt &environment) const;
104 
111  resolve_values(const abstract_object_sett &new_values) const;
112 
113  // data
115 
120  to_interval(const abstract_object_sett &other_values) const;
121 };
122 
123 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
#define CLONE
sharing_ptrt< class abstract_objectt > abstract_object_pointert
an unordered set of value objects
Common behaviour for abstract objects modelling values - constants, intervals, etc.
std::shared_ptr< index_ranget > index_range_ptrt
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
index_range_ptrt index_range(const namespacet &ns) const override
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
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.
const abstract_object_sett & get_values() const override
Getter for the set of stored abstract objects.
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 ...
abstract_object_pointert to_interval(const abstract_object_sett &other_values) const
Cast the set of values other_values to an interval.
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
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.
exprt to_constant() const override
Converts to a constant expression if possible.
abstract_object_pointert evaluate_conditional(const typet &type, const std::vector< abstract_object_sett > &operands, const abstract_environmentt &env, const namespacet &ns) const