cprover
Loading...
Searching...
No Matches
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 error().source_location=follow(declaration.type()).source_location();
56 error() << "anonymous union is not POD" << eom;
57 throw 0;
58 }
59
61
62 // do scoping
65
66 for(const auto &c : to_union_type(union_symbol.type).components())
67 {
68 if(c.type().id() == ID_code)
69 {
70 error().source_location=union_symbol.type.source_location();
71 error() << "anonymous union '" << union_symbol.base_name
72 << "' shall not have function members" << eom;
73 throw 0;
74 }
75
76 const irep_idt &base_name = c.get_base_name();
77
78 if(cpp_scopes.current_scope().contains(base_name))
79 {
80 error().source_location=union_symbol.type.source_location();
81 error() << "identifier '" << base_name << "' already in scope" << eom;
82 throw 0;
83 }
84
85 cpp_idt &id=cpp_scopes.current_scope().insert(base_name);
87 id.identifier = c.get_name();
88 id.class_identifier=union_symbol.name;
89 id.is_member=true;
90 }
91
93
94 return new_code;
95}
96
98 cpp_declarationt &declaration)
99{
100 PRECONDITION(!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))
112
113 // Elaborate any class template instance _unless_ we do a typedef.
114 // These are only elaborated on usage!
115 if(!is_typedef)
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 {
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
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(
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}
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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
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:39
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:150
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:223
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:162
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
const irep_idt & id() const
Definition irep.h:396
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:49
The NIL expression.
Definition std_expr.h:3026
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
Author: Diffblue Ltd.