Go to the documentation of this file.
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
63 const std::stack<exprt> &stack,
64 const exprt &specifier,
66 bool merging_write)
const override;
102 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
abstract_object_sett values
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
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.
constant_interval_exprt to_interval() const override
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of an abstract object.
Represents an interval of values.
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 ...
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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.
an unordered set of value objects
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
const abstract_object_sett & get_values() const override
Getter for the set of stored abstract objects.
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
This is the basic interface of the abstract interpreter with default implementations of the core func...
value_range_implementation_ptrt value_range_implementation() const override
value_set_abstract_objectt(const typet &type)
void set_top_internal() override
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
exprt to_constant() const override
Converts to a constant expression if possible.
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
Common behaviour for abstract objects modelling values - constants, intervals, etc.