fix up __float128 and _Float128 support

_Float128 is a keyword, defined in ISO/IEC TS 18661-3:2015.
It's a typedef since gcc 6.0.
It's a genuine keyword since gcc 7.0.
clang does not offer it.

__float128 is a typedef in gcc since 4.3/4.5, depending on architecture.

__float128 is a keyword in clang.

This PR attempts to clean this up.

Author: kroening

regression/ansi-c/gcc_version1/gcc-5.c

@@ -3,7 +3,8 @@ typedef float _Float32;
 typedef double _Float32x;
 typedef double _Float64;
 typedef long double _Float64x;
+typedef long double _Float128;
 typedef long double _Float128x;
 
 // But this type should:
-_Float128 f128;
+__float128 f128;

regression/ansi-c/gcc_version1/gcc-7.c

@@ -5,3 +5,5 @@ _Float64 f64;
 _Float64x f64x;
 _Float128 f128;
 _Float128x f128x;
+
+__float128 gcc_f128;

regression/cbmc/ts18661_typedefs/main.c

@@ -1,31 +1,51 @@
-#if defined(__GNUC__) && !defined(__clang__)
+#if defined(__GNUC__)
 
-#include <features.h> // For __GNUC_PREREQ
+#  ifdef __clang__
 
-#ifdef __x86_64__
-#define FLOAT128_MINOR_VERSION 3
-#else
-#define FLOAT128_MINOR_VERSION 5
-#endif
+#    define HAS_FLOAT128
 
-#if __GNUC__ >= 7
-#define HAS_FLOATN
-#elif __GNUC_PREREQ(4, FLOAT128_MINOR_VERSION)
-#define HAS_FLOAT128
-#endif
+#  else
+
+#    include <features.h> // For __GNUC_PREREQ
+
+#    ifdef __x86_64__
+#      define FLOAT128_MINOR_VERSION 3
+#    else
+#      define FLOAT128_MINOR_VERSION 5
+#    endif
+
+#    if __GNUC__ >= 7
+#      define HAS_FLOATN
+#    endif
+
+#    if __GNUC_PREREQ(4, FLOAT128_MINOR_VERSION)
+#      define HAS_FLOAT128
+#    endif
+
+#  endif
 
 #endif
 
-#ifndef HAS_FLOATN
+#ifdef HAS_FLOATN
+typedef _Float32 f1;
+typedef _Float32x f2;
+typedef _Float64 f3;
+typedef _Float64x f4;
+typedef _Float128 f5;
+typedef _Float128x f6;
+#else
 typedef float _Float32;
 typedef double _Float32x;
 typedef double _Float64;
 typedef long double _Float64x;
+typedef long double _Float128;
 typedef long double _Float128x;
 #endif
 
-#if !defined(HAS_FLOATN) && !defined(HAS_FLOAT128)
-typedef long double _Float128;
+#if defined(HAS_FLOAT128)
+typedef __float128 f7;
+#else
+typedef long double __float128;
 #endif
 
 int main(int argc, char** argv) {

src/ansi-c/ansi_c_internal_additions.cpp

@@ -208,8 +208,12 @@ void ansi_c_internal_additions(std::string &code)
       // 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)
+      if(
+        config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG &&
+        config.ansi_c.gcc__float128_type)
+      {
         code += "typedef " CPROVER_PREFIX "Float128 __float128;\n";
+      }
     }
     else if(config.ansi_c.arch == "ppc64le")
     {
@@ -222,8 +226,12 @@ void ansi_c_internal_additions(std::string &code)
       // 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)
+      if(
+        config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG &&
+        config.ansi_c.gcc__float128_type)
+      {
         code+="typedef long double __float128;\n";
+      }
     }
 
     if(

src/ansi-c/ansi_c_language.cpp

@@ -76,7 +76,6 @@ bool ansi_c_languaget::parse(
   ansi_c_parser.set_message_handler(get_message_handler());
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
-  ansi_c_parser.Float128_type = config.ansi_c.Float128_type;
   ansi_c_parser.cpp98=false; // it's not C++
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;

src/ansi-c/ansi_c_parser.h

@@ -28,16 +28,15 @@ class ansi_c_parsert:public parsert
 public:
   ansi_c_parse_treet parse_tree;
 
-  ansi_c_parsert():
-    tag_following(false),
-    asm_block_following(false),
-    parenthesis_counter(0),
-    mode(modet::NONE),
-    cpp98(false),
-    cpp11(false),
-    for_has_scope(false),
-    ts_18661_3_Floatn_types(false),
-    Float128_type(false)
+  ansi_c_parsert()
+    : tag_following(false),
+      asm_block_following(false),
+      parenthesis_counter(0),
+      mode(modet::NONE),
+      cpp98(false),
+      cpp11(false),
+      for_has_scope(false),
+      ts_18661_3_Floatn_types(false)
   {
   }
 
@@ -84,9 +83,6 @@ class ansi_c_parsert:public parsert
   // ISO/IEC TS 18661-3:2015
   bool ts_18661_3_Floatn_types;
 
-  // Does the compiler version emulated provide _Float128?
-  bool Float128_type;
-
   typedef ansi_c_identifiert identifiert;
   typedef ansi_c_scopet scopet;
 

src/ansi-c/scanner.l

@@ -565,7 +565,7 @@ void ansi_c_scanner_init()
                     return make_identifier();
                 }
 
-"_Float128"     { if(PARSER.Float128_type)
+"_Float128"     { if(PARSER.ts_18661_3_Floatn_types)
                   { loc(); return TOK_GCC_FLOAT128; }
                   else
                     return make_identifier();

src/cpp/cpp_parser.cpp

@@ -25,7 +25,6 @@ bool cpp_parsert::parse()
     config.cpp.cpp_standard==configt::cppt::cpp_standardt::CPP11 ||
     config.cpp.cpp_standard==configt::cppt::cpp_standardt::CPP14;
   ansi_c_parser.ts_18661_3_Floatn_types=false;
-  ansi_c_parser.Float128_type = false;
   ansi_c_parser.in=in;
   ansi_c_parser.mode=mode;
   ansi_c_parser.set_file(get_file());

src/goto-cc/gcc_mode.cpp

@@ -539,7 +539,9 @@ int gcc_modet::doit()
   const auto gcc_float128_minor_version =
     config.ansi_c.arch == "x86_64" ? 3u : 5u;
 
-  config.ansi_c.Float128_type =
+  // __float128 exists (as a typedef) since gcc 4.5 everywhere,
+  // and since 4.3 on x86_64
+  config.ansi_c.gcc__float128_type =
     gcc_version.flavor == gcc_versiont::flavort::GCC &&
     gcc_version.is_at_least(4u, gcc_float128_minor_version);
 

src/util/config.cpp

@@ -948,7 +948,7 @@ bool configt::set(const cmdlinet &cmdline)
   }
 
   if(ansi_c.preprocessor == ansi_ct::preprocessort::GCC)
-    ansi_c.Float128_type = true;
+    ansi_c.gcc__float128_type = true;
 
   set_arch(arch);