cprover
pointer_offset_size.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_UTIL_POINTER_OFFSET_SIZE_H
13 #define CPROVER_UTIL_POINTER_OFFSET_SIZE_H
14 
15 #include "mp_arith.h"
16 #include "irep.h"
17 
18 class exprt;
19 class namespacet;
20 class struct_typet;
21 class typet;
22 class member_exprt;
23 class constant_exprt;
24 
25 // these return -1 on failure
26 
27 // NOLINTNEXTLINE(readability/identifiers)
29 {
30  typedef std::pair<size_t, mp_integer> refst;
33  const namespacet &ns;
35 public:
37  const namespacet &_ns);
39  const refst &operator*() const { return current; }
40  const refst* operator->() const { return &current; }
41 };
42 
44  const struct_typet &type,
45  const irep_idt &member,
46  const namespacet &ns);
47 
49  const typet &type,
50  const namespacet &ns);
51 
53  const typet &type,
54  const namespacet &ns);
55 
57  const exprt &expr,
58  const namespacet &ns);
59 
60 // these return 'nil' on failure
61 
63  const member_exprt &,
64  const namespacet &ns);
65 
67  const struct_typet &type,
68  const irep_idt &member,
69  const namespacet &ns);
70 
72  const typet &type,
73  const namespacet &ns);
74 
76  const constant_exprt &expr,
77  const namespacet &ns);
78 
80  exprt &result,
81  mp_integer offset,
82  const typet &target_type,
83  const namespacet &ns);
84 
86  exprt &result,
87  const exprt &offset,
88  const typet &target_type,
89  const namespacet &ns);
90 
91 #endif // CPROVER_UTIL_POINTER_OFFSET_SIZE_H
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
The type of an expression.
Definition: type.h:20
exprt build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
BigInt mp_integer
Definition: mp_arith.h:19
const struct_typet & type
member_offset_iterator(const struct_typet &_type, const namespacet &_ns)
const refst * operator->() const
bool get_subexpression_at_offset(exprt &result, mp_integer offset, const typet &target_type, const namespacet &ns)
A constant literal expression.
Definition: std_expr.h:3685
Structure type.
Definition: std_types.h:296
Extract member of struct or union.
Definition: std_expr.h:3214
exprt size_of_expr(const typet &type, const namespacet &ns)
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
mp_integer compute_pointer_offset(const exprt &expr, const namespacet &ns)
Base class for all expressions.
Definition: expr.h:46
member_offset_iterator & operator++()
exprt member_offset_expr(const member_exprt &, const namespacet &ns)
std::pair< size_t, mp_integer > refst
const refst & operator*() const