cprover
value_set_abstract_value.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity variable-sensitivity-value-set
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 // NOLINTNEXTLINE(whitespace/line_length)
13 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_VALUE_H
14 // NOLINTNEXTLINE(whitespace/line_length)
15 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_VALUE_H
16 
18 
19 #include <unordered_set>
20 
22 {
23 public:
24  using valuest = std::unordered_set<exprt, irep_hash>;
25 
27  const typet &type,
28  bool top = true,
29  bool bottom = false);
31  exprt expr,
32  const abstract_environmentt &environment,
33  const namespacet &ns);
35 
38  const valuest &get_values() const;
39 
40  CLONE
41 
43  static constexpr std::size_t max_value_set_size = 10;
44 
45  exprt to_constant() const override;
46 
48  const exprt &expr,
49  const std::vector<abstract_object_pointert> &operands,
50  const abstract_environmentt &environment,
51  const namespacet &ns) const override;
52 
53  void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
54  const override;
55 
56 protected:
58 
59 private:
64 };
65 
66 // NOLINTNEXTLINE(whitespace/line_length)
67 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_VALUE_H
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
#define CLONE
sharing_ptrt< class abstract_objectt > abstract_object_pointert
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
static constexpr CLONE std::size_t max_value_set_size
TODO arbitrary limit, make configurable.
const valuest & get_values() const
Get the possible values for this abstract object.
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.
valuest values
If BOTTOM then empty.
std::unordered_set< exprt, irep_hash > valuest
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
Print the value of the abstract object.
exprt to_constant() const override
Converts to a constant expression if possible.
abstract_object_pointert merge(abstract_object_pointert other) const override
Create a new abstract object that is the result of the merge, unless the object would be unchanged,...
value_set_abstract_valuet(const typet &type, bool top=true, bool bottom=false)