cprover
pointer_logic.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Pointer Logic
4
5Author: 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
19class namespacet;
20class pointer_typet;
21
23{
24public:
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
73protected:
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