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 __CPROVER_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/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);

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*

src/ansi-c/scanner.l

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

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 __CPROVER_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