bugfix: __float128

Author: Daniel Kroening

src/ansi-c/ansi_c_internal_additions.cpp

@@ -196,8 +196,10 @@ 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::CLANG)
-        code+="typedef double __float128;\n"; // clang doesn't do __float128
+      // 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/cpp/cpp_internal_additions.cpp

@@ -127,8 +127,9 @@ 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::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 long double __float128;" << '\n';
     }
 
     // On 64-bit systems, gcc has typedefs