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