12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_POINTER_ABSTRACT_OBJECT_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_POINTER_ABSTRACT_OBJECT_H
63 const std::stack<exprt> &stack,
65 bool merging_write)
const override;
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...
Base class for all expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The type of an expression, extends irept.
abstract_object_sett values
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
exprt to_constant() const override
Converts to a constant expression if possible.
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 ...
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
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.
value_set_pointer_abstract_objectt(const typet &type)
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.
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
Evaluate reading the pointer's value.
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.