Go to the documentation of this file.
38 template <
typename Con,
typename F>
40 const std::vector<Con> &super_con,
41 std::vector<typename Con::value_type> &sub_con,
44 size_t n = sub_con.size();
45 if(n == super_con.size())
49 for(
const auto &value : super_con[n])
51 sub_con.push_back(value);
63 template <
typename Con,
typename F>
66 std::vector<typename Con::value_type> sub_con;
84 std::make_shared<constant_pointer_abstract_objectt>(
type,
top,
bottom));
94 std::make_shared<constant_pointer_abstract_objectt>(expr, environment, ns));
111 std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
112 results.
insert(pointer->read_dereference(env, ns));
115 return results.
first();
121 const std::stack<exprt> &stack,
123 bool merging_write)
const
128 environment, ns, stack, new_value, merging_write);
134 std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
135 pointer->write_dereference(
136 environment, ns, stack, new_value, merging_write);
139 return shared_from_this();
156 return shared_from_this();
160 auto result = std::dynamic_pointer_cast<value_set_pointer_abstract_objectt>(
169 result->set_values(unwrapped_values);
177 auto cast_other = std::dynamic_pointer_cast<const value_set_tag>(other);
180 auto union_values =
values;
181 union_values.
insert(cast_other->get_values());
211 out <<
"value-set-begin: ";
215 out <<
" :value-set-end";
223 for(
auto const &value : values)
229 return unwrapped_values;
235 auto const &value_as_set =
236 std::dynamic_pointer_cast<const value_set_tag>(maybe_singleton);
240 PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
241 value_as_set->get_values().first()));
243 return value_as_set->get_values().first();
246 return maybe_singleton;
252 auto const &context_value =
253 std::dynamic_pointer_cast<const context_abstract_objectt>(maybe_wrapped);
255 return context_value ? context_value->unwrap_context() : maybe_wrapped;
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.
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...
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Base class for all expressions.
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.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
#define PRECONDITION(CONDITION)
static abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values)
static abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton)
Helper for converting singleton value sets into its only value.
void insert(const abstract_object_pointert &o)
An abstraction of a pointer that tracks a single pointer.
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
Evaluate reading the pointer's value.
abstract_object_pointert first() const
virtual abstract_object_pointert write_dereference(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &value, bool merging_write) const
Evaluate writing to a pointer's value.
void for_each_comb(const std::vector< Con > &super_con, F f)
Call the function f on every combination of elements in super_con.
static abstract_object_pointert maybe_unwrap_context(const abstract_object_pointert &maybe_wrapped)
Helper for converting context objects into its abstract-value children maybe_wrapped: either an abstr...
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 ...
virtual abstract_object_pointert add_object_context(const abstract_object_pointert &abstract_object) const
Wraps an existing object in any configured context object.
Common behaviour for abstract objects modelling aggregate values - arrays, structs,...
value_set_pointer_abstract_objectt(const typet &type)
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
This is the basic interface of the abstract interpreter with default implementations of the core func...
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
Value Set of Pointer Abstract Object.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
abstract_object_pointert write_dereference(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &new_value, bool merging_write) const override
Evaluate writing to a pointer's value.
virtual internal_abstract_object_pointert mutable_clone() const
void apply_comb(const std::vector< Con > &super_con, std::vector< typename Con::value_type > &sub_con, F f)
Recursively construct a combination sub_con from super_con and once constructed call f.
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.