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 
13  : abstract_objectt(t)
14 {
15  PRECONDITION(t.id() == ID_pointer);
16 }
17 
19  const typet &type,
20  bool top,
21  bool bottom)
22  : abstract_objectt(type, top, bottom)
23 {
24  PRECONDITION(type.id() == ID_pointer);
25 }
26 
28  const exprt &e,
29  const abstract_environmentt &environment,
30  const namespacet &ns)
31  : abstract_objectt(e, environment, ns)
32 {
33  PRECONDITION(e.type().id() == ID_pointer);
34 }
35 
37  const exprt &expr,
38  const std::vector<abstract_object_pointert> &operands,
39  const abstract_environmentt &environment,
40  const namespacet &ns) const
41 {
42  if(expr.id() == ID_dereference)
43  return read_dereference(environment, ns);
44 
46  expr, operands, environment, ns);
47 }
48 
50  abstract_environmentt &environment,
51  const namespacet &ns,
52  const std::stack<exprt> &stack,
53  const exprt &specifier,
54  const abstract_object_pointert &value,
55  bool merging_write) const
56 {
57  return write_dereference(environment, ns, stack, value, merging_write);
58 }
59 
61  const abstract_environmentt &env,
62  const namespacet &ns) const
63 {
65  const typet &pointed_to_type = pointer_type.subtype();
66 
67  return env.abstract_object_factory(pointed_to_type, ns, true, false);
68 }
69 
72  const namespacet &ns,
73  const std::stack<exprt> &stack,
74  const abstract_object_pointert &value,
75  bool merging_write) const
76 {
77  if(is_top() || is_bottom())
78  {
79  env.havoc("Writing to a 2value pointer");
80  return shared_from_this();
81  }
82 
83  return std::make_shared<abstract_pointer_objectt>(type(), true, false);
84 }
85 
87  abstract_object_statisticst &statistics,
88  abstract_object_visitedt &visited,
89  const abstract_environmentt &env,
90  const namespacet &ns) const
91 {
92  abstract_objectt::get_statistics(statistics, visited, env, ns);
93  ++statistics.number_of_pointers;
94 }
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)
Definition: c_types.cpp:243
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.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
const irep_idt & id() const
Definition: irep.h:407
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533