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
Base class for all expressions.
Definition: expr.h:54
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
void get_dynamic_objects(std::vector< std::size_t > &objects) const
std::size_t get_null_object() const
Definition: pointer_logic.h:58
std::size_t get_invalid_object() const
Definition: pointer_logic.h:64
std::size_t invalid_object
Definition: pointer_logic.h:75
numberingt< exprt, irep_hash > objects
Definition: pointer_logic.h:26
std::size_t null_object
Definition: pointer_logic.h:75
std::size_t add_object(const exprt &expr)
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
const namespacet & ns
Definition: pointer_logic.h:74
bool is_dynamic_object(const exprt &expr) const
pointer_logict(const namespacet &_ns)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
BigInt mp_integer
Definition: smt_terms.h:12
pointert(std::size_t _obj, mp_integer _off)
Definition: pointer_logic.h:37