cprover
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:
24
26 const typet &new_type,
27 bool top,
28 bool bottom,
29 const abstract_object_sett &new_values);
30
33
35 const exprt &expr,
36 const abstract_environmentt &environment,
37 const namespacet &ns);
38
40 exprt to_constant() const override
41 {
42 verify();
43 return values.size() == 1 ? (*values.begin())->to_constant()
45 }
46
49 const abstract_object_sett &get_values() const override
50 {
51 return values;
52 }
53
56 void set_values(const abstract_object_sett &other_values);
57
60 static const size_t max_value_set_size = 10;
61
63 const abstract_environmentt &env,
64 const namespacet &ns) const override;
65
67 abstract_environmentt &environment,
68 const namespacet &ns,
69 const std::stack<exprt> &stack,
70 const abstract_object_pointert &new_value,
71 bool merging_write) const override;
72
74 const typet &new_type,
75 const abstract_environmentt &environment,
76 const namespacet &ns) const override;
77
79 const exprt &expr,
80 const std::vector<abstract_object_pointert> &operands,
81 const abstract_environmentt &environment,
82 const namespacet &ns) const override;
83
85 const exprt &expr,
86 const std::vector<abstract_object_pointert> &operands,
87 const abstract_environmentt &environment,
88 const namespacet &ns) const override;
89
90 void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
91 const override;
92
93protected:
94 CLONE
95
98 const abstract_object_pointert &other,
99 const widen_modet &widen_mode) const override;
100
101 exprt to_predicate_internal(const exprt &name) const override;
102
103private:
110 resolve_values(const abstract_object_sett &new_values) const;
111
112 // data
114};
115
116#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:119
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
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
CLONE abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const override
Merge two sets of constraints by appending to the first one.
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