cprover
Loading...
Searching...
No Matches
cpp_convert_type.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Conversion
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\*******************************************************************/
8
11
12#include "cpp_convert_type.h"
13
14#include <util/c_types.h>
15#include <util/config.h>
16#include <util/invariant.h>
17#include <util/std_types.h>
18
20
21#include "cpp_declaration.h"
22#include "cpp_name.h"
23
25{
26public:
27 // The following types exist in C11 and later, but are implemented as
28 // typedefs. In C++, they are keywords and thus required explicit handling in
29 // here.
31
32 void write(typet &type) override;
33
36 {
37 read(type);
38 }
39
40protected:
41 void clear() override
42 {
43 wchar_t_count = 0;
46
48 }
49
50 void read_rec(const typet &type) override;
51 void read_function_type(const typet &type);
52 void read_template(const typet &type);
53};
54
56{
57 #if 0
58 std::cout << "cpp_convert_typet::read_rec: "
59 << type.pretty() << '\n';
60 #endif
61
62 if(type.id() == ID_gcc_float80)
64 else if(type.id()==ID_wchar_t)
66 else if(type.id()==ID_char16_t)
68 else if(type.id()==ID_char32_t)
70 else if(type.id()==ID_constexpr)
72 else if(type.id()==ID_function_type)
73 {
75 }
76 else if(type.id()==ID_identifier)
77 {
78 // from parameters
79 }
80 else if(type.id()==ID_cpp_name)
81 {
82 // from typedefs
83 other.push_back(type);
84 }
85 else if(type.id()==ID_array)
86 {
87 other.push_back(type);
89 }
90 else if(type.id()==ID_template)
91 {
92 read_template(type);
93 }
94 else if(type.id()==ID_frontend_pointer)
95 {
96 // add width and turn into ID_pointer
97 pointer_typet tmp(
100 if(type.get_bool(ID_C_reference))
101 tmp.set(ID_C_reference, true);
102 if(type.get_bool(ID_C_rvalue_reference))
103 tmp.set(ID_C_rvalue_reference, true);
104 const irep_idt typedef_identifier = type.get(ID_C_typedef);
105 if(!typedef_identifier.empty())
106 tmp.set(ID_C_typedef, typedef_identifier);
107 other.push_back(tmp);
108 }
109 else if(type.id()==ID_pointer)
110 {
111 // ignore, we unfortunately convert multiple times
112 other.push_back(type);
113 }
114 else if(type.id() == ID_frontend_vector)
115 vector_size = static_cast<const exprt &>(type.find(ID_size));
116 else
117 {
119 }
120}
121
123{
124 other.push_back(type);
125 typet &t=other.back();
126
128
129 irept &arguments=t.add(ID_arguments);
130
131 for(auto &argument : arguments.get_sub())
132 {
133 exprt &decl = static_cast<exprt &>(argument);
134
135 // may be type or expression
136 bool is_type=decl.get_bool(ID_is_type);
137
138 if(is_type)
139 {
140 }
141 else
142 {
144 }
145
146 // TODO: initializer
147 }
148}
149
151{
152 other.push_back(type);
153 other.back().id(ID_code);
154
155 code_typet &t = to_code_type(other.back());
156
157 // change subtype to return_type
158 typet &return_type = t.return_type();
159
160 return_type.swap(t.subtype());
161 t.remove_subtype();
162
163 if(return_type.is_not_nil())
165
166 // take care of parameter types
167 code_typet::parameterst &parameters = t.parameters();
168
169 // see if we have an ellipsis
170 if(!parameters.empty() && parameters.back().id() == ID_ellipsis)
171 {
172 t.make_ellipsis();
173 parameters.pop_back();
174 }
175
176 for(auto &parameter_expr : parameters)
177 {
178 if(parameter_expr.id()==ID_cpp_declaration)
179 {
180 cpp_declarationt &declaration=to_cpp_declaration(parameter_expr);
181 source_locationt type_location=declaration.type().source_location();
182
184
185 // there should be only one declarator
186 assert(declaration.declarators().size()==1);
187
188 cpp_declaratort &declarator=
189 declaration.declarators().front();
190
191 // do we have a declarator?
192 if(declarator.is_nil())
193 {
194 parameter_expr = code_typet::parametert(declaration.type());
195 parameter_expr.add_source_location()=type_location;
196 }
197 else
198 {
199 const cpp_namet &cpp_name=declarator.name();
200 typet final_type=declarator.merge_type(declaration.type());
201
202 // see if it's an array type
203 if(final_type.id()==ID_array)
204 {
205 // turn into pointer type
206 final_type=pointer_type(final_type.subtype());
207 }
208
209 code_typet::parametert new_parameter(final_type);
210
211 if(cpp_name.is_nil())
212 {
213 new_parameter.add_source_location()=type_location;
214 }
215 else if(cpp_name.is_simple_name())
216 {
217 irep_idt base_name=cpp_name.get_base_name();
218 assert(!base_name.empty());
219 new_parameter.set_identifier(base_name);
220 new_parameter.set_base_name(base_name);
221 new_parameter.add_source_location()=cpp_name.source_location();
222 }
223 else
224 {
225 throw "expected simple name as parameter";
226 }
227
228 if(declarator.value().is_not_nil())
229 new_parameter.default_value().swap(declarator.value());
230
231 parameter_expr.swap(new_parameter);
232 }
233 }
234 else if(parameter_expr.id()==ID_ellipsis)
235 {
236 throw "ellipsis only allowed as last parameter";
237 }
238 else
240 }
241
242 // if we just have one parameter of type void, remove it
243 if(parameters.size() == 1 && parameters.front().type().id() == ID_empty)
244 parameters.clear();
245}
246
248{
249 if(!other.empty())
250 {
252 {
254 error() << "illegal type modifier for defined type" << eom;
255 throw 0;
256 }
257
259 }
260 else if(c_bool_cnt)
261 {
262 if(
267 {
268 throw "illegal type modifier for C++ bool";
269 }
270
272 }
273 else if(wchar_t_count)
274 {
275 // This is a distinct type, and can't be made signed/unsigned.
276 // This is tolerated by most compilers, however.
277
278 if(
282 {
283 throw "illegal type modifier for wchar_t";
284 }
285
286 type=wchar_t_type();
289 }
290 else if(char16_t_count)
291 {
292 // This is a distinct type, and can't be made signed/unsigned.
293 if(
297 {
298 throw "illegal type modifier for char16_t";
299 }
300
301 type=char16_t_type();
304 }
305 else if(char32_t_count)
306 {
307 // This is a distinct type, and can't be made signed/unsigned.
308 if(int_cnt || short_cnt || char_cnt || long_cnt ||
312 {
313 throw "illegal type modifier for char32_t";
314 }
315
316 type=char32_t_type();
319 }
320 else
321 {
323 }
324}
325
326void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
327{
328 if(
329 type.id() == ID_cpp_name || type.id() == ID_struct ||
330 type.id() == ID_union || type.id() == ID_array || type.id() == ID_code ||
331 type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
332 type.id() == ID_bool || type.id() == ID_floatbv || type.id() == ID_empty ||
333 type.id() == ID_constructor || type.id() == ID_destructor)
334 {
335 }
336 else if(type.id()==ID_c_enum)
337 {
338 // add width -- we use int, but the standard
339 // doesn't guarantee that
340 type.set(ID_width, config.ansi_c.int_width);
341 }
342 else if(type.id() == ID_c_bool)
343 {
344 type.set(ID_width, config.ansi_c.bool_width);
345 }
346 else
347 {
348 cpp_convert_typet cpp_convert_type(message_handler, type);
349 cpp_convert_type.write(type);
350 }
351}
352
354 typet &dest,
355 const typet &src,
356 message_handlert &message_handler)
357{
358 if(dest.id() != ID_merged_type && dest.has_subtype())
359 {
360 cpp_convert_auto(dest.subtype(), src, message_handler);
361 return;
362 }
363
364 cpp_convert_typet cpp_convert_type(message_handler, dest);
365 for(auto &t : cpp_convert_type.other)
366 if(t.id() == ID_auto)
367 t = src;
368
369 cpp_convert_type.write(dest);
370}
ANSI-C Language Conversion.
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:185
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
bitvector_typet wchar_t_type()
Definition: c_types.cpp:159
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:175
virtual void read_rec(const typet &type)
virtual void read(const typet &type)
virtual void write(typet &type)
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
source_locationt source_location
virtual void build_type_with_subtype(typet &type) const
Build a vector or complex type with type as subtype.
std::list< typet > other
const exprt & default_value() const
Definition: std_types.h:562
void set_base_name(const irep_idt &name)
Definition: std_types.h:585
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:580
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 make_ellipsis()
Definition: std_types.h:635
struct configt::ansi_ct ansi_c
std::size_t char32_t_count
void clear() override
void write(typet &type) override
cpp_convert_typet(message_handlert &message_handler, const typet &type)
std::size_t char16_t_count
void read_rec(const typet &type) override
std::size_t wchar_t_count
void read_template(const typet &type)
void read_function_type(const typet &type)
const declaratorst & declarators() const
typet merge_type(const typet &declaration_type) const
cpp_namet & name()
irep_idt get_base_name() const
Definition: cpp_name.cpp:16
bool is_simple_name() const
Definition: cpp_name.h:89
const source_locationt & source_location() const
Definition: cpp_name.h:73
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
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
source_locationt & add_source_location()
Definition: expr.h:235
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
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
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
message_handlert * message_handler
Definition: message.h:439
mstreamt & error() const
Definition: message.h:399
message_handlert & get_message_handler()
Definition: message.h:184
static eomt eom
Definition: message.h:297
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
source_locationt & add_source_location()
Definition: type.h:79
const source_locationt & source_location() const
Definition: type.h:74
bool has_subtype() const
Definition: type.h:66
void remove_subtype()
Definition: type.h:71
configt config
Definition: config.cpp:25
void cpp_convert_auto(typet &dest, const typet &src, message_handlert &message_handler)
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
C++ Language Conversion.
C++ Language Type Checking.
cpp_declarationt & to_cpp_declaration(irept &irep)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
std::size_t pointer_width
Definition: config.h:115
std::size_t bool_width
Definition: config.h:111
std::size_t int_width
Definition: config.h:109
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177