CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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{
21public:
23 const typet &new_type,
24 bool top,
25 bool bottom,
27
30
32 const exprt &expr,
33 const abstract_environmentt &environment,
34 const namespacet &ns);
35
37 exprt to_constant() const override
38 {
39 verify();
40 return values.size() == 1 ? (*values.begin())->to_constant()
42 }
43
46 const abstract_object_sett &get_values() const override
47 {
48 return values;
49 }
50
54
57 static const size_t max_value_set_size = 10;
58
61 const namespacet &ns) const override;
62
64 abstract_environmentt &environment,
65 const namespacet &ns,
66 const std::stack<exprt> &stack,
67 const abstract_object_pointert &new_value,
68 bool merging_write) const override;
69
71 const typet &new_type,
72 const abstract_environmentt &environment,
73 const namespacet &ns) const override;
74
76 const exprt &expr,
77 const std::vector<abstract_object_pointert> &operands,
78 const abstract_environmentt &environment,
79 const namespacet &ns) const override;
80
82 const exprt &expr,
83 const std::vector<abstract_object_pointert> &operands,
84 const abstract_environmentt &environment,
85 const namespacet &ns) const override;
86
87 void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
88 const override;
89
90protected:
92
95 const abstract_object_pointert &other,
96 const widen_modet &widen_mode) const override;
97
98 exprt to_predicate_internal(const exprt &name) const override;
99
100private:
108
109 // data
111};
112
113#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:117
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
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
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
abstract_object_pointert ptr_diff(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
exprt to_constant() const override
Converts to a constant expression if possible.
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) 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 ...
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 read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
A helper function to read elements from an array.
abstract_object_pointert typecast(const typet &new_type, const abstract_environmentt &environment, const namespacet &ns) const override
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.
exprt ptr_comparison_expr(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override