CBMC
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 
18 #include <optional>
19 
20 class exprt;
21 class namespacet;
22 class struct_typet;
23 class typet;
24 class member_exprt;
25 
26 std::optional<mp_integer> member_offset(
27  const struct_typet &type,
28  const irep_idt &member,
29  const namespacet &ns);
30 
31 std::optional<mp_integer> member_offset_bits(
32  const struct_typet &type,
33  const irep_idt &member,
34  const namespacet &ns);
35 
36 std::optional<mp_integer>
37 pointer_offset_size(const typet &type, const namespacet &ns);
38 
39 std::optional<mp_integer>
40 pointer_offset_bits(const typet &type, const namespacet &ns);
41 
42 std::optional<mp_integer>
43 compute_pointer_offset(const exprt &expr, const namespacet &ns);
44 
45 std::optional<exprt>
46 member_offset_expr(const member_exprt &, const namespacet &ns);
47 
48 std::optional<exprt> member_offset_expr(
49  const struct_typet &type,
50  const irep_idt &member,
51  const namespacet &ns);
52 
53 std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns);
54 
55 std::optional<exprt> get_subexpression_at_offset(
56  const exprt &expr,
57  const mp_integer &offset,
58  const typet &target_type,
59  const namespacet &ns);
60 
61 std::optional<exprt> get_subexpression_at_offset(
62  const exprt &expr,
63  const exprt &offset,
64  const typet &target_type,
65  const namespacet &ns);
66 
67 #endif // CPROVER_UTIL_POINTER_OFFSET_SIZE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
Extract member of struct or union.
Definition: std_expr.h:2854
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Structure type, corresponds to C style structs.
Definition: std_types.h:231
The type of an expression, extends irept.
Definition: type.h:29
std::optional< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset, const typet &target_type, const namespacet &ns)
std::optional< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
BigInt mp_integer
Definition: smt_terms.h:17