cprover
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 bool cpp_typecheckt::cpp_is_pod(const typet &type) const
15 {
16  if(type.id()==ID_struct)
17  {
18  // Not allowed in PODs:
19  // * Non-PODs
20  // * Constructors/Destructors
21  // * virtuals
22  // * private/protected, unless static
23  // * overloading assignment operator
24  // * Base classes
25 
26  const struct_typet &struct_type=to_struct_type(type);
27 
28  if(!struct_type.bases().empty())
29  return false;
30 
31  const struct_typet::componentst &components=
32  struct_type.components();
33 
34  for(const auto &c : components)
35  {
36  if(c.get_bool(ID_is_type))
37  continue;
38 
39  if(c.get_base_name() == "operator=")
40  return false;
41 
42  if(c.get_bool(ID_is_virtual))
43  return false;
44 
45  const typet &sub_type = c.type();
46 
47  if(sub_type.id()==ID_code)
48  {
49  if(c.get_bool(ID_is_virtual))
50  return false;
51 
52  const typet &comp_return_type = to_code_type(sub_type).return_type();
53 
54  if(
55  comp_return_type.id() == ID_constructor ||
56  comp_return_type.id() == ID_destructor)
57  {
58  return false;
59  }
60  }
61  else if(c.get(ID_access) != ID_public && !c.get_bool(ID_is_static))
62  return false;
63 
64  if(!cpp_is_pod(sub_type))
65  return false;
66  }
67 
68  return true;
69  }
70  else if(type.id()==ID_array)
71  {
72  return cpp_is_pod(type.subtype());
73  }
74  else if(type.id()==ID_pointer)
75  {
76  if(is_reference(type)) // references are not PODs
77  return false;
78 
79  // but pointers are PODs!
80  return true;
81  }
82  else if(type.id() == ID_symbol_type)
83  {
84  const symbolt &symb = lookup(to_symbol_type(type));
85  DATA_INVARIANT(symb.is_type, "type symbol is a type");
86  return cpp_is_pod(symb.type);
87  }
88  else if(type.id() == ID_struct_tag ||
89  type.id() == ID_union_tag)
90  {
91  const symbolt &symb = lookup(to_tag_type(type));
92  DATA_INVARIANT(symb.is_type, "tag symbol is a type");
93  return cpp_is_pod(symb.type);
94  }
95 
96  // everything else is POD
97  return true;
98 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
typet::subtype
const typet & subtype() const
Definition: type.h:38
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
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:485
typet
The type of an expression, extends irept.
Definition: type.h:27
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:203
cpp_typecheckt::cpp_is_pod
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
to_tag_type
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:503
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:303
irept::id
const irep_idt & id() const
Definition: irep.h:259
cpp_typecheck.h
to_symbol_type
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
Definition: std_types.h:98
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:132
symbolt
Symbol table entry.
Definition: symbol.h:27
symbolt::is_type
bool is_type
Definition: symbol.h:61
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:883