diff --git a/regression/ansi-c/always_inline5/test.desc b/regression/ansi-c/always_inline5/test.desc index 307a7ac801e..da401175efb 100644 --- a/regression/ansi-c/always_inline5/test.desc +++ b/regression/ansi-c/always_inline5/test.desc @@ -1,4 +1,4 @@ -CORE gcc-only broken-test-c++-front-end +CORE gcc-only test-c++-front-end main.c ^EXIT=0$ diff --git a/regression/ansi-c/builtin_ia32_undef/test.desc b/regression/ansi-c/builtin_ia32_undef/test.desc index ebddf7de15d..8f670e76f73 100644 --- a/regression/ansi-c/builtin_ia32_undef/test.desc +++ b/regression/ansi-c/builtin_ia32_undef/test.desc @@ -1,4 +1,4 @@ -CORE test-c++-front-end +CORE broken-test-c++-front-end main.c ^EXIT=0$ diff --git a/regression/ansi-c/gcc_attributes3/test.desc b/regression/ansi-c/gcc_attributes3/test.desc index 307a7ac801e..da401175efb 100644 --- a/regression/ansi-c/gcc_attributes3/test.desc +++ b/regression/ansi-c/gcc_attributes3/test.desc @@ -1,4 +1,4 @@ -CORE gcc-only broken-test-c++-front-end +CORE gcc-only test-c++-front-end main.c ^EXIT=0$ diff --git a/regression/cpp/CMakeLists.txt b/regression/cpp/CMakeLists.txt index bc92a35412f..0ad5e5ec889 100644 --- a/regression/cpp/CMakeLists.txt +++ b/regression/cpp/CMakeLists.txt @@ -1,3 +1,9 @@ +if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") +add_test_pl_tests( + "$" -X gcc-only +) +else() add_test_pl_tests( "$" ) +endif() diff --git a/regression/cpp/Makefile b/regression/cpp/Makefile index d341a665f6f..0edd426dd35 100644 --- a/regression/cpp/Makefile +++ b/regression/cpp/Makefile @@ -4,7 +4,7 @@ include ../../src/config.inc include ../../src/common ifeq ($(BUILD_ENV_),MSVC) - exe=../../../src/goto-cc/goto-cl + exe=../../../src/goto-cc/goto-cl -X gcc-only else exe=../../../src/goto-cc/goto-cc endif diff --git a/regression/cpp/gcc_attributes1/main.cpp b/regression/cpp/gcc_attributes1/main.cpp new file mode 100644 index 00000000000..6d7d6a83ce4 --- /dev/null +++ b/regression/cpp/gcc_attributes1/main.cpp @@ -0,0 +1,12 @@ +#ifdef __GNUC__ +const char *__attribute__((weak)) bar(); +#endif + +int main() +{ +#ifdef __GNUC__ + return bar() != 0; +#else + return 0 +#endif +} diff --git a/regression/cpp/gcc_attributes1/test.desc b/regression/cpp/gcc_attributes1/test.desc new file mode 100644 index 00000000000..64abef45f39 --- /dev/null +++ b/regression/cpp/gcc_attributes1/test.desc @@ -0,0 +1,8 @@ +CORE gcc-only +main.cpp + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 63da1ef5251..05a5bc5f76e 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -589,6 +589,13 @@ void ansi_c_convert_typet::write(typet &type) } } + build_type_with_subtype(type); + set_attributes(type); +} + +/// Build a vector or complex type with \p type as subtype. +void ansi_c_convert_typet::build_type_with_subtype(typet &type) const +{ if(vector_size.is_not_nil()) { type_with_subtypet new_type(ID_frontend_vector, type); @@ -604,7 +611,11 @@ void ansi_c_convert_typet::write(typet &type) new_type.add_source_location()=source_location; type.swap(new_type); } +} +/// Add qualifiers and GCC attributes onto \p type. +void ansi_c_convert_typet::set_attributes(typet &type) const +{ if(gcc_attribute_mode.is_not_nil()) { typet new_type=gcc_attribute_mode; diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h index fdd6f26697e..4910d5b8b61 100644 --- a/src/ansi-c/ansi_c_convert_type.h +++ b/src/ansi-c/ansi_c_convert_type.h @@ -51,8 +51,8 @@ class ansi_c_convert_typet:public messaget // qualifiers c_qualifierst c_qualifiers; - void read(const typet &type); - void write(typet &type); + virtual void read(const typet &type); + virtual void write(typet &type); source_locationt source_location; @@ -64,7 +64,7 @@ class ansi_c_convert_typet:public messaget { } - void clear() + virtual void clear() { unsigned_cnt=signed_cnt=char_cnt=int_cnt=short_cnt= long_cnt=double_cnt=float_cnt=c_bool_cnt=proper_bool_cnt=complex_cnt= @@ -90,7 +90,9 @@ class ansi_c_convert_typet:public messaget } protected: - void read_rec(const typet &type); + virtual void read_rec(const typet &type); + virtual void build_type_with_subtype(typet &type) const; + virtual void set_attributes(typet &type) const; }; #endif // CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index ee70524ff15..906279bd83e 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -19,53 +19,43 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include +#include #include #include "cpp_declaration.h" #include "cpp_name.h" -class cpp_convert_typet +class cpp_convert_typet : public ansi_c_convert_typet { public: - unsigned unsigned_cnt, signed_cnt, char_cnt, int_cnt, short_cnt, - long_cnt, const_cnt, restrict_cnt, constexpr_cnt, volatile_cnt, - double_cnt, float_cnt, complex_cnt, cpp_bool_cnt, proper_bool_cnt, - extern_cnt, noreturn_cnt, wchar_t_cnt, char16_t_cnt, char32_t_cnt, - int8_cnt, int16_cnt, int32_cnt, int64_cnt, ptr32_cnt, ptr64_cnt, - float80_cnt, float128_cnt, int128_cnt; + // The following types exist in C11 and later, but are implemented as + // typedefs. In C++, they are keywords and thus required explicit handling in + // here. + std::size_t wchar_t_count, char16_t_count, char32_t_count; - void read(const typet &type); - void write(typet &type); + void write(typet &type) override; - std::list other; - - cpp_convert_typet() { } - explicit cpp_convert_typet(const typet &type) { read(type); } + cpp_convert_typet(message_handlert &message_handler, const typet &type) + : ansi_c_convert_typet(message_handler) + { + read(type); + } protected: - void read_rec(const typet &type); + void clear() override + { + wchar_t_count = 0; + char16_t_count = 0; + char32_t_count = 0; + + ansi_c_convert_typet::clear(); + } + + void read_rec(const typet &type) override; void read_function_type(const typet &type); void read_template(const typet &type); }; -void cpp_convert_typet::read(const typet &type) -{ - unsigned_cnt=signed_cnt=char_cnt=int_cnt=short_cnt= - long_cnt=const_cnt=restrict_cnt=constexpr_cnt=volatile_cnt= - double_cnt=float_cnt=complex_cnt=cpp_bool_cnt=proper_bool_cnt= - extern_cnt=noreturn_cnt=wchar_t_cnt=char16_t_cnt=char32_t_cnt= - int8_cnt=int16_cnt=int32_cnt=int64_cnt= - ptr32_cnt=ptr64_cnt=float80_cnt=float128_cnt=int128_cnt=0; - - other.clear(); - - #if 0 - std::cout << "cpp_convert_typet::read: " << type.pretty() << '\n'; - #endif - - read_rec(type); -} - void cpp_convert_typet::read_rec(const typet &type) { #if 0 @@ -73,71 +63,16 @@ void cpp_convert_typet::read_rec(const typet &type) << type.pretty() << '\n'; #endif - if(type.id()==ID_merged_type) - { - forall_subtypes(it, type) - read_rec(*it); - } - else if(type.id()==ID_signed) - signed_cnt++; - else if(type.id()==ID_unsigned) - unsigned_cnt++; - else if(type.id()==ID_volatile) - volatile_cnt++; - else if(type.id()==ID_char) - char_cnt++; - else if(type.id()==ID_int) - int_cnt++; - else if(type.id()==ID_short) - short_cnt++; - else if(type.id()==ID_long) - long_cnt++; - else if(type.id()==ID_double) - double_cnt++; - else if(type.id()==ID_float) - float_cnt++; - else if(type.id()==ID_gcc_float80) - float80_cnt++; - else if(type.id()==ID_gcc_float128) - float128_cnt++; - else if(type.id()==ID_gcc_int128) - int128_cnt++; - else if(type.id()==ID_complex) - complex_cnt++; - else if(type.id() == ID_c_bool) - cpp_bool_cnt++; - else if(type.id()==ID_proper_bool) - proper_bool_cnt++; + if(type.id() == ID_gcc_float80) + ++gcc_float64x_cnt; else if(type.id()==ID_wchar_t) - wchar_t_cnt++; + ++wchar_t_count; else if(type.id()==ID_char16_t) - char16_t_cnt++; + ++char16_t_count; else if(type.id()==ID_char32_t) - char32_t_cnt++; - else if(type.id()==ID_int8) - int8_cnt++; - else if(type.id()==ID_int16) - int16_cnt++; - else if(type.id()==ID_int32) - int32_cnt++; - else if(type.id()==ID_int64) - int64_cnt++; - else if(type.id()==ID_ptr32) - ptr32_cnt++; - else if(type.id()==ID_ptr64) - ptr64_cnt++; - else if(type.id()==ID_const) - const_cnt++; - else if(type.id()==ID_restrict) - restrict_cnt++; + ++char32_t_count; else if(type.id()==ID_constexpr) - constexpr_cnt++; - else if(type.id()==ID_extern) - extern_cnt++; - else if(type.id()==ID_noreturn) - { - noreturn_cnt++; - } + c_qualifiers.is_constant = true; else if(type.id()==ID_function_type) { read_function_type(type); @@ -154,19 +89,12 @@ void cpp_convert_typet::read_rec(const typet &type) else if(type.id()==ID_array) { other.push_back(type); - cpp_convert_plain_type(other.back().subtype()); + cpp_convert_plain_type(other.back().subtype(), get_message_handler()); } else if(type.id()==ID_template) { read_template(type); } - else if(type.id()==ID_void) - { - // we store 'void' as 'empty' - typet tmp=type; - tmp.id(ID_empty); - other.push_back(tmp); - } else if(type.id()==ID_frontend_pointer) { // add width and turn into ID_pointer @@ -176,6 +104,9 @@ void cpp_convert_typet::read_rec(const typet &type) tmp.set(ID_C_reference, true); if(type.get_bool(ID_C_rvalue_reference)) tmp.set(ID_C_rvalue_reference, true); + const irep_idt typedef_identifier = type.get(ID_C_typedef); + if(!typedef_identifier.empty()) + tmp.set(ID_C_typedef, typedef_identifier); other.push_back(tmp); } else if(type.id()==ID_pointer) @@ -183,9 +114,11 @@ void cpp_convert_typet::read_rec(const typet &type) // ignore, we unfortunately convert multiple times other.push_back(type); } + else if(type.id() == ID_frontend_vector) + vector_size = static_cast(type.find(ID_size)); else { - other.push_back(type); + ansi_c_convert_typet::read_rec(type); } } @@ -194,7 +127,7 @@ void cpp_convert_typet::read_template(const typet &type) other.push_back(type); typet &t=other.back(); - cpp_convert_plain_type(t.subtype()); + cpp_convert_plain_type(t.subtype(), get_message_handler()); irept &arguments=t.add(ID_arguments); @@ -210,7 +143,7 @@ void cpp_convert_typet::read_template(const typet &type) } else { - cpp_convert_plain_type(decl.type()); + cpp_convert_plain_type(decl.type(), get_message_handler()); } // TODO: initializer @@ -231,7 +164,7 @@ void cpp_convert_typet::read_function_type(const typet &type) t.remove_subtype(); if(return_type.is_not_nil()) - cpp_convert_plain_type(return_type); + cpp_convert_plain_type(return_type, get_message_handler()); // take care of parameter types code_typet::parameterst ¶meters = t.parameters(); @@ -250,7 +183,7 @@ void cpp_convert_typet::read_function_type(const typet &type) cpp_declarationt &declaration=to_cpp_declaration(parameter_expr); source_locationt type_location=declaration.type().source_location(); - cpp_convert_plain_type(declaration.type()); + cpp_convert_plain_type(declaration.type(), get_message_handler()); // there should be only one declarator assert(declaration.declarators().size()==1); @@ -316,273 +249,84 @@ void cpp_convert_typet::read_function_type(const typet &type) void cpp_convert_typet::write(typet &type) { - type.clear(); - - // first, do "other" - if(!other.empty()) { - if(double_cnt || float_cnt || signed_cnt || - unsigned_cnt || int_cnt || cpp_bool_cnt || proper_bool_cnt || - short_cnt || char_cnt || wchar_t_cnt || - char16_t_cnt || char32_t_cnt || - int8_cnt || int16_cnt || int32_cnt || - int64_cnt || float80_cnt || float128_cnt || int128_cnt) - throw "type modifier not applicable"; - - if(other.size()!=1) - throw "illegal combination of types"; - - type.swap(other.front()); - } - else if(double_cnt) - { - if(signed_cnt || unsigned_cnt || int_cnt || - cpp_bool_cnt || proper_bool_cnt || - short_cnt || char_cnt || wchar_t_cnt || - char16_t_cnt || char32_t_cnt || - float_cnt || - int8_cnt || int16_cnt || int32_cnt || - int64_cnt || ptr32_cnt || ptr64_cnt || - float80_cnt || float128_cnt || int128_cnt) - throw "illegal type modifier for double"; - - if(long_cnt) - type=long_double_type(); - else - type=double_type(); - } - else if(float_cnt) - { - if(signed_cnt || unsigned_cnt || int_cnt || - cpp_bool_cnt || proper_bool_cnt || - short_cnt || char_cnt || wchar_t_cnt || double_cnt || - char16_t_cnt || char32_t_cnt || - int8_cnt || int16_cnt || int32_cnt || - int64_cnt || ptr32_cnt || ptr64_cnt || - float80_cnt || float128_cnt || int128_cnt) - throw "illegal type modifier for float"; - - if(long_cnt) - throw "float can't be long"; - - type=float_type(); - } - else if(float80_cnt) - { - if(signed_cnt || unsigned_cnt || int_cnt || - cpp_bool_cnt || proper_bool_cnt || - short_cnt || char_cnt || wchar_t_cnt || double_cnt || - char16_t_cnt || char32_t_cnt || - int8_cnt || int16_cnt || int32_cnt || - int64_cnt || int128_cnt || ptr32_cnt || ptr64_cnt || - float128_cnt) - throw "illegal type modifier for __float80"; - - if(long_cnt) - throw "__float80 can't be long"; - - // this isn't the same as long double - type=gcc_float64x_type(); - } - else if(float128_cnt) - { - if(signed_cnt || unsigned_cnt || int_cnt || - cpp_bool_cnt || proper_bool_cnt || - short_cnt || char_cnt || wchar_t_cnt || double_cnt || - char16_t_cnt || char32_t_cnt || - int8_cnt || int16_cnt || int32_cnt || - int64_cnt || int128_cnt || ptr32_cnt || ptr64_cnt) - throw "illegal type modifier for __float128"; - - if(long_cnt) - throw "__float128 can't be long"; + if(wchar_t_count || char16_t_count || char32_t_count) + { + error().source_location = source_location; + error() << "illegal type modifier for defined type" << eom; + throw 0; + } - // this isn't the same as long double - type=gcc_float128_type(); + ansi_c_convert_typet::write(type); } - else if(cpp_bool_cnt) + else if(c_bool_cnt) { - if(signed_cnt || unsigned_cnt || int_cnt || short_cnt || - char_cnt || wchar_t_cnt || proper_bool_cnt || - char16_t_cnt || char32_t_cnt || - int8_cnt || int16_cnt || int32_cnt || - int64_cnt || int128_cnt || ptr32_cnt || ptr64_cnt) + if( + signed_cnt || unsigned_cnt || int_cnt || short_cnt || char_cnt || + wchar_t_count || proper_bool_cnt || char16_t_count || char32_t_count || + int8_cnt || int16_cnt || int32_cnt || int64_cnt || gcc_int128_cnt || + ptr32_cnt || ptr64_cnt) + { throw "illegal type modifier for C++ bool"; + } - type = c_bool_type(); - } - else if(proper_bool_cnt) - { - if(signed_cnt || unsigned_cnt || int_cnt || short_cnt || - char_cnt || wchar_t_cnt || - char16_t_cnt || char32_t_cnt || - int8_cnt || int16_cnt || int32_cnt || - int64_cnt || int128_cnt || ptr32_cnt || ptr64_cnt) - throw "illegal type modifier for " CPROVER_PREFIX "bool"; - - type.id(ID_bool); - } - else if(char_cnt) - { - if(int_cnt || short_cnt || wchar_t_cnt || long_cnt || - char16_t_cnt || char32_t_cnt || - int8_cnt || int16_cnt || int32_cnt || - int64_cnt || int128_cnt || ptr32_cnt || ptr64_cnt) - throw "illegal type modifier for char"; - - // there are really three distinct char types in C++ - if(unsigned_cnt) - type=unsigned_char_type(); - else if(signed_cnt) - type=signed_char_type(); - else - type=char_type(); + ansi_c_convert_typet::write(type); } - else if(wchar_t_cnt) + else if(wchar_t_count) { // This is a distinct type, and can't be made signed/unsigned. // This is tolerated by most compilers, however. - if(int_cnt || short_cnt || char_cnt || long_cnt || - char16_t_cnt || char32_t_cnt || - int8_cnt || int16_cnt || int32_cnt || - int64_cnt || ptr32_cnt || ptr64_cnt) + if( + int_cnt || short_cnt || char_cnt || long_cnt || char16_t_count || + char32_t_count || int8_cnt || int16_cnt || int32_cnt || int64_cnt || + ptr32_cnt || ptr64_cnt) + { throw "illegal type modifier for wchar_t"; + } type=wchar_t_type(); + ansi_c_convert_typet::build_type_with_subtype(type); + ansi_c_convert_typet::set_attributes(type); } - else if(char16_t_cnt) + else if(char16_t_count) { // This is a distinct type, and can't be made signed/unsigned. - if(int_cnt || short_cnt || char_cnt || long_cnt || - char32_t_cnt || - int8_cnt || int16_cnt || int32_cnt || - int64_cnt || ptr32_cnt || ptr64_cnt || - signed_cnt || unsigned_cnt) + if( + int_cnt || short_cnt || char_cnt || long_cnt || char32_t_count || + int8_cnt || int16_cnt || int32_cnt || int64_cnt || ptr32_cnt || + ptr64_cnt || signed_cnt || unsigned_cnt) + { throw "illegal type modifier for char16_t"; + } type=char16_t_type(); + ansi_c_convert_typet::build_type_with_subtype(type); + ansi_c_convert_typet::set_attributes(type); } - else if(char32_t_cnt) + else if(char32_t_count) { // This is a distinct type, and can't be made signed/unsigned. if(int_cnt || short_cnt || char_cnt || long_cnt || int8_cnt || int16_cnt || int32_cnt || int64_cnt || ptr32_cnt || ptr64_cnt || signed_cnt || unsigned_cnt) + { throw "illegal type modifier for char32_t"; + } type=char32_t_type(); + ansi_c_convert_typet::build_type_with_subtype(type); + ansi_c_convert_typet::set_attributes(type); } else { - // it must be integer -- signed or unsigned? - - if(signed_cnt && unsigned_cnt) - throw "integer cannot be both signed and unsigned"; - - if(short_cnt) - { - if(long_cnt) - throw "cannot combine short and long"; - - if(unsigned_cnt) - type=unsigned_short_int_type(); - else - type=signed_short_int_type(); - } - else if(int8_cnt) - { - if(long_cnt) - throw "illegal type modifier for __int8"; - - // in terms of overloading, this behaves like "char" - if(unsigned_cnt) - type=unsigned_char_type(); - else if(signed_cnt) - type=signed_char_type(); - else - type=char_type(); // check? - } - else if(int16_cnt) - { - if(long_cnt) - throw "illegal type modifier for __int16"; - - // in terms of overloading, this behaves like "short" - if(unsigned_cnt) - type=unsigned_short_int_type(); - else - type=signed_short_int_type(); - } - else if(int32_cnt) - { - if(long_cnt) - throw "illegal type modifier for __int32"; - - // in terms of overloading, this behaves like "int" - if(unsigned_cnt) - type=unsigned_int_type(); - else - type=signed_int_type(); - } - else if(int64_cnt) - { - if(long_cnt) - throw "illegal type modifier for __int64"; - - // in terms of overloading, this behaves like "long long" - if(unsigned_cnt) - type=unsigned_long_long_int_type(); - else - type=signed_long_long_int_type(); - } - else if(int128_cnt) - { - if(long_cnt) - throw "illegal type modifier for __int128"; - - if(unsigned_cnt) - type=gcc_unsigned_int128_type(); - else - type=gcc_signed_int128_type(); - } - else if(long_cnt==0) - { - if(unsigned_cnt) - type=unsigned_int_type(); - else - type=signed_int_type(); - } - else if(long_cnt==1) - { - if(unsigned_cnt) - type=unsigned_long_int_type(); - else - type=signed_long_int_type(); - } - else if(long_cnt==2) - { - if(unsigned_cnt) - type=unsigned_long_long_int_type(); - else - type=signed_long_long_int_type(); - } - else - throw "illegal combination of type modifiers"; + ansi_c_convert_typet::write(type); } - - // is it constant? - if(const_cnt || constexpr_cnt) - type.set(ID_C_constant, true); - - // is it volatile? - if(volatile_cnt) - type.set(ID_C_volatile, true); } -void cpp_convert_plain_type(typet &type) +void cpp_convert_plain_type(typet &type, message_handlert &message_handler) { if( type.id() == ID_cpp_name || type.id() == ID_struct || @@ -604,20 +348,23 @@ void cpp_convert_plain_type(typet &type) } else { - cpp_convert_typet cpp_convert_type(type); + cpp_convert_typet cpp_convert_type(message_handler, type); cpp_convert_type.write(type); } } -void cpp_convert_auto(typet &dest, const typet &src) +void cpp_convert_auto( + typet &dest, + const typet &src, + message_handlert &message_handler) { if(dest.id() != ID_merged_type && dest.has_subtype()) { - cpp_convert_auto(dest.subtype(), src); + cpp_convert_auto(dest.subtype(), src, message_handler); return; } - cpp_convert_typet cpp_convert_type(dest); + cpp_convert_typet cpp_convert_type(message_handler, dest); for(auto &t : cpp_convert_type.other) if(t.id() == ID_auto) t = src; diff --git a/src/cpp/cpp_convert_type.h b/src/cpp/cpp_convert_type.h index 441db6ee7a3..24a55ade3cb 100644 --- a/src/cpp/cpp_convert_type.h +++ b/src/cpp/cpp_convert_type.h @@ -12,10 +12,11 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #ifndef CPROVER_CPP_CPP_CONVERT_TYPE_H #define CPROVER_CPP_CPP_CONVERT_TYPE_H -#include +class message_handlert; +class typet; -void cpp_convert_plain_type(typet &); +void cpp_convert_plain_type(typet &, message_handlert &); -void cpp_convert_auto(typet &dest, const typet &src); +void cpp_convert_auto(typet &dest, const typet &src, message_handlert &); #endif // CPROVER_CPP_CPP_CONVERT_TYPE_H diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index 79f945a2193..5c6c936a5e7 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -66,7 +66,7 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol) if(has_auto(symbol.type)) { - cpp_convert_auto(symbol.type, symbol.value.type()); + cpp_convert_auto(symbol.type, symbol.value.type(), get_message_handler()); typecheck_type(symbol.type); implicit_typecast(symbol.value, symbol.type); } @@ -152,7 +152,7 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol) } else if(has_auto(symbol.type)) { - cpp_convert_auto(symbol.type, symbol.value.type()); + cpp_convert_auto(symbol.type, symbol.value.type(), get_message_handler()); typecheck_type(symbol.type); implicit_typecast(symbol.value, symbol.type); } diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 89c2034394a..6fcb2fed457 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -1954,7 +1954,7 @@ exprt cpp_typecheck_resolvet::guess_function_template_args( // We only convert the arg_type, // and don't typecheck it -- that could cause all // sorts of trouble. - cpp_convert_plain_type(arg_type); + cpp_convert_plain_type(arg_type, cpp_typecheck.get_message_handler()); guess_template_args(arg_type, it->type()); } diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp index ad15bb5b1e6..624be9badd9 100644 --- a/src/cpp/cpp_typecheck_template.cpp +++ b/src/cpp/cpp_typecheck_template.cpp @@ -233,7 +233,7 @@ void cpp_typecheckt::typecheck_function_template( typet function_type= declarator.merge_type(declaration.type()); - cpp_convert_plain_type(function_type); + cpp_convert_plain_type(function_type, get_message_handler()); irep_idt symbol_name= function_template_identifier( diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp index ecb9a326183..9c034a432f1 100644 --- a/src/cpp/cpp_typecheck_type.cpp +++ b/src/cpp/cpp_typecheck_type.cpp @@ -27,7 +27,7 @@ void cpp_typecheckt::typecheck_type(typet &type) try { - cpp_convert_plain_type(type); + cpp_convert_plain_type(type, get_message_handler()); } catch(const char *err)