cprover
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#include "optional.h"
18
19class exprt;
20class namespacet;
21class struct_typet;
22class typet;
23class member_exprt;
24
26 const struct_typet &type,
27 const irep_idt &member,
28 const namespacet &ns);
29
31 const struct_typet &type,
32 const irep_idt &member,
33 const namespacet &ns);
34
36pointer_offset_size(const typet &type, const namespacet &ns);
37
39pointer_offset_bits(const typet &type, const namespacet &ns);
40
42compute_pointer_offset(const exprt &expr, const namespacet &ns);
43
45
47 const struct_typet &type,
48 const irep_idt &member,
49 const namespacet &ns);
50
52
54 const exprt &expr,
55 const mp_integer &offset,
56 const typet &target_type,
57 const namespacet &ns);
58
60 const exprt &expr,
61 const exprt &offset,
62 const typet &target_type,
63 const namespacet &ns);
64
65#endif // CPROVER_UTIL_POINTER_OFFSET_SIZE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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:2794
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Structure type, corresponds to C style structs.
Definition std_types.h:231
The type of an expression, extends irept.
Definition type.h:29
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset, const typet &target_type, const namespacet &ns)
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
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.
optionalt< exprt > member_offset_expr(const member_exprt &, const namespacet &ns)
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)