Go to the documentation of this file.
37 return util_make_unique<constant_index_ranget>(val);
118 std::dynamic_pointer_cast<const abstract_value_objectt>(other);
128 auto other_expr = other->to_constant();
129 if(
is_bottom() && other_expr.is_constant())
130 return std::make_shared<constant_abstract_valuet>(other_expr);
132 if(
value == other_expr)
133 return shared_from_this();
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual bool is_top() const
Find out if the abstract object is top.
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
exprt to_constant() const override
Converts to a constant expression if possible.
The type of an expression, extends irept.
Base class for all expressions.
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Attempts to do a constant/constant merge if both are constants, otherwise falls back to the parent me...
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
Represents an interval of values.
Defines typet, type_with_subtypet and type_with_subtypest.
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 merge_constant_constant(const abstract_value_pointert &other) const
Merges another abstract value into this one.
value_range_implementation_ptrt value_range_implementation() const override
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
An abstract version of a program environment.
virtual exprt to_constant() const
Converts to a constant expression if possible.
std::set< abstract_object_pointert > abstract_object_visitedt
constant_abstract_valuet(const typet &t)
constant_index_ranget(const exprt &val)
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
bool is_constant() const
Return whether the expression is a constant.
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.
This is the basic interface of the abstract interpreter with default implementations of the core func...
std::size_t number_of_constants
static index_range_implementation_ptrt make_constant_index_range(const exprt &val)
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
index_range_implementation_ptrt reset() const override
virtual bool is_bottom() const
Find out if the abstract object is bottom.
constant_interval_exprt to_interval() const override
API to expression classes.
static memory_sizet from_bytes(std::size_t bytes)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
index_range_implementation_ptrt make_indeterminate_index_range()
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
An abstraction of a single value that just stores a constant.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.