cprover
cpp_typecheck_declaration.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 
15 
16 #include <util/pointer_expr.h>
17 
19 {
20  // see if the declaration is empty
21  if(declaration.is_empty())
22  return;
23 
24  // The function bodies must not be checked here,
25  // but only at the very end when all declarations have been
26  // processed (or considering forward declarations at least)
27 
28  // templates are done in a dedicated function
29  if(declaration.is_template())
30  convert_template_declaration(declaration);
31  else
33 }
34 
36 {
37  codet new_code(ID_decl_block);
38  new_code.reserve_operands(declaration.declarators().size());
39 
40  // unnamed object
41  std::string identifier="#anon_union"+std::to_string(anon_counter++);
42 
43  const cpp_namet cpp_name(identifier, declaration.source_location());
44  cpp_declaratort declarator;
45  declarator.name()=cpp_name;
46 
47  cpp_declarator_convertert cpp_declarator_converter(*this);
48 
49  const symbolt &symbol=
50  cpp_declarator_converter.convert(declaration, declarator);
51 
52  if(!cpp_is_pod(declaration.type()))
53  {
54  error().source_location=follow(declaration.type()).source_location();
55  error() << "anonymous union is not POD" << eom;
56  throw 0;
57  }
58 
59  new_code.add_to_operands(code_declt(cpp_symbol_expr(symbol)));
60 
61  // do scoping
62  symbolt union_symbol =
63  symbol_table.get_writeable_ref(follow(symbol.type).get(ID_name));
64 
65  for(const auto &c : to_union_type(union_symbol.type).components())
66  {
67  if(c.type().id() == ID_code)
68  {
69  error().source_location=union_symbol.type.source_location();
70  error() << "anonymous union '" << union_symbol.base_name
71  << "' shall not have function members" << eom;
72  throw 0;
73  }
74 
75  const irep_idt &base_name = c.get_base_name();
76 
77  if(cpp_scopes.current_scope().contains(base_name))
78  {
79  error().source_location=union_symbol.type.source_location();
80  error() << "identifier '" << base_name << "' already in scope" << eom;
81  throw 0;
82  }
83 
84  cpp_idt &id=cpp_scopes.current_scope().insert(base_name);
86  id.identifier = c.get_name();
87  id.class_identifier=union_symbol.name;
88  id.is_member=true;
89  }
90 
91  symbol_table.get_writeable_ref(union_symbol.name)
92  .type.set(ID_C_unnamed_object, symbol.base_name);
93 
94  return new_code;
95 }
96 
98  cpp_declarationt &declaration)
99 {
100  assert(!declaration.is_template());
101 
102  // we first check if this is a typedef
103  typet &declaration_type=declaration.type();
104  bool is_typedef=declaration.is_typedef();
105 
106  // the name anonymous tag types
107  declaration.name_anon_struct_union();
108 
109  // do the type of the declaration
110  if(declaration.declarators().empty() || !has_auto(declaration_type))
111  typecheck_type(declaration_type);
112 
113  // Elaborate any class template instance _unless_ we do a typedef.
114  // These are only elaborated on usage!
115  if(!is_typedef)
116  elaborate_class_template(declaration_type);
117 
118  // mark as 'already typechecked'
119  if(!declaration.declarators().empty())
121 
122  // Special treatment for anonymous unions
123  if(declaration.declarators().empty() &&
124  follow(declaration.type()).get_bool(ID_C_is_anonymous))
125  {
126  typet final_type=follow(declaration.type());
127 
128  if(final_type.id()!=ID_union)
129  {
130  error().source_location=final_type.source_location();
131  error() << "top-level declaration does not declare anything"
132  << eom;
133  throw 0;
134  }
135 
136  convert_anonymous_union(declaration);
137  }
138 
139  // do the declarators (optional)
140  for(auto &d : declaration.declarators())
141  {
142  // copy the declarator (we destroy the original)
143  cpp_declaratort declarator=d;
144 
145  cpp_declarator_convertert cpp_declarator_converter(*this);
146 
147  cpp_declarator_converter.is_typedef=is_typedef;
148 
149  symbolt &symbol=cpp_declarator_converter.convert(
150  declaration_type, declaration.storage_spec(),
151  declaration.member_spec(), declarator);
152 
153  if(!symbol.is_type && !symbol.is_extern && symbol.type.id() == ID_empty)
154  {
155  error().source_location = symbol.location;
156  error() << "void-typed symbol not permitted" << eom;
157  throw 0;
158  }
159 
160  // any template instance to remember?
161  if(declaration.find(ID_C_template).is_not_nil())
162  {
163  symbol.type.set(ID_C_template, declaration.find(ID_C_template));
164  symbol.type.set(
165  ID_C_template_arguments,
166  declaration.find(ID_C_template_arguments));
167  }
168 
169  // replace declarator by symbol expression
170  exprt tmp=cpp_symbol_expr(symbol);
171  d.swap(tmp);
172 
173  // is there a constructor to be called for the declarator?
174  if(symbol.is_lvalue &&
175  declarator.init_args().has_operands())
176  {
177  auto constructor = cpp_constructor(
178  symbol.location,
179  cpp_symbol_expr(symbol),
180  declarator.init_args().operands());
181 
182  if(constructor.has_value())
183  symbol.value = constructor.value();
184  else
185  symbol.value = nil_exprt();
186  }
187  }
188 }
static void make_already_typechecked(typet &type)
symbol_tablet & symbol_table
A codet representing the declaration of a local variable.
Definition: std_code.h:402
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
const declaratorst & declarators() const
bool is_template() const
const cpp_storage_spect & storage_spec() const
const cpp_member_spect & member_spec() const
bool is_empty() const
bool is_typedef() const
void name_anon_struct_union()
symbolt & convert(const typet &type, const cpp_storage_spect &storage_spec, const cpp_member_spect &member_spec, cpp_declaratort &declarator)
cpp_namet & name()
exprt & init_args()
Definition: cpp_id.h:28
id_classt id_class
Definition: cpp_id.h:50
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
cpp_idt & insert(const irep_idt &_base_name)
Definition: cpp_scope.h:52
bool contains(const irep_idt &base_name_to_lookup)
Definition: cpp_scope.cpp:203
void typecheck_type(typet &) override
void convert_template_declaration(cpp_declarationt &declaration)
void convert_non_template_declaration(cpp_declarationt &declaration)
unsigned anon_counter
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
void convert(cpp_linkage_spect &)
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
void elaborate_class_template(const typet &type)
elaborate class template instances
static bool has_auto(const typet &type)
codet convert_anonymous_union(cpp_declarationt &declaration)
cpp_scopest cpp_scopes
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
const source_locationt & source_location() const
Definition: expr.h:234
void reserve_operands(operandst::size_type n)
Definition: expr.h:128
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:140
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
The NIL expression.
Definition: std_expr.h:2735
const componentst & components() const
Definition: std_types.h:142
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_extern
Definition: symbol.h:66
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
The type of an expression, extends irept.
Definition: type.h:28
const source_locationt & source_location() const
Definition: type.h:71
C++ Language Type Checking.
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition: cpp_util.cpp:14
API to expression classes for Pointers.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:430
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.