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$
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..d8174265c17 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -182,21 +182,45 @@ 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;
 
     // 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::APPLE)
-        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";
+    }
+
+    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
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/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 <<EOF
 // some newer versions of GCC apparently support __floatXYZ
 #define dfloat32_type_node __float32
 #define dfloat64_type_node __float64
-#define dfloat128_type_node __float128
+#define dfloat128_type_node __CPROVER_Float128
 
 #define build_qualified_type(t, q) q t
 #define build_pointer_type(t) t*
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index 031d64365ab..9e73ee7785f 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
@@ -489,15 +489,17 @@ 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;
                 }
 
-"__float128"    { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
+"__CPROVER_Float80" {
+                  loc(); return TOK_GCC_FLOAT80;
+                }
+
+"__float128"    { // This is a keyword for CLANG,
+                  // but a typedef for GCC
+                  if(PARSER.mode==configt::ansi_ct::flavourt::CLANG)
                   { loc(); return TOK_GCC_FLOAT128; }
                   else
                     return make_identifier();
@@ -509,6 +511,10 @@ void ansi_c_scanner_init()
                     return make_identifier();
                 }
 
+"__CPROVER_Float128" {
+                  loc(); return TOK_GCC_FLOAT128;
+                }
+
 "_Float128x"    { if(PARSER.ts_18661_3_Floatn_types)
                   { loc(); return TOK_GCC_FLOAT128X; }
                   else
@@ -516,7 +522,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 +573,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 +582,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 +591,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 +610,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 +620,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 +629,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 +638,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 +656,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 +695,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 +711,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 +823,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 +891,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 +950,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 +1125,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 +1133,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 +1160,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 +1259,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 +1270,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 +1281,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 +1303,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 +1312,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 +1323,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 +1334,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 +1345,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 +1356,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 +1367,32 @@ __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::CLANG)
+                { /* ignore */ }
+              else
+                return make_identifier();
+            }
+
+  /* This is a clang extension */
 
-"_Nullable" { if(PARSER.mode==configt::ansi_ct::flavourt::APPLE)
+"_Nonnull" { 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)
+"_Null_unspecified" { if(PARSER.mode==configt::ansi_ct::flavourt::CLANG)
                 { /* ignore */ }
               else
                 return make_identifier();
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 9f733c6abab..673c97442d6 100644
--- a/src/cpp/cpp_internal_additions.cpp
+++ b/src/cpp/cpp_internal_additions.cpp
@@ -115,19 +115,45 @@ 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);
 
     if(
       config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
-      config.ansi_c.arch == "x32")
+      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")
     {
-      // clang doesn't do __float128
-      if(config.ansi_c.mode == configt::ansi_ct::flavourt::APPLE)
-        out << "typedef double __float128;" << '\n';
+      // 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.
+      // C++ doesn't have _Float128.
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
+        out << "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.
+      // C++ doesn't have _Float128.
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
+        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
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;
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..9bea9ec7cd2 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")
@@ -904,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
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,