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 
83  const mp_integer &offset,
84  const typet &pointer_type,
85  const exprt &src) const;
86 };
87 
88 #endif // CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H
The type of an expression.
Definition: type.h:22
std::size_t get_null_object() const
Definition: pointer_logic.h:59
BigInt mp_integer
Definition: mp_arith.h:22
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
void get_dynamic_objects(std::vector< std::size_t > &objects) const
const namespacet & ns
Definition: pointer_logic.h:75
hash_numbering< exprt, irep_hash > objectst
Definition: pointer_logic.h:26
std::size_t get_invalid_object() const
Definition: pointer_logic.h:65
pointert(std::size_t _obj, mp_integer _off)
Definition: pointer_logic.h:38
The pointer type.
Definition: std_types.h:1435
TO_BE_DOCUMENTED.
Definition: namespace.h:74
bool is_dynamic_object(const exprt &expr) const
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
pointer_logict(const namespacet &_ns)
objectst objects
Definition: pointer_logic.h:27
Base class for all expressions.
Definition: expr.h:42
std::size_t add_object(const exprt &expr)
std::size_t null_object
Definition: pointer_logic.h:76
exprt object_rec(const mp_integer &offset, const typet &pointer_type, const exprt &src) const
std::size_t invalid_object
Definition: pointer_logic.h:76