cprover
Loading...
Searching...
No Matches
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{
21public:
23 explicit value_set_abstract_objectt(const typet &type);
24
27
29 const exprt &expr,
30 const abstract_environmentt &environment,
31 const namespacet &ns);
32
34 make_value_set(const abstract_object_sett &initial_values);
35
37 index_range_implementation(const namespacet &ns) const override;
38
40
42 exprt to_constant() const override;
43 constant_interval_exprt to_interval() const override;
44
46 constrain(const exprt &lower, const exprt &upper) const override;
47
50 const abstract_object_sett &get_values() const override
51 {
52 return values;
53 }
54
57 static const size_t max_value_set_size = 10;
58
59 void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
60 const override;
61
62protected:
63 CLONE
64
66 const abstract_value_pointert &other,
67 const widen_modet &widen_mode) const override;
68
70 meet_with_value(const abstract_value_pointert &other) const override;
71
72 exprt to_predicate_internal(const exprt &name) const override;
73
74private:
77 void set_values(const abstract_object_sett &other_values);
78
85 resolve_values(const abstract_object_sett &new_values) const;
86
87 void set_top_internal() override;
88
89 // data
91};
92
93#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::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:119
Represents an interval of values.
Definition interval.h:48
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:91
The type of an expression, extends irept.
Definition type.h:29
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_with_value(const abstract_value_pointert &other, const widen_modet &widen_mode) const override
abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override
constant_interval_exprt to_interval() const override
abstract_value_pointert constrain(const exprt &lower, const exprt &upper) const override
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 ...
const abstract_object_sett & get_values() const override
Getter for the set of stored abstract objects.
value_range_implementation_ptrt value_range_implementation() const override
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
static abstract_object_pointert make_value_set(const abstract_object_sett &initial_values)
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
exprt to_constant() const override
Converts to a constant expression if possible.