12#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H
13#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H
34 template <
typename... Args>
35 static std::shared_ptr<interval_abstract_valuet>
38 return std::make_shared<interval_abstract_valuet>(
39 std::forward<Args>(args)...);
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Common behaviour for abstract objects modelling values - constants, intervals, etc.
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
typet t
To enforce copy-on-write these are private and have read-only accessors.
abstract_value_objectt(const typet &type, bool tp, bool bttm)
This is the basic interface of the abstract interpreter with default implementations of the core func...
Represents an interval of values.
Base class for all expressions.
CLONE abstract_object_pointert merge_with_value(const abstract_value_pointert &other, const widen_modet &widen_mode) const override
Merge another interval abstract object with this one.
static std::shared_ptr< interval_abstract_valuet > make_interval(Args &&... args)
interval_abstract_valuet(const typet &t, bool tp, bool bttm)
bool internal_equality(const abstract_object_pointert &other) const override
constant_interval_exprt to_interval() const override
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
exprt to_constant() const override
Converts to a constant expression if possible.
abstract_value_pointert constrain(const exprt &lower, const exprt &upper) const override
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override
Meet another interval abstract object with this one.
value_range_implementation_ptrt value_range_implementation() const override
void set_top_internal() override
size_t internal_hash() const override
~interval_abstract_valuet() override=default
constant_interval_exprt interval
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.