From 3849bb0f2064d5626d067d07c556b9a6cce9d357 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 28 Jul 2018 14:55:38 +0100 Subject: [PATCH 1/6] rename APPLE flavor to CLANG --- src/ansi-c/ansi_c_declaration.cpp | 7 ++- src/ansi-c/ansi_c_internal_additions.cpp | 11 ++-- src/ansi-c/builtin_factory.cpp | 7 ++- src/ansi-c/c_typecheck_base.cpp | 2 +- src/ansi-c/scanner.l | 72 ++++++++++++------------ src/cpp/cpp_internal_additions.cpp | 9 +-- src/goto-cc/gcc_mode.cpp | 2 +- src/util/config.cpp | 35 ++++++------ src/util/config.h | 12 +++- 9 files changed, 85 insertions(+), 72 deletions(-) diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp index 5287fa6cfb6..859b99a2d36 100644 --- a/src/ansi-c/ansi_c_declaration.cpp +++ b/src/ansi-c/ansi_c_declaration.cpp @@ -150,9 +150,10 @@ void ansi_c_declarationt::to_symbol( if(get_is_inline()) symbol.type.set(ID_C_inlined, true); - if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC || - config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE || - config.ansi_c.mode==configt::ansi_ct::flavourt::ARM) + if( + config.ansi_c.mode == configt::ansi_ct::flavourt::GCC || + config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG || + config.ansi_c.mode == configt::ansi_ct::flavourt::ARM) { // GCC extern inline cleanup, to enable remove_internal_symbols // do its full job diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 21f6fc41f4a..71808c10c9b 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -182,9 +182,10 @@ void ansi_c_internal_additions(std::string &code) "\n"; // GCC junk stuff, also for CLANG and ARM - if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC || - config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE || - config.ansi_c.mode==configt::ansi_ct::flavourt::ARM) + if( + config.ansi_c.mode == configt::ansi_ct::flavourt::GCC || + config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG || + config.ansi_c.mode == configt::ansi_ct::flavourt::ARM) { code+=gcc_builtin_headers_types; @@ -195,11 +196,11 @@ void ansi_c_internal_additions(std::string &code) config.ansi_c.arch=="x86_64" || config.ansi_c.arch=="x32") { - if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE) + if(config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG) code+="typedef double __float128;\n"; // clang doesn't do __float128 } - // On 64-bit systems, gcc has typedefs + // On 64-bit systems, both gcc and clang have typedefs // __int128_t und __uint128_t -- but not on 32 bit! if(config.ansi_c.long_int_width>=64) { diff --git a/src/ansi-c/builtin_factory.cpp b/src/ansi-c/builtin_factory.cpp index a92269a754c..f20c669cf87 100644 --- a/src/ansi-c/builtin_factory.cpp +++ b/src/ansi-c/builtin_factory.cpp @@ -134,9 +134,10 @@ bool builtin_factory( } // GCC junk stuff, also for CLANG and ARM - if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC || - config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE || - config.ansi_c.mode==configt::ansi_ct::flavourt::ARM) + if( + config.ansi_c.mode == configt::ansi_ct::flavourt::GCC || + config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG || + config.ansi_c.mode == configt::ansi_ct::flavourt::ARM) { if(find_pattern(pattern, gcc_builtin_headers_generic, s)) return convert(identifier, s, symbol_table, mh); diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index aeddbf14a0a..ee120fe00fd 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -336,7 +336,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type( if( old_symbol.type.get_bool(ID_C_inlined) && (config.ansi_c.mode == configt::ansi_ct::flavourt::GCC || - config.ansi_c.mode == configt::ansi_ct::flavourt::APPLE || + config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG || config.ansi_c.mode == configt::ansi_ct::flavourt::ARM || config.ansi_c.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO)) { diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 031d64365ab..54abb2e602d 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -452,7 +452,7 @@ void ansi_c_scanner_init() "while" { loc(); return TOK_WHILE; } "__auto_type" { if((PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE) + PARSER.mode==configt::ansi_ct::flavourt::CLANG) && !PARSER.cpp98) { loc(); return TOK_GCC_AUTO_TYPE; } else @@ -516,7 +516,7 @@ void ansi_c_scanner_init() } "__int128" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE) + PARSER.mode==configt::ansi_ct::flavourt::CLANG) { loc(); return TOK_GCC_INT128; } else return make_identifier(); @@ -567,7 +567,7 @@ void ansi_c_scanner_init() "__complex__" | "__complex" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM) { loc(); return TOK_COMPLEX; } else @@ -576,7 +576,7 @@ void ansi_c_scanner_init() "__real__" | "__real" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM) { loc(); return TOK_REAL; } else @@ -585,7 +585,7 @@ void ansi_c_scanner_init() "__imag__" | "__imag" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM) { loc(); return TOK_IMAG; } else @@ -604,7 +604,7 @@ void ansi_c_scanner_init() } "__builtin_va_arg" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM) { loc(); return TOK_BUILTIN_VA_ARG; } else @@ -614,7 +614,7 @@ void ansi_c_scanner_init() "__builtin_offsetof" | "__offsetof__" | "offsetof" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM) { loc(); return TOK_OFFSETOF; } else @@ -623,7 +623,7 @@ void ansi_c_scanner_init() "__builtin_types_compatible_p" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM) { loc(); return TOK_GCC_BUILTIN_TYPES_COMPATIBLE_P; } else @@ -632,14 +632,14 @@ void ansi_c_scanner_init() "__builtin_convertvector" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE) + PARSER.mode==configt::ansi_ct::flavourt::CLANG) { loc(); return TOK_CLANG_BUILTIN_CONVERTVECTOR; } else return make_identifier(); } "__alignof__" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM) { loc(); return TOK_ALIGNOF; } else @@ -650,7 +650,7 @@ void ansi_c_scanner_init() // http://msdn.microsoft.com/en-us/library/45t0s5f4%28v=vs.71%29.aspx if(PARSER.mode==configt::ansi_ct::flavourt::VISUAL_STUDIO || PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM) { loc(); return TOK_ALIGNOF; } else @@ -689,7 +689,7 @@ void ansi_c_scanner_init() } "asm" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::CODEWARRIOR) { if(PARSER.cpp98) @@ -705,7 +705,7 @@ void ansi_c_scanner_init() } "__asm__" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::CODEWARRIOR || PARSER.mode==configt::ansi_ct::flavourt::ARM) { @@ -817,7 +817,7 @@ xor_eq { return cpp98_keyword(TOK_XORASSIGN); } __decltype { if(PARSER.cpp98 && (PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE)) + PARSER.mode==configt::ansi_ct::flavourt::CLANG)) return cpp98_keyword(TOK_DECLTYPE); else return make_identifier(); @@ -885,28 +885,28 @@ __decltype { if(PARSER.cpp98 && } "__char16_t" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE) + PARSER.mode==configt::ansi_ct::flavourt::CLANG) return cpp98_keyword(TOK_CHAR16_T); // GNU extension else return make_identifier(); } "__nullptr" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE) + PARSER.mode==configt::ansi_ct::flavourt::CLANG) return cpp98_keyword(TOK_NULLPTR); // GNU extension else return make_identifier(); } "__null" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE) + PARSER.mode==configt::ansi_ct::flavourt::CLANG) return cpp98_keyword(TOK_NULLPTR); // GNU extension else return make_identifier(); } "__char32_t" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE) + PARSER.mode==configt::ansi_ct::flavourt::CLANG) return cpp98_keyword(TOK_CHAR32_T); // GNU extension else return make_identifier(); @@ -944,7 +944,7 @@ __decltype { if(PARSER.cpp98 && "__attribute__" | "__attribute" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::CODEWARRIOR || PARSER.mode==configt::ansi_ct::flavourt::ARM) { @@ -1119,7 +1119,7 @@ __decltype { if(PARSER.cpp98 && "typeof" { if(PARSER.cpp98 || PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::CODEWARRIOR || PARSER.mode==configt::ansi_ct::flavourt::ARM) { loc(); return TOK_TYPEOF; } @@ -1127,7 +1127,7 @@ __decltype { if(PARSER.cpp98 && return make_identifier(); } "__typeof" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM) { loc(); return TOK_TYPEOF; } else @@ -1154,7 +1154,7 @@ __decltype { if(PARSER.cpp98 && "__inline__" { loc(); return TOK_INLINE; } "__label__" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM) { loc(); return TOK_GCC_LABEL; } else @@ -1253,7 +1253,7 @@ __decltype { if(PARSER.cpp98 && } "__thread" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM) { loc(); return TOK_THREAD_LOCAL; } else @@ -1264,7 +1264,7 @@ __decltype { if(PARSER.cpp98 && "_Alignas" { if(!PARSER.cpp98 && (PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM)) { loc(); return TOK_ALIGNAS; } else @@ -1275,7 +1275,7 @@ __decltype { if(PARSER.cpp98 && "_Alignof" { if(!PARSER.cpp98 && (PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM || PARSER.mode==configt::ansi_ct::flavourt::VISUAL_STUDIO)) { loc(); return TOK_ALIGNOF; } @@ -1297,7 +1297,7 @@ __decltype { if(PARSER.cpp98 && if(!PARSER.cpp98 && (PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM)) { loc(); return TOK_ATOMIC_TYPE_SPECIFIER; } else @@ -1306,7 +1306,7 @@ __decltype { if(PARSER.cpp98 && "_Atomic" { if(!PARSER.cpp98 && (PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM)) { loc(); return TOK_ATOMIC_TYPE_QUALIFIER; } else @@ -1317,7 +1317,7 @@ __decltype { if(PARSER.cpp98 && "_Generic" { if(!PARSER.cpp98 && (PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM)) { loc(); return TOK_GENERIC; } else @@ -1328,7 +1328,7 @@ __decltype { if(PARSER.cpp98 && "_Imaginary" { if(!PARSER.cpp98 && (PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM)) { loc(); return TOK_IMAGINARY; } else @@ -1339,7 +1339,7 @@ __decltype { if(PARSER.cpp98 && "_Noreturn" { if(!PARSER.cpp98 && (PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM)) { loc(); return TOK_NORETURN; } else @@ -1350,7 +1350,7 @@ __decltype { if(PARSER.cpp98 && "_Static_assert" { if(!PARSER.cpp98 && (PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM)) { loc(); return TOK_STATIC_ASSERT; } else @@ -1361,24 +1361,24 @@ __decltype { if(PARSER.cpp98 && "_Thread_local" { if(!PARSER.cpp98 && (PARSER.mode==configt::ansi_ct::flavourt::GCC || - PARSER.mode==configt::ansi_ct::flavourt::APPLE || + PARSER.mode==configt::ansi_ct::flavourt::CLANG || PARSER.mode==configt::ansi_ct::flavourt::ARM)) { loc(); return TOK_THREAD_LOCAL; } else return make_identifier(); } - /* This is an Apple clang extension */ + /* This is a clang extension */ -"_Nullable" { if(PARSER.mode==configt::ansi_ct::flavourt::APPLE) +"_Nullable" { if(PARSER.mode==configt::ansi_ct::flavourt::CLANG) { /* ignore */ } else return make_identifier(); } - /* This is an Apple clang extension */ + /* This is a clang extension */ -"_Nonnull" { if(PARSER.mode==configt::ansi_ct::flavourt::APPLE) +"_Nonnull" { if(PARSER.mode==configt::ansi_ct::flavourt::CLANG) { /* ignore */ } else return make_identifier(); diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 9f733c6abab..e1048cf6888 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -115,9 +115,10 @@ void cpp_internal_additions(std::ostream &out) out << "void " INITIALIZE_FUNCTION "();" << '\n'; // GCC junk stuff, also for CLANG and ARM - if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC || - config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE || - config.ansi_c.mode==configt::ansi_ct::flavourt::ARM) + if( + config.ansi_c.mode == configt::ansi_ct::flavourt::GCC || + config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG || + config.ansi_c.mode == configt::ansi_ct::flavourt::ARM) { out << c2cpp(gcc_builtin_headers_types); @@ -126,7 +127,7 @@ void cpp_internal_additions(std::ostream &out) config.ansi_c.arch == "x32") { // clang doesn't do __float128 - if(config.ansi_c.mode == configt::ansi_ct::flavourt::APPLE) + if(config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG) out << "typedef double __float128;" << '\n'; } diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 373ddb21411..97d316e85ba 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -564,7 +564,7 @@ int gcc_modet::doit() debug() << "Enabling Visual Studio syntax" << eom; } else if(config.this_operating_system()=="macos") - config.ansi_c.mode=configt::ansi_ct::flavourt::APPLE; + config.ansi_c.mode = configt::ansi_ct::flavourt::CLANG; else config.ansi_c.mode=configt::ansi_ct::flavourt::GCC; diff --git a/src/util/config.cpp b/src/util/config.cpp index 56a39662c95..e14d4fb8769 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -155,11 +155,11 @@ void configt::ansi_ct::set_arch_spec_i386() switch(mode) { case flavourt::GCC: - case flavourt::APPLE: + case flavourt::CLANG: defines.push_back("i386"); defines.push_back("__i386"); defines.push_back("__i386__"); - if(mode==flavourt::APPLE) + if(mode == flavourt::CLANG) defines.push_back("__LITTLE_ENDIAN__"); break; @@ -188,14 +188,15 @@ void configt::ansi_ct::set_arch_spec_x86_64() switch(mode) { case flavourt::GCC: - case flavourt::APPLE: + case flavourt::CLANG: defines.push_back("__LP64__"); defines.push_back("__x86_64"); defines.push_back("__x86_64__"); defines.push_back("_LP64"); defines.push_back("__amd64__"); defines.push_back("__amd64"); - if(mode==flavourt::APPLE) + + if(os == ost::OS_MACOS) defines.push_back("__LITTLE_ENDIAN__"); break; @@ -233,13 +234,13 @@ void configt::ansi_ct::set_arch_spec_power(const irep_idt &subarch) switch(mode) { case flavourt::GCC: - case flavourt::APPLE: + case flavourt::CLANG: defines.push_back("__powerpc"); defines.push_back("__powerpc__"); defines.push_back("__POWERPC__"); defines.push_back("__ppc__"); - if(mode==flavourt::APPLE) + if(os == ost::OS_MACOS) defines.push_back("__BIG_ENDIAN__"); if(subarch!="powerpc") @@ -295,7 +296,7 @@ void configt::ansi_ct::set_arch_spec_arm(const irep_idt &subarch) switch(mode) { case flavourt::GCC: - case flavourt::APPLE: + case flavourt::CLANG: if(subarch=="arm64") defines.push_back("__aarch64__"); else @@ -336,7 +337,7 @@ void configt::ansi_ct::set_arch_spec_alpha() defines.push_back("_M_ALPHA"); break; - case flavourt::APPLE: + case flavourt::CLANG: case flavourt::CODEWARRIOR: case flavourt::ARM: case flavourt::ANSI: @@ -386,7 +387,7 @@ void configt::ansi_ct::set_arch_spec_mips(const irep_idt &subarch) UNREACHABLE; // not supported by Visual Studio break; - case flavourt::APPLE: + case flavourt::CLANG: case flavourt::CODEWARRIOR: case flavourt::ARM: case flavourt::ANSI: @@ -415,7 +416,7 @@ void configt::ansi_ct::set_arch_spec_s390() UNREACHABLE; // not supported by Visual Studio break; - case flavourt::APPLE: + case flavourt::CLANG: case flavourt::CODEWARRIOR: case flavourt::ARM: case flavourt::ANSI: @@ -443,7 +444,7 @@ void configt::ansi_ct::set_arch_spec_s390x() UNREACHABLE; // not supported by Visual Studio break; - case flavourt::APPLE: + case flavourt::CLANG: case flavourt::CODEWARRIOR: case flavourt::ARM: case flavourt::ANSI: @@ -483,7 +484,7 @@ void configt::ansi_ct::set_arch_spec_sparc(const irep_idt &subarch) UNREACHABLE; // not supported by Visual Studio break; - case flavourt::APPLE: + case flavourt::CLANG: case flavourt::CODEWARRIOR: case flavourt::ARM: case flavourt::ANSI: @@ -514,7 +515,7 @@ void configt::ansi_ct::set_arch_spec_ia64() defines.push_back("_M_IA64"); break; - case flavourt::APPLE: + case flavourt::CLANG: case flavourt::CODEWARRIOR: case flavourt::ARM: case flavourt::ANSI: @@ -549,7 +550,7 @@ void configt::ansi_ct::set_arch_spec_x32() UNREACHABLE; // not supported by Visual Studio break; - case flavourt::APPLE: + case flavourt::CLANG: case flavourt::CODEWARRIOR: case flavourt::ARM: case flavourt::ANSI: @@ -603,7 +604,7 @@ void configt::ansi_ct::set_arch_spec_hppa() UNREACHABLE; // not supported by Visual Studio break; - case flavourt::APPLE: + case flavourt::CLANG: case flavourt::CODEWARRIOR: case flavourt::ARM: case flavourt::ANSI: @@ -633,7 +634,7 @@ void configt::ansi_ct::set_arch_spec_sh4() UNREACHABLE; // not supported by Visual Studio break; - case flavourt::APPLE: + case flavourt::CLANG: case flavourt::CODEWARRIOR: case flavourt::ARM: case flavourt::ANSI: @@ -890,7 +891,7 @@ bool configt::set(const cmdlinet &cmdline) { ansi_c.lib=configt::ansi_ct::libt::LIB_FULL; ansi_c.os=configt::ansi_ct::ost::OS_MACOS; - ansi_c.mode=ansi_ct::flavourt::APPLE; + ansi_c.mode = ansi_ct::flavourt::CLANG; ansi_c.preprocessor=ansi_ct::preprocessort::CLANG; } else if(os=="linux" || os=="solaris") diff --git a/src/util/config.h b/src/util/config.h index 2209d92b4ab..1de13531ac0 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -101,8 +101,16 @@ class configt void set_arch_spec_hppa(); void set_arch_spec_sh4(); - enum class flavourt { NONE, ANSI, GCC, ARM, APPLE, - VISUAL_STUDIO, CODEWARRIOR }; + enum class flavourt + { + NONE, + ANSI, + GCC, + ARM, + CLANG, + VISUAL_STUDIO, + CODEWARRIOR + }; flavourt mode; // the syntax of source files enum class preprocessort { NONE, GCC, CLANG, VISUAL_STUDIO, From 16a49a7c189c8391997f1d00db0e098b9d3eaea7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 28 Jul 2018 15:00:31 +0100 Subject: [PATCH 2/6] bugfix: __float128 --- src/ansi-c/ansi_c_internal_additions.cpp | 23 ++++++++++++++++++----- src/ansi-c/gcc_builtin_headers_ia32.h | 8 ++++---- src/ansi-c/get-gcc-builtins.sh | 2 +- src/ansi-c/scanner.l | 9 +++++++-- src/cpp/cpp_internal_additions.cpp | 22 ++++++++++++++++++---- 5 files changed, 48 insertions(+), 16 deletions(-) diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 71808c10c9b..50860180c62 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -192,12 +192,25 @@ void ansi_c_internal_additions(std::string &code) // there are many more, e.g., look at // https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html - if(config.ansi_c.arch=="i386" || - config.ansi_c.arch=="x86_64" || - config.ansi_c.arch=="x32") + if( + config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" || + config.ansi_c.arch == "x32" || config.ansi_c.arch == "powerpc" || + config.ansi_c.arch == "ppc64" || config.ansi_c.arch == "ppc64le" || + config.ansi_c.arch == "ia64") { - if(config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG) - code+="typedef double __float128;\n"; // clang doesn't do __float128 + // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html + // For clang, __float128 is a keyword. + // For gcc, this is a typedef and not a keyword. + if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG) + code += "typedef __CPROVER_Float128 __float128;\n"; + } + else if(config.ansi_c.arch == "hppa") + { + // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html + // For clang, __float128 is a keyword. + // For gcc, this is a typedef and not a keyword. + if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG) + code+="typedef long double __float128;\n"; } // On 64-bit systems, both gcc and clang have typedefs diff --git a/src/ansi-c/gcc_builtin_headers_ia32.h b/src/ansi-c/gcc_builtin_headers_ia32.h index 9be09f54701..1cf8a04df6c 100644 --- a/src/ansi-c/gcc_builtin_headers_ia32.h +++ b/src/ansi-c/gcc_builtin_headers_ia32.h @@ -1,11 +1,11 @@ // from // http://gcc.gnu.org/onlinedocs/gcc-4.7.0/gcc/X86-Built_002din-Functions.html -__float128 __builtin_fabsq(__float128); -__float128 __builtin_copysignq(__float128, __float128); +__CPROVER_Float128 __builtin_fabsq(__CPROVER_Float128); +__CPROVER_Float128 __builtin_copysignq(__CPROVER_Float128, __CPROVER_Float128); void __builtin_ia32_pause(); -__float128 __builtin_infq(void); -__float128 __builtin_huge_valq(void); +__CPROVER_Float128 __builtin_infq(void); +__CPROVER_Float128 __builtin_huge_valq(void); __gcc_v8qi __builtin_ia32_paddb(__gcc_v8qi, __gcc_v8qi); __gcc_v4hi __builtin_ia32_paddw(__gcc_v4hi, __gcc_v4hi); __gcc_v2si __builtin_ia32_paddd(__gcc_v2si, __gcc_v2si); diff --git a/src/ansi-c/get-gcc-builtins.sh b/src/ansi-c/get-gcc-builtins.sh index fd06b79945d..344c271d692 100755 --- a/src/ansi-c/get-gcc-builtins.sh +++ b/src/ansi-c/get-gcc-builtins.sh @@ -102,7 +102,7 @@ cat > builtins.h < Date: Sat, 28 Jul 2018 15:03:49 +0100 Subject: [PATCH 3/6] added _Null_unspecified clang extension --- src/ansi-c/scanner.l | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 5ee1199dd63..6ded268b7db 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1389,6 +1389,14 @@ __decltype { if(PARSER.cpp98 && return make_identifier(); } + /* This is a clang extension */ + +"_Null_unspecified" { if(PARSER.mode==configt::ansi_ct::flavourt::CLANG) + { /* ignore */ } + else + return make_identifier(); + } + } /* operators following */ From 54956259ad976c0deb1ad1ce1abb8e9f5239cb65 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 28 Jul 2018 15:07:12 +0100 Subject: [PATCH 4/6] FreeBSD: default flavor is now CLANG --- src/util/config.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/config.cpp b/src/util/config.cpp index e14d4fb8769..9bea9ec7cd2 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -905,7 +905,7 @@ bool configt::set(const cmdlinet &cmdline) { ansi_c.lib=configt::ansi_ct::libt::LIB_FULL; ansi_c.os=configt::ansi_ct::ost::OS_LINUX; - ansi_c.mode=ansi_ct::flavourt::GCC; + ansi_c.mode=ansi_ct::flavourt::CLANG; ansi_c.preprocessor=ansi_ct::preprocessort::CLANG; } else From 8288a72298ca498089632851dec53a2ed779a58f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 28 Jul 2018 15:20:14 +0100 Subject: [PATCH 5/6] __float80 is a typedef, not a keyword --- src/ansi-c/ansi_c_internal_additions.cpp | 12 +++++++++- src/ansi-c/scanner.l | 11 +++++---- src/cpp/cpp_convert_type.cpp | 30 ++++++++++++++++++++---- src/cpp/cpp_internal_additions.cpp | 11 +++++++++ src/cpp/parse.cpp | 3 ++- 5 files changed, 55 insertions(+), 12 deletions(-) diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 50860180c62..d8174265c17 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -213,7 +213,17 @@ void ansi_c_internal_additions(std::string &code) code+="typedef long double __float128;\n"; } - // On 64-bit systems, both gcc and clang have typedefs + if( + config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" || + config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64") + { + // clang doesn't do __float80 + // Note that __float80 is a typedef, and not a keyword. + if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG) + code += "typedef __CPROVER_Float64x __float80;\n"; + } + + // On 64-bit systems, gcc has typedefs // __int128_t und __uint128_t -- but not on 32 bit! if(config.ansi_c.long_int_width>=64) { diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 6ded268b7db..9e73ee7785f 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -489,11 +489,12 @@ void ansi_c_scanner_init() return make_identifier(); } -"__float80" { // clang doesn't have it - if(PARSER.mode==configt::ansi_ct::flavourt::GCC) - { loc(); return TOK_GCC_FLOAT80; } - else - return make_identifier(); +"__CPROVER_Float64x" { + loc(); return TOK_GCC_FLOAT64X; + } + +"__CPROVER_Float80" { + loc(); return TOK_GCC_FLOAT80; } "__float128" { // This is a keyword for CLANG, diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index 7002d7de4be..e3dcadddea7 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -32,7 +32,7 @@ class cpp_convert_typet 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, - float128_cnt, int128_cnt; + float80_cnt, float128_cnt, int128_cnt; void read(const typet &type); void write(typet &type); @@ -55,7 +55,7 @@ void cpp_convert_typet::read(const typet &type) 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=float128_cnt=int128_cnt=0; + ptr32_cnt=ptr64_cnt=float80_cnt=float128_cnt=int128_cnt=0; other.clear(); @@ -96,6 +96,8 @@ void cpp_convert_typet::read_rec(const typet &type) 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) @@ -329,7 +331,7 @@ void cpp_convert_typet::write(typet &type) short_cnt || char_cnt || wchar_t_cnt || char16_t_cnt || char32_t_cnt || int8_cnt || int16_cnt || int32_cnt || - int64_cnt || float128_cnt || int128_cnt) + int64_cnt || float80_cnt || float128_cnt || int128_cnt) throw "type modifier not applicable"; if(other.size()!=1) @@ -346,7 +348,7 @@ void cpp_convert_typet::write(typet &type) float_cnt || int8_cnt || int16_cnt || int32_cnt || int64_cnt || ptr32_cnt || ptr64_cnt || - float128_cnt || int128_cnt) + float80_cnt || float128_cnt || int128_cnt) throw "illegal type modifier for double"; if(long_cnt) @@ -361,7 +363,8 @@ void cpp_convert_typet::write(typet &type) 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 || float128_cnt || int128_cnt) + int64_cnt || ptr32_cnt || ptr64_cnt || + float80_cnt || float128_cnt || int128_cnt) throw "illegal type modifier for float"; if(long_cnt) @@ -369,6 +372,23 @@ void cpp_convert_typet::write(typet &type) 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 || diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 215b3adc0ab..673c97442d6 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -145,6 +145,17 @@ void cpp_internal_additions(std::ostream &out) out << "typedef long double __float128;" << '\n'; } + if( + config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" || + config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64") + { + // clang doesn't do __float80 + // Note that __float80 is a typedef, and not a keyword, + // and that C++ doesn't have _Float64x. + if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG) + out << "typedef __CPROVER_Float80 __float80;" << '\n'; + } + // On 64-bit systems, gcc has typedefs // __int128_t und __uint128_t -- but not on 32 bit! if(config.ansi_c.long_int_width >= 64) diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index bae7366f9a0..dabfebb85b7 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -762,7 +762,7 @@ bool Parser::isTypeSpecifier() || t==TOK_INT8 || t==TOK_INT16 || t==TOK_INT32 || t==TOK_INT64 || t==TOK_GCC_INT128 || t==TOK_PTR32 || t==TOK_PTR64 - || t==TOK_GCC_FLOAT128 + || t==TOK_GCC_FLOAT80 || t==TOK_GCC_FLOAT128 || t==TOK_VOID || t==TOK_BOOL || t==TOK_CPROVER_BOOL || t==TOK_CLASS || t==TOK_STRUCT || t==TOK_UNION || t==TOK_ENUM || t==TOK_INTERFACE @@ -2455,6 +2455,7 @@ bool Parser::optIntegralTypeOrClassSpec(typet &p) case TOK_INT32: type_id=ID_int32; break; case TOK_INT64: type_id=ID_int64; break; case TOK_GCC_INT128: type_id=ID_gcc_int128; break; + case TOK_GCC_FLOAT80: type_id=ID_gcc_float80; break; case TOK_GCC_FLOAT128: type_id=ID_gcc_float128; break; case TOK_BOOL: type_id=ID_bool; break; case TOK_CPROVER_BOOL: type_id=ID_proper_bool; break; From f74c161312ce8137c72c9f303c4a994d18f3a1b7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 30 Jul 2018 14:59:37 +0100 Subject: [PATCH 6/6] test for __float80 and __float128 --- regression/ansi-c/gcc_float_types1/main.c | 19 +++++++++++++++++++ regression/ansi-c/gcc_float_types1/test.desc | 8 ++++++++ 2 files changed, 27 insertions(+) create mode 100644 regression/ansi-c/gcc_float_types1/main.c create mode 100644 regression/ansi-c/gcc_float_types1/test.desc diff --git a/regression/ansi-c/gcc_float_types1/main.c b/regression/ansi-c/gcc_float_types1/main.c new file mode 100644 index 00000000000..e72a6f65273 --- /dev/null +++ b/regression/ansi-c/gcc_float_types1/main.c @@ -0,0 +1,19 @@ +// for gcc, __float80 and __float128 are typedefs +// for clang, __float128 is a keyword, and __float80 doesn't exist. + +#ifdef __clang__ +int __float80; +__float128 f128; +#else +__float80 f80; +__float128 f128; +#endif + +int main() +{ + #ifndef __clang__ + // on gcc, they can be re-declared, as they are identifiers, not keywords + int __float80; + int __float128; + #endif +} diff --git a/regression/ansi-c/gcc_float_types1/test.desc b/regression/ansi-c/gcc_float_types1/test.desc new file mode 100644 index 00000000000..0e1ed863bc1 --- /dev/null +++ b/regression/ansi-c/gcc_float_types1/test.desc @@ -0,0 +1,8 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$