CBMC
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 }
const typet & return_type() const
Definition: std_types.h:689
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:16
const irep_idt & id() const
Definition: irep.h:388
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:46
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:262
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
Symbol table entry.
Definition: symbol.h:28
bool is_type
Definition: symbol.h:61
typet type
Type of symbol.
Definition: symbol.h:31
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.
Definition: std_types.cpp:145
#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 struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
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