CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_typecheck_declaration.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\********************************************************************/
8
11
12#include <util/c_types.h>
14
16#include "cpp_typecheck.h"
17#include "cpp_util.h"
18
20{
21 // see if the declaration is empty
22 if(declaration.is_empty())
23 return;
24
25 // The function bodies must not be checked here,
26 // but only at the very end when all declarations have been
27 // processed (or considering forward declarations at least)
28
29 // templates are done in a dedicated function
30 if(declaration.is_template())
32 else
34}
35
37{
38 codet new_code(ID_decl_block);
39 new_code.reserve_operands(declaration.declarators().size());
40
41 // unnamed object
42 std::string identifier="#anon_union"+std::to_string(anon_counter++);
43
44 const cpp_namet cpp_name(identifier, declaration.source_location());
45 cpp_declaratort declarator;
46 declarator.name()=cpp_name;
47
49
50 const symbolt &symbol=
51 cpp_declarator_converter.convert(declaration, declarator);
52
53 if(!cpp_is_pod(declaration.type()))
54 {
55 const typet &followed =
56 declaration.type().id() == ID_struct_tag
57 ? static_cast<const typet &>(
58 follow_tag(to_struct_tag_type(declaration.type())))
59 : declaration.type().id() == ID_union_tag
60 ? static_cast<const typet &>(
61 follow_tag(to_union_tag_type(declaration.type())))
62 : declaration.type().id() == ID_c_enum_tag
63 ? static_cast<const typet &>(
64 follow_tag(to_c_enum_tag_type(declaration.type())))
65 : declaration.type();
66 error().source_location = followed.source_location();
67 error() << "anonymous union is not POD" << eom;
68 throw 0;
69 }
70
72
73 // do scoping
76
77 for(const auto &c : to_union_type(union_symbol.type).components())
78 {
79 if(c.type().id() == ID_code)
80 {
81 error().source_location=union_symbol.type.source_location();
82 error() << "anonymous union '" << union_symbol.base_name
83 << "' shall not have function members" << eom;
84 throw 0;
85 }
86
87 const irep_idt &base_name = c.get_base_name();
88
89 if(cpp_scopes.current_scope().contains(base_name))
90 {
91 error().source_location=union_symbol.type.source_location();
92 error() << "identifier '" << base_name << "' already in scope" << eom;
93 throw 0;
94 }
95
96 cpp_idt &id=cpp_scopes.current_scope().insert(base_name);
98 id.identifier = c.get_name();
99 id.class_identifier=union_symbol.name;
100 id.is_member=true;
101 }
102
104
105 return new_code;
106}
107
109 cpp_declarationt &declaration)
110{
111 PRECONDITION(!declaration.is_template());
112
113 // we first check if this is a typedef
114 typet &declaration_type=declaration.type();
115 bool is_typedef=declaration.is_typedef();
116
117 // the name anonymous tag types
118 declaration.name_anon_struct_union();
119
120 // do the type of the declaration
121 if(declaration.declarators().empty() || !has_auto(declaration_type))
123
124 // Elaborate any class template instance _unless_ we do a typedef.
125 // These are only elaborated on usage!
126 if(!is_typedef)
128
129 // mark as 'already typechecked'
130 if(!declaration.declarators().empty())
132
133 // Special treatment for anonymous unions
134 if(
135 declaration.declarators().empty() &&
136 ((declaration.type().id() == ID_struct_tag &&
137 follow_tag(to_struct_tag_type(declaration.type()))
138 .get_bool(ID_C_is_anonymous)) ||
139 (declaration.type().id() == ID_union_tag &&
140 follow_tag(to_union_tag_type(declaration.type()))
141 .get_bool(ID_C_is_anonymous)) ||
142 declaration.type().get_bool(ID_C_is_anonymous)))
143 {
144 if(declaration.type().id() != ID_union_tag)
145 {
146 error().source_location = declaration.type().source_location();
147 error() << "top-level declaration does not declare anything"
148 << eom;
149 throw 0;
150 }
151
152 convert_anonymous_union(declaration);
153 }
154
155 // do the declarators (optional)
156 for(auto &d : declaration.declarators())
157 {
158 // copy the declarator (we destroy the original)
159 cpp_declaratort declarator=d;
160
162
163 cpp_declarator_converter.is_typedef=is_typedef;
164
165 symbolt &symbol=cpp_declarator_converter.convert(
166 declaration_type, declaration.storage_spec(),
167 declaration.member_spec(), declarator);
168
169 if(!symbol.is_type && !symbol.is_extern && symbol.type.id() == ID_empty)
170 {
171 error().source_location = symbol.location;
172 error() << "void-typed symbol not permitted" << eom;
173 throw 0;
174 }
175
176 // any template instance to remember?
177 if(declaration.find(ID_C_template).is_not_nil())
178 {
179 symbol.type.set(ID_C_template, declaration.find(ID_C_template));
180 symbol.type.set(
182 declaration.find(ID_C_template_arguments));
183 }
184
185 // replace declarator by symbol expression
186 exprt tmp=cpp_symbol_expr(symbol);
187 d.swap(tmp);
188
189 // is there a constructor to be called for the declarator?
190 if(symbol.is_lvalue &&
191 declarator.init_args().has_operands())
192 {
193 auto constructor = cpp_constructor(
194 symbol.location,
195 cpp_symbol_expr(symbol),
196 declarator.init_args().operands());
197
198 if(constructor.has_value())
199 symbol.value = constructor.value();
200 else
201 symbol.value = nil_exprt();
202 }
203 }
204}
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition c_types.h:377
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
static void make_already_typechecked(typet &type)
symbol_table_baset & symbol_table
A codet representing the declaration of a local variable.
Definition std_code.h:347
Data structure for representing an arbitrary statement in a program.
const declaratorst & declarators() const
const cpp_member_spect & member_spec() const
const cpp_storage_spect & storage_spec() const
bool is_template() const
bool is_empty() const
bool is_typedef() const
cpp_namet & name()
exprt & init_args()
id_classt id_class
Definition cpp_id.h:45
cpp_scopet & current_scope()
Definition cpp_scopes.h:32
cpp_idt & insert(const irep_idt &_base_name)
Definition cpp_scope.h:52
bool contains(const irep_idt &base_name_to_lookup)
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
std::optional< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
void convert(cpp_linkage_spect &)
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:38
Base class for all expressions.
Definition expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:91
void reserve_operands(operandst::size_type n)
Definition expr.h:158
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
const irep_idt & id() const
Definition irep.h:388
source_locationt source_location
Definition message.h:239
mstreamt & error() const
Definition message.h:391
static eomt eom
Definition message.h:289
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
The NIL expression.
Definition std_expr.h:3208
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
bool is_extern
Definition symbol.h:74
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 irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
bool is_lvalue
Definition symbol.h:72
exprt value
Initial value of symbol.
Definition symbol.h:34
The type of an expression, extends irept.
Definition type.h:29
const source_locationt & source_location() const
Definition type.h:72
C++ Language Type Checking.
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition cpp_util.cpp:14
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
Author: Diffblue Ltd.