CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_is_pod.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\*******************************************************************/
8
11
12#include "cpp_typecheck.h"
13
14#include <util/pointer_expr.h>
15
16bool 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
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(
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
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
bool cpp_is_pod(const typet &type) const
const irep_idt & id() const
Definition irep.h:388
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Structure type, corresponds to C style structs.
Definition std_types.h:231
std::vector< componentt > componentst
Definition std_types.h:140
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
C++ Language Type Checking.
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition std_types.h:434