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 "irep.h"
16 #include "mp_arith.h"
17 #include "optional.h"
18 
19 class exprt;
20 class namespacet;
21 class struct_typet;
22 class typet;
23 class member_exprt;
24 class constant_exprt;
25 
26 // these return 'nullopt' on failure
27 
29  const struct_typet &type,
30  const irep_idt &member,
31  const namespacet &ns);
32 
34  const struct_typet &type,
35  const irep_idt &member,
36  const namespacet &ns);
37 
39 pointer_offset_size(const typet &type, const namespacet &ns);
40 
42 pointer_offset_bits(const typet &type, const namespacet &ns);
43 
45 compute_pointer_offset(const exprt &expr, const namespacet &ns);
46 
47 // these return 'nil' on failure
48 
50  const member_exprt &,
51  const namespacet &ns);
52 
54  const struct_typet &type,
55  const irep_idt &member,
56  const namespacet &ns);
57 
59  const typet &type,
60  const namespacet &ns);
61 
63  const constant_exprt &expr,
64  const namespacet &ns);
65 
67  const exprt &expr,
68  const mp_integer &offset,
69  const typet &target_type,
70  const namespacet &ns);
71 
73  const exprt &expr,
74  const exprt &offset,
75  const typet &target_type,
76  const namespacet &ns);
77 
78 #endif // CPROVER_UTIL_POINTER_OFFSET_SIZE_H
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
The type of an expression, extends irept.
Definition: type.h:27
exprt build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
BigInt mp_integer
Definition: mp_arith.h:22
typet & type()
Return the type of the expression.
Definition: expr.h:68
A constant literal expression.
Definition: std_expr.h:4384
Structure type, corresponds to C style structs.
Definition: std_types.h:276
Extract member of struct or union.
Definition: std_expr.h:3890
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
exprt size_of_expr(const typet &type, const namespacet &ns)
nonstd::optional< T > optionalt
Definition: optional.h:35
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt get_subexpression_at_offset(const exprt &expr, const mp_integer &offset, const typet &target_type, const namespacet &ns)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Base class for all expressions.
Definition: expr.h:54
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
exprt member_offset_expr(const member_exprt &, const namespacet &ns)
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)