Go to the documentation of this file.
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;
99 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_POINTER_ABSTRACT_OBJECT_H
sharing_ptrt< class abstract_objectt > abstract_object_pointert
const_iterator begin() const
abstract_object_sett values
The type of an expression, extends irept.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Base class for all expressions.
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.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
value_sett::size_type size() const
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
an unordered set of value objects
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
Evaluate reading the pointer's value.
virtual exprt to_constant() const
Converts to a constant expression if possible.
const abstract_object_sett & get_values() const override
Getter for the set of stored abstract objects.
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 ...
value_set_pointer_abstract_objectt(const typet &type)
The base of all pointer abstractions.
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
This is the basic interface of the abstract interpreter with default implementations of the core func...
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
exprt to_constant() const override
Converts to a constant expression if possible.
void output(std::ostream &out, const ai_baset &ai, 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.
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.