Go to the documentation of this file.
52 std::set<exprt>::const_iterator
next;
58 return util_make_unique<value_set_index_ranget>(vals);
100 return util_make_unique<value_set_value_ranget>(vals);
138 std::make_shared<constant_abstract_valuet>(expr, environment, ns));
149 std::set<exprt> flattened;
150 for(
const auto &o :
values)
152 const auto &v = std::dynamic_pointer_cast<const abstract_value_objectt>(o);
153 for(
auto e : v->index_range(ns))
174 if(interval.is_single_value_interval())
175 return interval.get_lower();
188 const std::stack<exprt> &stack,
189 const exprt &specifier,
191 bool merging_write)
const
194 for(
const auto &st_value :
values)
197 st_value->write(environment, ns, stack, specifier, value, merging_write));
216 return shared_from_this();
222 return std::make_shared<interval_abstract_valuet>(
223 unwrapped_values.to_interval());
231 std::dynamic_pointer_cast<value_set_abstract_objectt>(
mutable_clone());
232 result->set_values(unwrapped_values);
241 auto other_value_set = std::dynamic_pointer_cast<const value_set_tag>(other);
244 union_values.insert(other_value_set->get_values());
249 std::dynamic_pointer_cast<const abstract_value_objectt>(other);
252 union_values.insert(other_value);
297 out <<
"value-set-begin: ";
301 out <<
" :value-set-end";
308 auto const &context_value =
309 std::dynamic_pointer_cast<const context_abstract_objectt>(maybe_wrapped);
311 return context_value ? context_value->unwrap_context() : maybe_wrapped;
318 for(
auto const &value : values)
324 return unwrapped_values;
330 auto const &value_as_set =
331 std::dynamic_pointer_cast<const value_set_tag>(maybe_singleton);
335 PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
336 value_as_set->get_values().first()));
338 return value_as_set->get_values().first();
341 return maybe_singleton;
348 return value->is_top();
static bool are_any_top(const abstract_object_sett &set)
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
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.
const_iterator begin() const
static abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values)
The type of an expression, extends irept.
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
std::set< exprt >::const_iterator next
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
value_range_implementation_ptrt reset() const override
const_iterator end() const
Base class for all expressions.
value_sett::const_iterator const_iterator
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.
bool advance_to_next() override
bool advance_to_next() override
abstract_object_sett::const_iterator next
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...
static abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton)
Helper for converting singleton value sets into its only value.
static value_range_implementation_ptrt make_value_set_value_range(const abstract_object_sett &vals)
const abstract_object_pointert & current() const override
value_sett::size_type size() const
Value Set Abstract Object.
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.
#define PRECONDITION(CONDITION)
const exprt & current() const override
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
void insert(const abstract_object_pointert &o)
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
abstract_object_pointert first() const
virtual exprt to_constant() const
Converts to a constant expression if possible.
static index_range_implementation_ptrt make_value_set_index_range(const std::set< exprt > &vals)
index_range_implementation_ptrt reset() const override
const abstract_object_sett & values
value_set_index_ranget(const std::set< exprt > &vals)
value_set_value_ranget(const abstract_object_sett &vals)
virtual abstract_object_pointert add_object_context(const abstract_object_pointert &abstract_object) const
Wraps an existing object in any configured context object.
An interval to represent a set of possible values.
The base type of all abstract array representations.
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...
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
value_range_implementation_ptrt value_range_implementation() const override
value_set_abstract_objectt(const typet &type)
static abstract_object_pointert maybe_unwrap_context(const abstract_object_pointert &maybe_wrapped)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
void set_top_internal() override
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
virtual bool is_bottom() const
Find out if the abstract object is bottom.
exprt to_constant() const override
Converts to a constant expression if possible.
abstract_object_pointert cur
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
constant_interval_exprt to_interval() const
Calculate the set of values as an interval.
index_range_implementation_ptrt make_indeterminate_index_range()
virtual internal_abstract_object_pointert mutable_clone() const
An abstraction of a single value that just stores a constant.