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 #define BV_ADDR_BITS 8
20 
21 class namespacet;
22 
24 {
25 public:
26  // this numbers the objects
28  objectst objects;
29 
30  struct pointert
31  {
32  std::size_t object;
34 
36  {
37  }
38 
39  pointert(std::size_t _obj, mp_integer _off):object(_obj), offset(_off)
40  {
41  }
42  };
43 
44  // converts an (object,offset) pair to an expression
46  const pointert &pointer,
47  const typet &type) const;
48 
49  // converts an (object,0) pair to an expression
51  std::size_t object,
52  const typet &type) const;
53 
55  explicit pointer_logict(const namespacet &_ns);
56 
57  std::size_t add_object(const exprt &expr);
58 
59  // number of NULL object
60  std::size_t get_null_object() const
61  {
62  return null_object;
63  }
64 
65  // number of INVALID object
66  std::size_t get_invalid_object() const
67  {
68  return invalid_object;
69  }
70 
71  bool is_dynamic_object(const exprt &expr) const;
72 
73  void get_dynamic_objects(std::vector<std::size_t> &objects) const;
74 
75 protected:
76  const namespacet &ns;
78 
80  const mp_integer &offset,
81  const exprt &object) const;
82 
84  const mp_integer &offset,
85  const typet &pointer_type,
86  const exprt &src) const;
87 };
88 
89 #endif // CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H
The type of an expression.
Definition: type.h:20
std::size_t get_null_object() const
Definition: pointer_logic.h:60
BigInt mp_integer
Definition: mp_arith.h:19
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
void get_dynamic_objects(std::vector< std::size_t > &objects) const
const namespacet & ns
Definition: pointer_logic.h:76
hash_numbering< exprt, irep_hash > objectst
Definition: pointer_logic.h:27
std::size_t get_invalid_object() const
Definition: pointer_logic.h:66
pointert(std::size_t _obj, mp_integer _off)
Definition: pointer_logic.h:39
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bool is_dynamic_object(const exprt &expr) const
exprt pointer_expr(const pointert &pointer, const typet &type) const
pointer_logict(const namespacet &_ns)
objectst objects
Definition: pointer_logic.h:28
Base class for all expressions.
Definition: expr.h:46
std::size_t add_object(const exprt &expr)
std::size_t null_object
Definition: pointer_logic.h:77
exprt object_rec(const mp_integer &offset, const typet &pointer_type, const exprt &src) const
std::size_t invalid_object
Definition: pointer_logic.h:77