Go to the documentation of this file.
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H
81 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
The type of an expression, extends irept.
~interval_abstract_valuet() override=default
Base class for all expressions.
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
abstract_object_pointert merge_intervals(abstract_value_pointert &other) const
Merge another interval abstract object with this one.
exprt to_constant() const override
Converts to a constant expression if possible.
Represents an interval of values.
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...
size_t internal_hash() const override
abstract_object_pointert meet_intervals(interval_abstract_value_pointert other) const
Meet another interval abstract object with this one.
constant_interval_exprt to_interval() const override
sharing_ptrt< interval_abstract_valuet > interval_abstract_value_pointert
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
std::set< abstract_object_pointert > abstract_object_visitedt
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Create a new abstract object that is the result of the merge, unless the object would be unchanged,...
bool internal_equality(const abstract_object_pointert &other) const override
Statistics gathering for the variable senstivity domain.
This is the basic interface of the abstract interpreter with default implementations of the core func...
interval_abstract_valuet(const typet &t)
abstract_object_pointert meet(const abstract_object_pointert &other) const override
Base implementation of the meet operation: only used if no more precise abstraction can be used,...
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
constant_interval_exprt interval
value_range_implementation_ptrt value_range_implementation() const override
API to expression classes.
typet t
To enforce copy-on-write these are private and have read-only accessors.
Common behaviour for abstract objects modelling values - constants, intervals, etc.