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_struct_tag ||
83  type.id() == ID_union_tag)
84  {
85  const symbolt &symb = lookup(to_tag_type(type));
86  DATA_INVARIANT(symb.is_type, "tag symbol is a type");
87  return cpp_is_pod(symb.type);
88  }
89 
90  // everything else is POD
91  return true;
92 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
typet::subtype
const typet & subtype() const
Definition: type.h:47
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
typet
The type of an expression, extends irept.
Definition: type.h:29
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
namespacet::lookup
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
cpp_typecheckt::cpp_is_pod
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
to_tag_type
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:475
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:511
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:257
irept::id
const irep_idt & id() const
Definition: irep.h:418
cpp_typecheck.h
C++ Language Type Checking.
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:133
symbolt
Symbol table entry.
Definition: symbol.h:28
symbolt::is_type
bool is_type
Definition: symbol.h:61
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847