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;
Common behaviour for abstract objects modelling aggregate values - arrays, structs,...
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual abstract_object_pointert add_object_context(const abstract_object_pointert &abstract_object) const
Wraps an existing object in any configured context object.
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.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
void insert(const abstract_object_pointert &o)
abstract_object_pointert first() const
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual internal_abstract_object_pointert mutable_clone() const
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 const typet & type() const
Get the real type of the variable this abstract object is representing.
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.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Base class for all expressions.
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.
abstract_object_sett values
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_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 ...
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
value_set_pointer_abstract_objectt(const typet &type)
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.
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
Evaluate reading the pointer's value.
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.
An abstraction of a pointer that tracks a single pointer.
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
#define PRECONDITION(CONDITION)
void for_each_comb(const std::vector< Con > &super_con, F f)
Call the function f on every combination of elements in super_con.
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.
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 abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton)
Helper for converting singleton value sets into its only value.
static abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values)
Value Set of Pointer Abstract Object.