Go to the documentation of this file.
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_VALUE_OBJECT_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_VALUE_OBJECT_H
25 std::unique_ptr<index_range_implementationt>;
43 return range->current();
130 std::unique_ptr<value_range_implementationt>;
148 return range->current();
231 return util_make_unique<empty_value_ranget>();
285 const std::vector<abstract_object_pointert> &operands,
virtual value_range_implementation_ptrt reset() const =0
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
index_ranget(index_ranget &&rhs)
sharing_ptrt< class abstract_objectt > abstract_object_pointert
index_range_implementation_ptrt make_indeterminate_index_range()
value_ranget value_range() const
index_range_implementation_ptrt make_empty_index_range()
The type of an expression, extends irept.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
bool operator!=(const value_range_iteratort &other) const
index_range_iteratort end() const
const exprt & current() const override
value_range_iteratort(value_range_implementation_ptrt &&r)
abstract_object_pointert nothing
Base class for all expressions.
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
value_ranget(value_range_implementation_ptrt r)
virtual index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const =0
value_range_iteratort(const value_range_iteratort &)=delete
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
virtual value_range_implementation_ptrt value_range_implementation() const =0
Represents an interval of values.
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
virtual bool advance_to_next()=0
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
abstract_value_objectt(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
value_range_implementation_ptrt range
value_range_iteratort end() const
value_range_iteratort(value_range_iteratort &&rhs)
single_value_index_ranget(const exprt &val)
abstract_object_pointert value_type
const abstract_object_pointert & operator*() const
const abstract_object_pointert & current() const override
~index_range_iteratort()=default
virtual const exprt & current() const =0
virtual bool advance_to_next()=0
value_range_implementation_ptrt reset() const override
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
virtual index_range_implementation_ptrt reset() const =0
bool operator==(const value_range_iteratort &other) const
const exprt & operator*() const
index_range_iteratort(index_range_iteratort &&rhs)
index_ranget(const index_ranget &)=delete
index_range_implementation_ptrt range
bool operator==(const index_range_iteratort &other) const
bool advance_to_next() override
index_range_implementation_ptrt range
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const final
Interface for transforms.
index_ranget index_range(const namespacet &ns) const
virtual ~index_range_implementationt()=default
abstract_value_objectt(const typet &type, bool tp, bool bttm)
virtual ~value_range_implementationt()=default
value_ranget(const value_ranget &)=delete
bool advance_to_next() override
virtual constant_interval_exprt to_interval() const =0
value_ranget(value_ranget &&rhs)
index_range_iteratort(index_range_implementation_ptrt &&r)
bool operator!=(const index_range_iteratort &other) const
virtual const abstract_object_pointert & current() const =0
value_range_implementation_ptrt range
index_range_iteratort begin() const
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
index_ranget(index_range_implementation_ptrt r)
abstract_value_objectt(const typet &type)
index_range_iteratort(const index_range_iteratort &)=delete
~value_range_iteratort()=default
value_range_iteratort begin() const