cprover
cpp_typecheck_type.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 "cpp_typecheck.h"
13
15#include <util/simplify_expr.h>
16#include <util/c_types.h>
17
18#include <ansi-c/c_qualifiers.h>
19
20#include "cpp_convert_type.h"
21#include "cpp_typecheck_fargs.h"
22
24{
25 assert(!type.id().empty());
26 assert(type.is_not_nil());
27
28 try
29 {
31 }
32
33 catch(const char *err)
34 {
36 error() << err << eom;
37 throw 0;
38 }
39
40 catch(const std::string &err)
41 {
43 error() << err << eom;
44 throw 0;
45 }
46
47 if(type.id()==ID_cpp_name)
48 {
49 c_qualifierst qualifiers(type);
50
51 cpp_namet cpp_name;
52 cpp_name.swap(type);
53
54 exprt symbol_expr=resolve(
55 cpp_name,
58
59 if(symbol_expr.id()!=ID_type)
60 {
62 error() << "error: expected type" << eom;
63 throw 0;
64 }
65
66 type=symbol_expr.type();
67 assert(type.is_not_nil());
68
69 if(type.get_bool(ID_C_constant))
70 qualifiers.is_constant = true;
71
72 qualifiers.write(type);
73 }
74 else if(type.id()==ID_struct ||
75 type.id()==ID_union)
76 {
78 }
79 else if(type.id()==ID_pointer)
80 {
81 c_qualifierst qualifiers(type);
82
83 // the pointer/reference might have a qualifier,
84 // but do subtype first
85 typecheck_type(type.subtype());
86
87 // Check if it is a pointer-to-member
88 if(type.find(ID_to_member).is_not_nil())
89 {
90 // these can point either to data members or member functions
91 // of a class
92
93 typet &class_object = static_cast<typet &>(type.add(ID_to_member));
94
95 if(class_object.id()==ID_cpp_name)
96 {
97 assert(class_object.get_sub().back().id()=="::");
98 class_object.get_sub().pop_back();
99 }
100
101 typecheck_type(class_object);
102
103 // there may be parameters if this is a pointer to member function
104 if(type.subtype().id()==ID_code)
105 {
106 code_typet::parameterst &parameters =
108
109 if(parameters.empty() || !parameters.front().get_this())
110 {
111 // Add 'this' to the parameters
112 code_typet::parametert a0(pointer_type(class_object));
113 a0.set_base_name(ID_this);
114 a0.set_this();
115 parameters.insert(parameters.begin(), a0);
116 }
117 }
118 }
119
120 if(type.get_bool(ID_C_constant))
121 qualifiers.is_constant = true;
122
123 qualifiers.write(type);
124 }
125 else if(type.id()==ID_array)
126 {
127 exprt &size_expr=to_array_type(type).size();
128
129 if(size_expr.is_not_nil())
130 {
131 typecheck_expr(size_expr);
132 simplify(size_expr, *this);
133 }
134
135 typecheck_type(type.subtype());
136
137 if(type.subtype().get_bool(ID_C_constant))
138 type.set(ID_C_constant, true);
139
140 if(type.subtype().get_bool(ID_C_volatile))
141 type.set(ID_C_volatile, true);
142 }
143 else if(type.id()==ID_vector)
144 {
145 // already done
146 }
147 else if(type.id() == ID_frontend_vector)
148 {
150 }
151 else if(type.id()==ID_code)
152 {
153 code_typet &code_type=to_code_type(type);
154 typecheck_type(code_type.return_type());
155
156 code_typet::parameterst &parameters=code_type.parameters();
157
158 for(auto &param : parameters)
159 {
160 typecheck_type(param.type());
161
162 // see if there is a default value
163 if(param.has_default_value())
164 {
165 typecheck_expr(param.default_value());
166 implicit_typecast(param.default_value(), param.type());
167 }
168 }
169 }
170 else if(type.id()==ID_template)
171 {
172 typecheck_type(type.subtype());
173 }
174 else if(type.id()==ID_c_enum)
175 {
177 }
178 else if(type.id()==ID_c_enum_tag)
179 {
180 }
181 else if(type.id()==ID_c_bit_field)
182 {
184 }
185 else if(
186 type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
187 type.id() == ID_bool || type.id() == ID_c_bool || type.id() == ID_floatbv ||
188 type.id() == ID_fixedbv || type.id() == ID_empty)
189 {
190 }
191 else if(type.id() == ID_struct_tag)
192 {
193 }
194 else if(type.id() == ID_union_tag)
195 {
196 }
197 else if(type.id()==ID_constructor ||
198 type.id()==ID_destructor)
199 {
200 }
201 else if(type.id()=="cpp-cast-operator")
202 {
203 }
204 else if(type.id()=="cpp-template-type")
205 {
206 }
207 else if(type.id()==ID_typeof)
208 {
209 exprt e=static_cast<const exprt &>(type.find(ID_expr_arg));
210
211 if(e.is_nil())
212 {
213 typet tmp_type=
214 static_cast<const typet &>(type.find(ID_type_arg));
215
216 if(tmp_type.id()==ID_cpp_name)
217 {
218 // this may be ambiguous -- it can be either a type or
219 // an expression
220
222
223 exprt symbol_expr=resolve(
224 to_cpp_name(static_cast<const irept &>(tmp_type)),
226 fargs);
227
228 type=symbol_expr.type();
229 }
230 else
231 {
232 typecheck_type(tmp_type);
233 type=tmp_type;
234 }
235 }
236 else
237 {
239 type=e.type();
240 }
241 }
242 else if(type.id()==ID_decltype)
243 {
244 exprt e=static_cast<const exprt &>(type.find(ID_expr_arg));
246
247 if(e.type().id() == ID_c_bit_field)
248 type = e.type().subtype();
249 else
250 type = e.type();
251 }
252 else if(type.id()==ID_unassigned)
253 {
254 // ignore, for template parameter guessing
255 }
256 else if(type.id()==ID_template_class_instance)
257 {
258 // ok (internally generated)
259 }
260 else if(type.id()==ID_block_pointer)
261 {
262 // This is an Apple extension for lambda-like constructs.
263 // http://thirdcog.eu/pwcblocks/
264 // we just treat them as references to functions
265 type.id(ID_frontend_pointer);
266 typecheck_type(type);
267 }
268 else if(type.id()==ID_nullptr)
269 {
270 }
271 else if(type.id()==ID_already_typechecked)
272 {
274 }
275 else if(type.id() == ID_gcc_attribute_mode)
276 {
278 }
279 else
280 {
282 error() << "unexpected cpp type: " << type.pretty() << eom;
283 throw 0;
284 }
285
286 assert(type.is_not_nil());
287}
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:58
const exprt & size() const
Definition: std_types.h:790
virtual void write(typet &src) const override
virtual void typecheck_vector_type(typet &type)
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
virtual void typecheck_type(typet &type)
void set_base_name(const irep_idt &name)
Definition: std_types.h:585
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:542
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
void typecheck_type(typet &) override
void typecheck_enum_type(typet &type)
void implicit_typecast(exprt &expr, const typet &type) override
void typecheck_compound_type(struct_union_typet &) override
void typecheck_expr(exprt &) override
exprt resolve(const cpp_namet &cpp_name, const cpp_typecheck_resolvet::wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
Definition: cpp_typecheck.h:83
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
bool is_not_nil() const
Definition: irep.h:380
subt & get_sub()
Definition: irep.h:456
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
irept & add(const irep_idt &name)
Definition: irep.cpp:116
bool is_nil() const
Definition: irep.h:376
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
message_handlert & get_message_handler()
Definition: message.h:184
static eomt eom
Definition: message.h:297
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
const source_locationt & source_location() const
Definition: type.h:74
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
C++ Language Conversion.
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:148
C++ Language Type Checking.
C++ Language Type Checking.
bool simplify(exprt &expr, const namespacet &ns)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214