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
27 
28  struct pointert
29  {
30  std::size_t object;
32 
34  {
35  }
36 
37  pointert(std::size_t _obj, mp_integer _off):object(_obj), offset(_off)
38  {
39  }
40  };
41 
44  const pointert &pointer,
45  const pointer_typet &type) const;
46 
49  std::size_t object,
50  const pointer_typet &type) const;
51 
53  explicit pointer_logict(const namespacet &_ns);
54 
55  std::size_t add_object(const exprt &expr);
56 
58  std::size_t get_null_object() const
59  {
60  return null_object;
61  }
62 
64  std::size_t get_invalid_object() const
65  {
66  return invalid_object;
67  }
68 
69  bool is_dynamic_object(const exprt &expr) const;
70 
71  void get_dynamic_objects(std::vector<std::size_t> &objects) const;
72 
73 protected:
74  const namespacet &ns;
76 };
77 
78 #endif // CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H
pointer_logict::get_null_object
std::size_t get_null_object() const
Definition: pointer_logic.h:58
pointer_logict::get_dynamic_objects
void get_dynamic_objects(std::vector< std::size_t > &objects) const
Definition: pointer_logic.cpp:33
mp_arith.h
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
template_numberingt
Definition: numbering.h:22
pointer_logict::add_object
std::size_t add_object(const exprt &expr)
Definition: pointer_logic.cpp:43
exprt
Base class for all expressions.
Definition: expr.h:53
pointer_logict::pointer_logict
pointer_logict(const namespacet &_ns)
Definition: pointer_logic.cpp:153
pointer_logict::ns
const namespacet & ns
Definition: pointer_logic.h:74
pointer_logict
Definition: pointer_logic.h:23
pointer_logict::~pointer_logict
~pointer_logict()
Definition: pointer_logic.cpp:163
expr.h
pointer_logict::pointert::object
std::size_t object
Definition: pointer_logic.h:30
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
pointer_logict::objects
hash_numbering< exprt, irep_hash > objects
Definition: pointer_logic.h:26
pointer_logict::null_object
std::size_t null_object
Definition: pointer_logic.h:75
pointer_logict::pointert::offset
mp_integer offset
Definition: pointer_logic.h:31
pointer_logict::pointert::pointert
pointert()
Definition: pointer_logic.h:33
numbering.h
pointer_logict::is_dynamic_object
bool is_dynamic_object(const exprt &expr) const
Definition: pointer_logic.cpp:24
pointer_logict::invalid_object
std::size_t invalid_object
Definition: pointer_logic.h:75
pointer_logict::get_invalid_object
std::size_t get_invalid_object() const
Definition: pointer_logic.h:64
pointer_logict::pointert::pointert
pointert(std::size_t _obj, mp_integer _off)
Definition: pointer_logic.h:37
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
pointer_logict::pointert
Definition: pointer_logic.h:29
pointer_logict::pointer_expr
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
Definition: pointer_logic.cpp:67