cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
cpp_is_pod.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: C++ Language Type Checking
4
5
Author: Daniel Kroening, kroening@cs.cmu.edu
6
7
\*******************************************************************/
8
11
12
#include "
cpp_typecheck.h
"
13
14
#include <
util/pointer_expr.h
>
15
16
bool
cpp_typecheckt::cpp_is_pod
(
const
typet
&type)
const
17
{
18
if
(type.
id
()==ID_struct)
19
{
20
// Not allowed in PODs:
21
// * Non-PODs
22
// * Constructors/Destructors
23
// * virtuals
24
// * private/protected, unless static
25
// * overloading assignment operator
26
// * Base classes
27
28
const
struct_typet
&struct_type=
to_struct_type
(type);
29
30
if
(!struct_type.
bases
().empty())
31
return
false
;
32
33
const
struct_typet::componentst
&components=
34
struct_type.
components
();
35
36
for
(
const
auto
&c : components)
37
{
38
if
(c.get_bool(ID_is_type))
39
continue
;
40
41
if
(c.get_base_name() ==
"operator="
)
42
return
false
;
43
44
if
(c.get_bool(ID_is_virtual))
45
return
false
;
46
47
const
typet
&sub_type = c.type();
48
49
if
(sub_type.
id
()==ID_code)
50
{
51
if
(c.get_bool(ID_is_virtual))
52
return
false
;
53
54
const
typet
&comp_return_type =
to_code_type
(sub_type).
return_type
();
55
56
if
(
57
comp_return_type.
id
() == ID_constructor ||
58
comp_return_type.
id
() == ID_destructor)
59
{
60
return
false
;
61
}
62
}
63
else
if
(c.get(ID_access) != ID_public && !c.get_bool(ID_is_static))
64
return
false
;
65
66
if
(!
cpp_is_pod
(sub_type))
67
return
false
;
68
}
69
70
return
true
;
71
}
72
else
if
(type.
id
()==ID_array)
73
{
74
return
cpp_is_pod
(
to_array_type
(type).element_type());
75
}
76
else
if
(type.
id
()==ID_pointer)
77
{
78
if
(
is_reference
(type))
// references are not PODs
79
return
false
;
80
81
// but pointers are PODs!
82
return
true
;
83
}
84
else
if
(type.
id
() == ID_struct_tag ||
85
type.
id
() == ID_union_tag)
86
{
87
const
symbolt
&symb =
lookup
(
to_tag_type
(type));
88
DATA_INVARIANT
(symb.
is_type
,
"tag symbol is a type"
);
89
return
cpp_is_pod
(symb.
type
);
90
}
91
92
// everything else is POD
93
return
true
;
94
}
code_typet::return_type
const typet & return_type() const
Definition
std_types.h:689
cpp_typecheckt::cpp_is_pod
bool cpp_is_pod(const typet &type) const
Definition
cpp_is_pod.cpp:16
irept::id
const irep_idt & id() const
Definition
irep.h:388
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition
namespace.cpp:134
struct_typet
Structure type, corresponds to C style structs.
Definition
std_types.h:231
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition
std_types.h:262
struct_union_typet::components
const componentst & components() const
Definition
std_types.h:147
struct_union_typet::componentst
std::vector< componentt > componentst
Definition
std_types.h:140
symbolt
Symbol table entry.
Definition
symbol.h:28
symbolt::is_type
bool is_type
Definition
symbol.h:61
symbolt::type
typet type
Type of symbol.
Definition
symbol.h:31
typet
The type of an expression, extends irept.
Definition
type.h:29
cpp_typecheck.h
C++ Language Type Checking.
pointer_expr.h
API to expression classes for Pointers.
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition
std_types.cpp:145
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition
invariant.h:534
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition
std_types.h:788
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition
std_types.h:308
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition
std_types.h:888
to_tag_type
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition
std_types.h:434
cpp
cpp_is_pod.cpp
Generated by
1.17.0