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;
24class 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
37pointer_offset_size(const typet &type, const namespacet &ns);
38
40pointer_offset_bits(const typet &type, const namespacet &ns);
41
43compute_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
55build_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
A constant literal expression.
Definition: std_expr.h:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
Extract member of struct or union.
Definition: std_expr.h:2667
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
nonstd::optional< T > optionalt
Definition: optional.h:35
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< exprt > build_sizeof_expr(const constant_exprt &expr, 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)
BigInt mp_integer
Definition: smt_terms.h:12