63 std::cout <<
"cpp_convert_typet::read: " << type.
pretty() <<
'\n';
72 std::cout <<
"cpp_convert_typet::read_rec: " 76 if(type.
id()==ID_merged_type)
81 else if(type.
id()==ID_signed)
83 else if(type.
id()==ID_unsigned)
85 else if(type.
id()==ID_volatile)
87 else if(type.
id()==ID_char)
89 else if(type.
id()==ID_int)
91 else if(type.
id()==ID_short)
93 else if(type.
id()==ID_long)
95 else if(type.
id()==ID_double)
97 else if(type.
id()==ID_float)
99 else if(type.
id()==ID_gcc_float80)
101 else if(type.
id()==ID_gcc_float128)
103 else if(type.
id()==ID_gcc_int128)
105 else if(type.
id()==ID_complex)
107 else if(type.
id()==ID_bool)
109 else if(type.
id()==ID_proper_bool)
111 else if(type.
id()==ID_wchar_t)
113 else if(type.
id()==ID_char16_t)
115 else if(type.
id()==ID_char32_t)
117 else if(type.
id()==ID_int8)
119 else if(type.
id()==ID_int16)
121 else if(type.
id()==ID_int32)
123 else if(type.
id()==ID_int64)
125 else if(type.
id()==ID_ptr32)
127 else if(type.
id()==ID_ptr64)
129 else if(type.
id()==ID_const)
131 else if(type.
id()==ID_restrict)
133 else if(type.
id()==ID_constexpr)
135 else if(type.
id()==ID_extern)
137 else if(type.
id()==ID_noreturn)
141 else if(type.
id()==ID_function_type)
145 else if(type.
id()==ID_identifier)
149 else if(type.
id()==ID_cpp_name)
152 other.push_back(type);
154 else if(type.
id()==ID_array)
156 other.push_back(type);
159 else if(type.
id()==ID_template)
163 else if(type.
id()==ID_void)
168 other.push_back(tmp);
170 else if(type.
id()==ID_frontend_pointer)
176 tmp.
set(ID_C_reference,
true);
177 if(type.
get_bool(ID_C_rvalue_reference))
178 tmp.set(ID_C_rvalue_reference,
true);
179 other.push_back(tmp);
181 else if(type.
id()==ID_pointer)
184 other.push_back(type);
188 other.push_back(type);
194 other.push_back(type);
199 irept &arguments=t.
add(ID_arguments);
206 bool is_type=decl.
get_bool(ID_is_type);
222 other.push_back(type);
228 static_cast<typet &
>(t.
add(ID_return_type));
237 irept ¶meters=t.
add(ID_parameters);
240 if(!parameters.
get_sub().empty() &&
241 parameters.
get_sub().back().id()==ID_ellipsis)
243 parameters.
set(ID_ellipsis,
true);
249 exprt ¶meter_expr=
static_cast<exprt &
>(*it);
251 if(parameter_expr.
id()==ID_cpp_declaration)
265 if(declarator.is_nil())
267 parameter_expr=
exprt(ID_parameter, declaration.
type());
272 const cpp_namet &cpp_name=declarator.name();
273 typet final_type=declarator.merge_type(declaration.
type());
276 if(final_type.
id()==ID_array)
291 assert(!base_name.
empty());
298 throw "expected simple name as parameter";
301 if(declarator.value().is_not_nil())
304 parameter_expr.
swap(new_parameter);
307 else if(parameter_expr.
id()==ID_ellipsis)
309 throw "ellipsis only allowed as last parameter";
316 if(parameters.
get_sub().size()==1 &&
317 parameters.
get_sub().front().find(ID_type).id()==ID_empty)
335 throw "type modifier not applicable";
338 throw "illegal combination of types";
352 throw "illegal type modifier for double";
368 throw "illegal type modifier for float";
371 throw "float can't be long";
384 throw "illegal type modifier for __float80";
387 throw "__float80 can't be long";
400 throw "illegal type modifier for __float128";
403 throw "__float128 can't be long";
415 throw "illegal type modifier for C++ bool";
426 throw "illegal type modifier for __CPROVER_bool";
436 throw "illegal type modifier for char";
455 throw "illegal type modifier for wchar_t";
467 throw "illegal type modifier for char16_t";
478 throw "illegal type modifier for char32_t";
487 throw "integer cannot be both signed and unsigned";
492 throw "cannot combine short and long";
502 throw "illegal type modifier for __int8";
515 throw "illegal type modifier for __int16";
526 throw "illegal type modifier for __int32";
537 throw "illegal type modifier for __int64";
548 throw "illegal type modifier for __int128";
577 throw "illegal combination of type modifiers";
582 type.
set(ID_C_constant,
true);
586 type.
set(ID_C_volatile,
true);
591 if(type.
id()==ID_cpp_name ||
592 type.
id()==ID_struct ||
593 type.
id()==ID_union ||
594 type.
id()==ID_array ||
595 type.
id()==ID_code ||
596 type.
id()==ID_unsignedbv ||
597 type.
id()==ID_signedbv ||
598 type.
id()==ID_bool ||
599 type.
id()==ID_floatbv ||
600 type.
id()==ID_empty ||
601 type.
id()==ID_symbol ||
602 type.
id()==ID_constructor ||
603 type.
id()==ID_destructor)
606 else if(type.
id()==ID_c_enum)
615 cpp_convert_type.
write(type);
628 for(
auto &t : cpp_convert_type.
other)
629 if(t.id() == ID_auto)
632 cpp_convert_type.
write(dest);
bitvector_typet gcc_float128_type()
The type of an expression.
signedbv_typet gcc_signed_int128_type()
#define forall_subtypes(it, type)
struct configt::ansi_ct ansi_c
pointer_typet pointer_type(const typet &subtype)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
unsignedbv_typet unsigned_int_type()
bitvector_typet gcc_float64x_type()
unsignedbv_typet char32_t_type()
bitvector_typet double_type()
bool is_simple_name() const
unsignedbv_typet gcc_unsigned_int128_type()
bool get_bool(const irep_namet &name) const
cpp_convert_typet(const typet &type)
void set_base_name(const irep_idt &name)
const irep_idt & id() const
const source_locationt & source_location() const
const declaratorst & declarators() const
bitvector_typet float_type()
void cpp_convert_auto(typet &dest, const typet &src)
signedbv_typet signed_long_int_type()
void read(const typet &type)
Base class for tree-like data structures with sharing.
#define Forall_irep(it, irep)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
std::size_t pointer_width
unsignedbv_typet char16_t_type()
bitvector_typet long_double_type()
const source_locationt & source_location() const
irep_idt get_base_name() const
void read_function_type(const typet &type)
signedbv_typet signed_short_int_type()
C++ Language Type Checking.
void read_template(const typet &type)
bitvector_typet wchar_t_type()
cpp_declarationt & to_cpp_declaration(irept &irep)
void set_identifier(const irep_idt &identifier)
unsignedbv_typet unsigned_short_int_type()
Base class for all expressions.
source_locationt & add_source_location()
irept & add(const irep_namet &name)
void cpp_convert_plain_type(typet &type)
source_locationt & add_source_location()
unsignedbv_typet unsigned_long_long_int_type()
void read_rec(const typet &type)
signedbv_typet signed_int_type()
unsignedbv_typet unsigned_char_type()
const typet & subtype() const
unsignedbv_typet unsigned_long_int_type()
signedbv_typet signed_long_long_int_type()
signedbv_typet signed_char_type()
bitvector_typet char_type()
const exprt & default_value() const
void set(const irep_namet &name, const irep_idt &value)