33 const typet &new_type,
36 value_stack(old.value_stack)
45 value_stack(expr, environment, ns)
63 std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
74 std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
85 cast_other->value_stack.target_expression(d))
102 std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
109 cast_other->value_stack.offset_expression());
118 return std::make_shared<constant_pointer_abstract_objectt>(*other);
120 bool matching_pointers =
123 if(matching_pointers)
124 return shared_from_this();
156 if(value.
id() == ID_address_of)
159 if(addressee.id() == ID_symbol)
165 else if(addressee.id() == ID_dynamic_object)
167 out << addressee.get(ID_identifier);
169 else if(addressee.id() == ID_index)
172 auto const &array = array_index.array();
173 if(array.id() == ID_symbol)
176 out << array_symbol.get_identifier() <<
"[";
177 if(array_index.index().is_constant())
211 const std::stack<exprt> &stack,
213 bool merging_write)
const
217 environment.
havoc(
"Writing to a 2value pointer");
218 return shared_from_this();
222 return std::make_shared<constant_pointer_abstract_objectt>(
223 type(),
true,
false);
239 environment.
assign(value, merged_value, ns);
243 environment.
assign(value, new_value, ns);
251 environment.
write(pointed_value, new_value, stack, ns, merging_write);
252 environment.
assign(value, modified_value, ns);
256 return shared_from_this();
260 const typet &new_type,
268 if(value.
id() == ID_dynamic_object)
272 auto heap_array_type =
276 auto heap_symbol =
symbol_exprt(value.
get(ID_identifier), heap_array_type);
277 env.assign(heap_symbol, array_object, ns);
280 auto new_pointer = std::make_shared<constant_pointer_abstract_objectt>(
281 heap_address, env, ns);
285 return std::make_shared<constant_pointer_abstract_objectt>(new_type, *
this);
305 const std::vector<abstract_object_pointert> &operands,
309 auto &rhs = operands.back();
315 expr, operands, environment, ns);
335 if(
id == ID_notequal)
350 if(
id == ID_notequal)
357 const std::vector<abstract_object_pointert> &operands,
361 auto rhs = std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(
364 if(
is_top() || rhs->is_top())
369 auto lhs_offset =
offset();
370 auto rhs_offset = rhs->offset();
372 if(lhs_offset.id() == ID_member)
374 expr.
id(), lhs_offset, rhs_offset);
375 if(lhs_offset.id() == ID_symbol)
382 if(expr.
id() == ID_equal)
384 if(expr.
id() == ID_notequal)
390 const exprt &name)
const
An abstract version of a program environment.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Statistics gathering for the variable senstivity domain.
signedbv_typet signed_size_type()
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
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 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 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.
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
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
Operator to return the address of an object.
This is the basic interface of the abstract interpreter with default implementations of the core func...
A base class for relations, i.e., binary predicates whose two operands have the same type.
const irep_idt & get_value() const
abstract_object_pointert merge(const abstract_object_pointert &op1, const widen_modet &widen_mode) const override
Set this abstract object to be the result of merging this abstract object.
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
A helper function to dereference a value from a pointer.
abstract_object_pointert ptr_diff(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
sharing_ptrt< constant_pointer_abstract_objectt > constant_pointer_abstract_pointert
CLONE exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Print the value of the pointer.
abstract_object_pointert merge_constant_pointers(const constant_pointer_abstract_pointert &other, const widen_modet &widen_mode) const
Merges two constant pointers.
bool same_target(abstract_object_pointert other) const
exprt ptr_comparison_expr(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
exprt offset_from(abstract_object_pointert other) const
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 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 &value, bool merging_write) const override
A helper function to evaluate writing to a pointers value.
constant_pointer_abstract_objectt(const typet &type, bool top, bool bottom)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
The Boolean constant false.
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
irep_idt get_component_name() 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 Boolean constant true.
The type of an expression, extends irept.
exprt target_expression(size_t depth) const
exprt offset_expression() const
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.
static exprt to_bool_expr(bool v)
exprt struct_member_ptr_comparison_expr(irep_idt const &id, exprt const &lhs, exprt const &rhs)
exprt symbol_ptr_comparison_expr(irep_idt const &id, exprt const &lhs, exprt const &rhs)
An abstraction of a pointer that tracks a single pointer.
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.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
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.
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.
abstract_object_pointert object