bugfix: __float128

Author: Daniel Kroening

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
+      // clang doesn't do __float128
+      // Note that this is a typedef and not a keyword.
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
+        code += "typedef _Float128 __float128;\n";
+    }
+    else if(config.ansi_c.arch == "hppa")
+    {
+      // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
+      // clang doesn't do __float128
+      // Note that 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

src/ansi-c/scanner.l

@@ -496,13 +496,6 @@ void ansi_c_scanner_init()
                     return make_identifier();
                 }
 
-"__float128"    { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
-                  { loc(); return TOK_GCC_FLOAT128; }
-                  else
-                    return make_identifier();
-                }
-
 "_Float128"     { if(PARSER.Float128_type)
                   { loc(); return TOK_GCC_FLOAT128; }
                   else

src/cpp/cpp_internal_additions.cpp

@@ -124,11 +124,23 @@ void cpp_internal_additions(std::ostream &out)
 
     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")
     {
+      // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
       // clang doesn't do __float128
-      if(config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG)
-        out << "typedef double __float128;" << '\n';
+      // Note that this is a typedef and not a keyword.
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
+        out << "typedef _Float128 __float128;" << '\n';
+    }
+    else if(config.ansi_c.arch == "hppa")
+    {
+      // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
+      // clang doesn't do __float128
+      // Note that this is a typedef and not a keyword.
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
+        out << "typedef long double __float128;" << '\n';
     }
 
     // On 64-bit systems, gcc has typedefs