_FloatX support based on gcc version

Author: Daniel Kroening

regression/ansi-c/float_constant1/main.c

@@ -12,7 +12,7 @@ STATIC_ASSERT(0X.0p+1f == 0);
 
 // 32-bit, 64-bit and 128-bit constants, GCC proper only,
 // clang doesn't have it
-#if defined(__GNUC__) && !defined(__clang__)
+#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ >= 7
 STATIC_ASSERT(__builtin_types_compatible_p(_Float32, __typeof(1.0f32)));
 STATIC_ASSERT(__builtin_types_compatible_p(_Float64, __typeof(1.0f64)));
 STATIC_ASSERT(__builtin_types_compatible_p(_Float128, __typeof(1.0f128)));

regression/ansi-c/gcc_types_compatible_p1/main.c

@@ -95,16 +95,19 @@ STATIC_ASSERT(!__builtin_types_compatible_p(long int, int));
 STATIC_ASSERT(!__builtin_types_compatible_p(long long int, long int));
 STATIC_ASSERT(!__builtin_types_compatible_p(unsigned, signed));
 
-#ifndef __clang__
+STATIC_ASSERT(!__builtin_types_compatible_p(__int128, unsigned __int128));
+
 // clang doesn't have these
+#if !defined(__clang__)
+#if __GNUC__ >= 7
 STATIC_ASSERT(!__builtin_types_compatible_p(_Float32, float));
 STATIC_ASSERT(!__builtin_types_compatible_p(_Float64, double));
 STATIC_ASSERT(!__builtin_types_compatible_p(_Float32x, float));
 STATIC_ASSERT(!__builtin_types_compatible_p(_Float64x, double));
+#endif
 STATIC_ASSERT(!__builtin_types_compatible_p(__float80, double));
 STATIC_ASSERT(!__builtin_types_compatible_p(__float128, long double));
 STATIC_ASSERT(!__builtin_types_compatible_p(__float128, double));
-STATIC_ASSERT(!__builtin_types_compatible_p(__int128, unsigned __int128));
 #endif
 #endif
 

src/ansi-c/ansi_c_language.cpp

@@ -75,6 +75,7 @@ bool ansi_c_languaget::parse(
   ansi_c_parser.in=&codestr;
   ansi_c_parser.set_message_handler(get_message_handler());
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
+  ansi_c_parser.Floatn=config.ansi_c.Floatn;
   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;
@@ -196,6 +197,7 @@ bool ansi_c_languaget::to_expr(
   ansi_c_parser.in=&i_preprocessed;
   ansi_c_parser.set_message_handler(get_message_handler());
   ansi_c_parser.mode=config.ansi_c.mode;
+  ansi_c_parser.Floatn=config.ansi_c.Floatn;
   ansi_c_scanner_init();
 
   bool result=ansi_c_parser.parse();

src/ansi-c/ansi_c_parser.h

@@ -35,7 +35,8 @@ class ansi_c_parsert:public parsert
     mode(modet::NONE),
     cpp98(false),
     cpp11(false),
-    for_has_scope(false)
+    for_has_scope(false),
+    Floatn(false)
   {
   }
 
@@ -77,6 +78,9 @@ class ansi_c_parsert:public parsert
   // in C99 and upwards, for(;;) has a scope
   bool for_has_scope;
 
+  // ISO/IEC TS 18661-3:2015
+  bool Floatn;
+
   typedef ansi_c_identifiert identifiert;
   typedef ansi_c_scopet scopet;
 

src/ansi-c/scanner.l

@@ -459,36 +459,31 @@ void ansi_c_scanner_init()
                     return make_identifier();
                 }
 
-"_Float16"      { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
+"_Float16"      { if(PARSER.Floatn)
                   { loc(); return TOK_GCC_FLOAT16; }
                   else
                     return make_identifier();
                 }
 
-"_Float32"      { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
+"_Float32"      { if(PARSER.Floatn)
                   { loc(); return TOK_GCC_FLOAT32; }
                   else
                     return make_identifier();
                 }
 
-"_Float32x"     { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
+"_Float32x"     { if(PARSER.Floatn)
                   { loc(); return TOK_GCC_FLOAT32X; }
                   else
                     return make_identifier();
                 }
 
-"_Float64"      { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
+"_Float64"      { if(PARSER.Floatn)
                   { loc(); return TOK_GCC_FLOAT64; }
                   else
                     return make_identifier();
                 }
 
-"_Float64x"     { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
+"_Float64x"     { if(PARSER.Floatn)
                   { loc(); return TOK_GCC_FLOAT64X; }
                   else
                     return make_identifier();
@@ -501,16 +496,20 @@ void ansi_c_scanner_init()
                     return make_identifier();
                 }
 
-"__float128" |
-"_Float128"     { // clang doesn't have it
+"__float128"    { // clang doesn't have it
                   if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
                   { loc(); return TOK_GCC_FLOAT128; }
                   else
                     return make_identifier();
                 }
 
-"_Float128x"    { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
+"_Float128"     { if(PARSER.Floatn)
+                  { loc(); return TOK_GCC_FLOAT128; }
+                  else
+                    return make_identifier();
+                }
+
+"_Float128x"    { if(PARSER.Floatn)
                   { loc(); return TOK_GCC_FLOAT128X; }
                   else
                     return make_identifier();

src/goto-cc/gcc_mode.cpp

@@ -525,6 +525,11 @@ int gcc_modet::doit()
   if(cmdline.isset("-fsingle-precision-constant"))
     config.ansi_c.single_precision_constant=true;
 
+  // ISO/IEC TS 18661-3:2015 support was introduced with gcc 7.0
+  if(gcc_version.flavor==gcc_versiont::flavort::GCC &&
+     gcc_version.is_at_least(7))
+    config.ansi_c.Floatn=true;
+
   // -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

@@ -738,6 +738,7 @@ bool configt::set(const cmdlinet &cmdline)
 
   ansi_c.single_precision_constant=false;
   ansi_c.for_has_scope=true; // C99 or later
+  ansi_c.Floatn=false;
   ansi_c.c_standard=ansi_ct::default_c_standard();
   ansi_c.endianness=ansi_ct::endiannesst::NO_ENDIANNESS;
   ansi_c.os=ansi_ct::ost::NO_OS;
@@ -1135,8 +1136,8 @@ void configt::set_from_symbol_table(
 
   ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
   ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
-  // for_has_scope, single_precision_constant, rounding_mode not
-  // stored in namespace
+  // for_has_scope, single_precision_constant, rounding_mode, Floatn
+  // not architectural features, and thus not stored in namespace
 
   ansi_c.alignment=unsigned_from_ns(ns, "alignment");
 

src/util/config.h

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