cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
exprt
Base class for all expressions.
Definition
expr.h:57
exprt::type
typet & type()
Return the type of the expression.
Definition
expr.h:85
member_exprt
Extract member of struct or union.
Definition
std_expr.h:2856
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
struct_typet
Structure type, corresponds to C style structs.
Definition
std_types.h:231
typet
The type of an expression, extends irept.
Definition
type.h:29
irep.h
mp_arith.h
pointer_offset_size
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.
Definition
pointer_offset_size.cpp:91
get_subexpression_at_offset
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset, const typet &target_type, const namespacet &ns)
Definition
pointer_offset_size.cpp:565
pointer_offset_bits
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition
pointer_offset_size.cpp:102
member_offset_bits
std::optional< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition
pointer_offset_size.cpp:66
member_offset_expr
std::optional< exprt > member_offset_expr(const member_exprt &, const namespacet &ns)
Definition
pointer_offset_size.cpp:222
compute_pointer_offset
std::optional< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
Definition
pointer_offset_size.cpp:501
size_of_expr
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition
pointer_offset_size.cpp:287
member_offset
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition
pointer_offset_size.cpp:25
mp_integer
BigInt mp_integer
Definition
smt_terms.h:17
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
util
pointer_offset_size.h
Generated by
1.17.0