cprover
pointer_logic.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pointer Logic
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H
13 #define CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H
14 
15 #include <util/mp_arith.h>
16 #include <util/expr.h>
17 #include <util/numbering.h>
18 
19 class namespacet;
20 class pointer_typet;
21 
23 {
24 public:
25  // this numbers the objects
28 
29  struct pointert
30  {
31  std::size_t object;
33 
35  {
36  }
37 
38  pointert(std::size_t _obj, mp_integer _off):object(_obj), offset(_off)
39  {
40  }
41  };
42 
43  // converts an (object,offset) pair to an expression
45  const pointert &pointer,
46  const pointer_typet &type) const;
47 
48  // converts an (object,0) pair to an expression
50  std::size_t object,
51  const pointer_typet &type) const;
52 
54  explicit pointer_logict(const namespacet &_ns);
55 
56  std::size_t add_object(const exprt &expr);
57 
58  // number of NULL object
59  std::size_t get_null_object() const
60  {
61  return null_object;
62  }
63 
64  // number of INVALID object
65  std::size_t get_invalid_object() const
66  {
67  return invalid_object;
68  }
69 
70  bool is_dynamic_object(const exprt &expr) const;
71 
72  void get_dynamic_objects(std::vector<std::size_t> &objects) const;
73 
74 protected:
75  const namespacet &ns;
77 
79  const mp_integer &offset,
80  const exprt &object) const;
81 };
82 
83 #endif // CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H
pointer_logict::get_null_object
std::size_t get_null_object() const
Definition: pointer_logic.h:59
pointer_logict::get_dynamic_objects
void get_dynamic_objects(std::vector< std::size_t > &objects) const
Definition: pointer_logic.cpp:36
mp_arith.h
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
template_numberingt
Definition: numbering.h:21
pointer_logict::add_object
std::size_t add_object(const exprt &expr)
Definition: pointer_logic.cpp:49
exprt
Base class for all expressions.
Definition: expr.h:54
pointer_logict::pointer_logict
pointer_logict(const namespacet &_ns)
Definition: pointer_logic.cpp:145
pointer_logict::ns
const namespacet & ns
Definition: pointer_logic.h:75
pointer_logict
Definition: pointer_logic.h:22
pointer_logict::~pointer_logict
~pointer_logict()
Definition: pointer_logic.cpp:155
expr.h
pointer_logict::pointert::object
std::size_t object
Definition: pointer_logic.h:31
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
pointer_logict::objects
objectst objects
Definition: pointer_logic.h:27
pointer_logict::null_object
std::size_t null_object
Definition: pointer_logic.h:76
pointer_logict::pointert::offset
mp_integer offset
Definition: pointer_logic.h:32
pointer_logict::pointert::pointert
pointert()
Definition: pointer_logic.h:34
numbering.h
pointer_logict::objectst
hash_numbering< exprt, irep_hash > objectst
Definition: pointer_logic.h:26
pointer_logict::is_dynamic_object
bool is_dynamic_object(const exprt &expr) const
Definition: pointer_logic.cpp:23
pointer_logict::invalid_object
std::size_t invalid_object
Definition: pointer_logic.h:76
pointer_logict::get_invalid_object
std::size_t get_invalid_object() const
Definition: pointer_logic.h:65
pointer_logict::pointert::pointert
pointert(std::size_t _obj, mp_integer _off)
Definition: pointer_logic.h:38
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
pointer_logict::pointert
Definition: pointer_logic.h:29
pointer_logict::pointer_expr
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Definition: pointer_logic.cpp:73