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 
27  const struct_typet &type,
28  const irep_idt &member,
29  const namespacet &ns);
30 
32  const struct_typet &type,
33  const irep_idt &member,
34  const namespacet &ns);
35 
37 pointer_offset_size(const typet &type, const namespacet &ns);
38 
40 pointer_offset_bits(const typet &type, const namespacet &ns);
41 
43 compute_pointer_offset(const exprt &expr, const namespacet &ns);
44 
46 
48  const struct_typet &type,
49  const irep_idt &member,
50  const namespacet &ns);
51 
53 
55 build_sizeof_expr(const constant_exprt &expr, const namespacet &ns);
56 
58  const exprt &expr,
59  const mp_integer &offset,
60  const typet &target_type,
61  const namespacet &ns);
62 
64  const exprt &expr,
65  const exprt &offset,
66  const typet &target_type,
67  const namespacet &ns);
68 
69 #endif // CPROVER_UTIL_POINTER_OFFSET_SIZE_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
mp_arith.h
typet
The type of an expression, extends irept.
Definition: type.h:29
compute_pointer_offset
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:507
optional.h
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
exprt
Base class for all expressions.
Definition: expr.h:53
member_offset_bits
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:64
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
build_sizeof_expr
optionalt< exprt > build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:569
get_subexpression_at_offset
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset, const typet &target_type, const namespacet &ns)
Definition: pointer_offset_size.cpp:612
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
pointer_offset_size
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.
Definition: pointer_offset_size.cpp:89
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:23
member_offset_expr
optionalt< exprt > member_offset_expr(const member_exprt &, const namespacet &ns)
Definition: pointer_offset_size.cpp:226
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
irep.h