53 std::make_shared<constant_pointer_abstract_objectt>(
type,
top,
bottom));
63 std::make_shared<constant_pointer_abstract_objectt>(expr, environment, ns));
72 return env.abstract_object_factory(
80 std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
81 results.insert(pointer->read_dereference(
env, ns));
90 const std::stack<exprt> &stack,
96 environment.
havoc(
"Writing to a 2value pointer");
103 std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
104 pointer->write_dereference(
124 std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
127 return std::make_shared<value_set_pointer_abstract_objectt>(
133 const std::vector<abstract_object_pointert> &operands,
138 std::dynamic_pointer_cast<const value_set_pointer_abstract_objectt>(
141 auto differences = std::vector<abstract_object_pointert>{};
145 auto lhsp = std::dynamic_pointer_cast<const abstract_pointer_objectt>(
lhsv);
146 for(
auto const &
rhsp : rhs->values)
148 auto ops = std::vector<abstract_object_pointert>{
lhsp,
rhsp};
153 return std::accumulate(
160 return abstract_objectt::merge(lhs, rhs, widen_modet::no).object;
166 const std::vector<abstract_object_pointert> &operands,
171 std::dynamic_pointer_cast<const value_set_pointer_abstract_objectt>(
178 auto lhsp = std::dynamic_pointer_cast<const abstract_pointer_objectt>(
lhsv);
179 for(
auto const &
rhsp : rhs->values)
181 auto ops = std::vector<abstract_object_pointert>{
lhsp,
rhsp};
203 auto result = std::dynamic_pointer_cast<value_set_pointer_abstract_objectt>(
221 auto cast_other = std::dynamic_pointer_cast<const value_set_tag>(other);
233 const exprt &name)
const
244 return value->to_predicate(name);
274 out <<
"value-set-begin: ";
278 out <<
" :value-set-end";
286 for(
auto const &value : values)
297 auto const &
value_as_set = std::dynamic_pointer_cast<const value_set_tag>(
302 PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
An abstract version of a program environment.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual void havoc(const std::string &havoc_string)
This should be used as a default case / everything else has failed The string is so that I can easily...
const_iterator begin() const
value_sett::size_type size() const
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
const_iterator end() 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 combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
This is the basic interface of the abstract interpreter with default implementations of the core func...
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class for all expressions.
std::vector< exprt > operandst
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.
abstract_object_pointert ptr_diff(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
CLONE abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const override
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 ...
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 read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
A helper function to read elements from an array.
abstract_object_pointert typecast(const typet &new_type, const abstract_environmentt &environment, 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.
exprt ptr_comparison_expr(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
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...
API to expression classes for Pointers.
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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.
static abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values)
Value Set of Pointer Abstract Object.