Restore _Float128 support by default

_Float128 was exposed by GCC as of version 4.3 (x86-64) to 4.5 (i386 and I think others).
cbmc still makes no effort to imitate a particular GCC version, so I simply enable recognising
the token by default, which used to happen universally; goto-cc on the other hand uses the
new `gcc_versiont` to choose an appropriate behaviour.

This fixes a regression on tests using math.h due to some versions of glibc defining _Float128
conditional on the compiler version, which cbmc and goto-cc now both allow to appear like the
gcc found on the path.

Author: smowton

src/ansi-c/ansi_c_language.cpp

@@ -76,6 +76,7 @@ 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

@@ -36,7 +36,8 @@ class ansi_c_parsert:public parsert
     cpp98(false),
     cpp11(false),
     for_has_scope(false),
-    ts_18661_3_Floatn_types(false)
+    ts_18661_3_Floatn_types(false),
+    Float128_type(false)
   {
   }
 
@@ -81,6 +82,9 @@ 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

@@ -47,11 +47,11 @@ extern int yyansi_cdebug;
 int make_identifier()
 {
   loc();
-  
+
   // deal with universal charater names
   std::string final_base_name;
   final_base_name.reserve(yyleng);
-  
+
   for(const char *p=yytext; *p!=0; p++)
   {
     if(p[0]=='\\' && (p[1]=='u' || p[1]=='U'))
@@ -62,18 +62,18 @@ int make_identifier()
       unsigned letter=hex_to_unsigned(p, digits);
       for(; *p!=0 && digits>0; digits--, p++);
       p--; // go back for p++ later
-      
+
       std::basic_string<unsigned> utf32;
       utf32+=letter;
-      
+
       // turn into utf-8
       std::string utf8_value=utf32_to_utf8(utf32);
       final_base_name+=utf8_value;
     }
     else
       final_base_name+=*p;
   }
-  
+
   if(PARSER.cpp98)
   {
     stack(yyansi_clval).id(ID_symbol);
@@ -503,7 +503,7 @@ void ansi_c_scanner_init()
                     return make_identifier();
                 }
 
-"_Float128"     { if(PARSER.ts_18661_3_Floatn_types)
+"_Float128"     { if(PARSER.Float128_type)
                   { loc(); return TOK_GCC_FLOAT128; }
                   else
                     return make_identifier();

src/cpp/cpp_parser.cpp

@@ -25,6 +25,7 @@ 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

@@ -530,6 +530,13 @@ int gcc_modet::doit()
      gcc_version.is_at_least(7))
     config.ansi_c.ts_18661_3_Floatn_types=true;
 
+  int gcc_float128_minor_version =
+    config.ansi_c.arch == "x86_64" ? 3 : 5;
+
+  config.ansi_c.Float128_type =
+    gcc_version.flavor==gcc_versiont::flavort::GCC &&
+    gcc_version.is_at_least(4, gcc_float128_minor_version);
+
   // -fshort-double makes double the same as float
   if(cmdline.isset("fshort-double"))
     config.ansi_c.double_width=config.ansi_c.single_width;

src/util/config.cpp

@@ -912,6 +912,9 @@ bool configt::set(const cmdlinet &cmdline)
     ansi_c.preprocessor=ansi_ct::preprocessort::GCC;
   }
 
+  if(ansi_c.preprocessor == ansi_ct::preprocessort::GCC)
+    ansi_c.Float128_type = true;
+
   set_arch(arch);
 
   if(os=="windows")

src/util/config.h

@@ -43,6 +43,7 @@ class configt
     bool char_is_unsigned, wchar_t_is_unsigned;
     bool for_has_scope;
     bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015
+    bool Float128_type;
     bool single_precision_constant;
     enum class c_standardt { C89, C99, C11 } c_standard;
     static c_standardt default_c_standard();