__float80 is a typedef, not a keyword

Author: Daniel Kroening

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)
     {

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,

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,14 +363,32 @@ 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)
       throw "float can't be long";
 
     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 ||

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)

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;