54 std::cout <<
"cpp_convert_typet::read_rec: "
58 if(type.
id() == ID_gcc_float80)
60 else if(type.
id()==ID_wchar_t)
62 else if(type.
id()==ID_char16_t)
64 else if(type.
id()==ID_char32_t)
66 else if(type.
id()==ID_constexpr)
68 else if(type.
id()==ID_function_type)
72 else if(type.
id()==ID_identifier)
76 else if(type.
id()==ID_cpp_name)
79 other.push_back(type);
81 else if(type.
id()==ID_array)
83 other.push_back(type);
87 else if(type.
id()==ID_template)
91 else if(type.
id()==ID_frontend_pointer)
98 tmp.
set(ID_C_reference,
true);
99 if(type.
get_bool(ID_C_rvalue_reference))
100 tmp.
set(ID_C_rvalue_reference,
true);
101 const irep_idt typedef_identifier = type.
get(ID_C_typedef);
102 if(!typedef_identifier.
empty())
103 tmp.
set(ID_C_typedef, typedef_identifier);
104 other.push_back(tmp);
106 else if(type.
id()==ID_pointer)
109 other.push_back(type);
111 else if(type.
id() == ID_frontend_vector)
121 other.push_back(type);
126 irept &arguments=t.
add(ID_arguments);
128 for(
auto &argument : arguments.
get_sub())
133 bool is_type=decl.
get_bool(ID_is_type);
149 other.push_back(type);
150 other.back().id(ID_code);
167 if(!parameters.empty() && parameters.back().id() == ID_ellipsis)
170 parameters.pop_back();
173 for(
auto ¶meter_expr : parameters)
175 if(parameter_expr.id()==ID_cpp_declaration)
184 "there should be only one declarator");
193 parameter_expr.add_source_location()=type_location;
201 if(final_type.
id()==ID_array)
223 throw "expected simple name as parameter";
229 parameter_expr.swap(new_parameter);
232 else if(parameter_expr.id()==ID_ellipsis)
234 throw "ellipsis only allowed as last parameter";
241 if(parameters.size() == 1 && parameters.front().type().id() == ID_empty)
267 throw "illegal type modifier for C++ bool";
282 throw "illegal type modifier for wchar_t";
297 throw "illegal type modifier for char16_t";
312 throw "illegal type modifier for char32_t";
328 type.
id() == ID_cpp_name || type.
id() == ID_struct ||
329 type.
id() == ID_union || type.
id() == ID_array || type.
id() == ID_code ||
330 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
331 type.
id() == ID_bool || type.
id() == ID_floatbv || type.
id() == ID_empty ||
332 type.
id() == ID_constructor || type.
id() == ID_destructor ||
333 type.
id() == ID_c_enum)
336 else if(type.
id() == ID_c_bool)
343 cpp_convert_type.
write(type);
360 for(
auto &t : cpp_convert_type.
other)
361 if(t.id() == ID_auto)
364 cpp_convert_type.
write(dest);
ANSI-C Language Conversion.
unsignedbv_typet char32_t_type()
pointer_typet pointer_type(const typet &subtype)
bitvector_typet wchar_t_type()
unsignedbv_typet char16_t_type()
virtual void read_rec(const typet &type)
virtual void write(typet &type)
message_handlert & message_handler
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
unsigned gcc_float64x_cnt
source_locationt source_location
virtual void build_type_with_subtype(typet &type) const
Build a vector or complex type with type as subtype.
c_qualifierst c_qualifiers
const typet & element_type() const
The type of the elements of the array.
const exprt & default_value() const
void set_base_name(const irep_idt &name)
void set_identifier(const irep_idt &identifier)
std::vector< parametert > parameterst
const typet & return_type() const
const parameterst & parameters() const
struct configt::ansi_ct ansi_c
std::size_t char32_t_count
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
irep_idt get_base_name() const
const source_locationt & source_location() const
bool is_simple_name() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
source_locationt & add_source_location()
typet & type()
Return the type of the expression.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool get_bool(const irep_idt &name) const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
irept & add(const irep_idt &name)
Class that provides messages with a built-in verbosity 'level'.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
The type of an expression, extends irept.
const source_locationt & source_location() const
source_locationt & add_source_location()
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 Type Checking.
cpp_declarationt & to_cpp_declaration(irept &irep)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
std::size_t pointer_width
const type_with_subtypet & to_type_with_subtype(const typet &type)