cprover
abstract_pointer_object.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Thomas Kiley, thomas.kiley@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include <util/pointer_expr.h>
13 
15  : abstract_objectt(t)
16 {
17  PRECONDITION(t.id() == ID_pointer);
18 }
19 
21  const typet &type,
22  bool top,
23  bool bottom)
24  : abstract_objectt(type, top, bottom)
25 {
26  PRECONDITION(type.id() == ID_pointer);
27 }
28 
30  const exprt &e,
31  const abstract_environmentt &environment,
32  const namespacet &ns)
33  : abstract_objectt(e, environment, ns)
34 {
35  PRECONDITION(e.type().id() == ID_pointer);
36 }
37 
39  const exprt &expr,
40  const std::vector<abstract_object_pointert> &operands,
41  const abstract_environmentt &environment,
42  const namespacet &ns) const
43 {
44  if(expr.id() == ID_dereference)
45  return read_dereference(environment, ns);
46 
48  expr, operands, environment, ns);
49 }
50 
52  abstract_environmentt &environment,
53  const namespacet &ns,
54  const std::stack<exprt> &stack,
55  const exprt &specifier,
56  const abstract_object_pointert &value,
57  bool merging_write) const
58 {
59  return write_dereference(environment, ns, stack, value, merging_write);
60 }
61 
63  const abstract_environmentt &env,
64  const namespacet &ns) const
65 {
67  const typet &pointed_to_type = pointer_type.subtype();
68 
69  return env.abstract_object_factory(pointed_to_type, ns, true, false);
70 }
71 
74  const namespacet &ns,
75  const std::stack<exprt> &stack,
76  const abstract_object_pointert &value,
77  bool merging_write) const
78 {
79  if(is_top() || is_bottom())
80  {
81  env.havoc("Writing to a 2value pointer");
82  return shared_from_this();
83  }
84 
85  return std::make_shared<abstract_pointer_objectt>(type(), true, false);
86 }
87 
89  abstract_object_statisticst &statistics,
90  abstract_object_visitedt &visited,
91  const abstract_environmentt &env,
92  const namespacet &ns) const
93 {
94  abstract_objectt::get_statistics(statistics, visited, env, ns);
95  ++statistics.number_of_pointers;
96 }
typet::subtype
const typet & subtype() const
Definition: type.h:47
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
abstract_objectt::is_top
virtual bool is_top() const
Find out if the abstract object is top.
Definition: abstract_object.cpp:150
abstract_object_statisticst::number_of_pointers
std::size_t number_of_pointers
Definition: abstract_object_statistics.h:24
typet
The type of an expression, extends irept.
Definition: type.h:28
abstract_objectt::type
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Definition: abstract_object.cpp:53
abstract_pointer_objectt::expression_transform
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.
Definition: abstract_pointer_object.cpp:38
abstract_pointer_objectt::abstract_pointer_objectt
abstract_pointer_objectt(const typet &type)
Definition: abstract_pointer_object.cpp:14
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
abstract_environmentt::havoc
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...
Definition: abstract_environment.cpp:322
abstract_objectt::get_statistics
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
Definition: abstract_object.cpp:284
abstract_pointer_objectt::get_statistics
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
Definition: abstract_pointer_object.cpp:88
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
abstract_environmentt::abstract_object_factory
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.
Definition: abstract_environment.cpp:251
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
pointer_expr.h
API to expression classes for Pointers.
abstract_environment.h
An abstract version of a program environment.
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
irept::id
const irep_idt & id() const
Definition: irep.h:407
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:76
abstract_pointer_objectt::write_dereference
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.
Definition: abstract_pointer_object.cpp:72
abstract_pointer_objectt::read_dereference
virtual abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const
Evaluate reading the pointer's value.
Definition: abstract_pointer_object.cpp:62
abstract_pointer_object.h
The base of all pointer abstractions.
abstract_objectt
Definition: abstract_object.h:79
abstract_objectt::is_bottom
virtual bool is_bottom() const
Find out if the abstract object is bottom.
Definition: abstract_object.cpp:155
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
abstract_pointer_objectt::write
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.
Definition: abstract_pointer_object.cpp:51
abstract_objectt::t
typet t
To enforce copy-on-write these are private and have read-only accessors.
Definition: abstract_object.h:361
abstract_objectt::expression_transform
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.
Definition: abstract_object.cpp:108