46 value_stack(expr, environment, ns)
63 std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
81 return std::make_shared<constant_pointer_abstract_objectt>(*other);
85 bool matching_pointer =
90 return shared_from_this();
126 if(value.
id() == ID_address_of)
129 if(addressee.id() == ID_symbol)
135 else if(addressee.id() == ID_index)
138 auto const &array = array_index.array();
139 if(array.id() == ID_symbol)
142 out << array_symbol.get_identifier() <<
"[";
143 if(array_index.index().id() == ID_constant)
165 type().subtype(), ns, is_value_top, !is_value_top);
177 const std::stack<exprt> &stack,
179 bool merging_write)
const
184 environment, ns, stack, new_value, merging_write);
200 environment.
assign(value, merged_value, ns);
204 environment.
assign(value, new_value, ns);
212 environment.
write(pointed_value, new_value, stack, ns, merging_write);
213 environment.
assign(value, modified_value, ns);
217 return std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(
An abstract version of a program environment.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
virtual abstract_object_pointert write(const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write)
Used within assign to do the actual dispatch.
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 assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
virtual exprt to_constant() const
Converts to a constant expression if possible.
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 void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
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.
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.
This is the basic interface of the abstract interpreter with default implementations of the core func...
const irep_idt & get_value() const
abstract_object_pointert merge_constant_pointers(const constant_pointer_abstract_pointert &other) const
Merges two constant pointers.
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
A helper function to dereference a value from a pointer.
sharing_ptrt< constant_pointer_abstract_objectt > constant_pointer_abstract_pointert
constant_pointer_abstract_objectt(const typet &type)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Print the value of the pointer.
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
exprt to_constant() const override
To try and find a constant expression for this abstract object.
abstract_object_pointert merge(abstract_object_pointert op1) const override
Set this abstract object to be the result of merging this abstract object.
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 override
A helper function to evaluate writing to a pointers value.
Base class for all expressions.
typet & type()
Return the type of the expression.
const irep_idt & id() const
static memory_sizet from_bytes(std::size_t bytes)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The type of an expression, extends irept.
bool is_top_value() const
Is the stack representing an unknown value and hence can't be written to or read from.
exprt to_expression() const
Convert the stack to an expression that can be used to write to.
An abstraction of a pointer that tracks a single pointer.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
#define PRECONDITION(CONDITION)
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.