CBMC
Loading...
Searching...
No Matches
pointer_offset_size.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_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
20class exprt;
21class namespacet;
22class struct_typet;
23class typet;
24class member_exprt;
25
26std::optional<mp_integer> member_offset(
27 const struct_typet &type,
28 const irep_idt &member,
29 const namespacet &ns);
30
31std::optional<mp_integer> member_offset_bits(
32 const struct_typet &type,
33 const irep_idt &member,
34 const namespacet &ns);
35
36std::optional<mp_integer>
37pointer_offset_size(const typet &type, const namespacet &ns);
38
39std::optional<mp_integer>
40pointer_offset_bits(const typet &type, const namespacet &ns);
41
42std::optional<mp_integer>
43compute_pointer_offset(const exprt &expr, const namespacet &ns);
44
45std::optional<exprt>
47
48std::optional<exprt> member_offset_expr(
49 const struct_typet &type,
50 const irep_idt &member,
51 const namespacet &ns);
52
53std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns);
54
55std::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
61std::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:2971
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 > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
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 > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &, const namespacet &ns)
std::optional< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:17