38 const std::vector<abstract_object_pointert> &operands,
42 if(expr.
id() == ID_dereference)
46 expr, operands, environment, ns);
52 const std::stack<exprt> &stack,
53 const exprt &specifier,
55 bool merging_write)
const
73 const std::stack<exprt> &stack,
75 bool merging_write)
const
79 env.
havoc(
"Writing to a 2value pointer");
80 return shared_from_this();
83 return std::make_shared<abstract_pointer_objectt>(
type(),
true,
false);
An abstract version of a program environment.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
The base of all pointer abstractions.
pointer_typet pointer_type(const typet &subtype)
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...
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.
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 abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
Interface for transforms.
typet t
To enforce copy-on-write these are private and have read-only accessors.
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
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.
virtual abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const
Evaluate reading the pointer's value.
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
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.
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
abstract_pointer_objectt(const typet &type)
Base class for all expressions.
typet & type()
Return the type of the expression.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
The type of an expression, extends irept.
const typet & subtype() const
#define PRECONDITION(CONDITION)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::size_t number_of_pointers