_FloatX support based on gcc version

kroening · kroening · commit e040723285d6 · 2018-06-06T08:05:41.000+01:00
diff --git a/appveyor.yml b/appveyor.yml
@@ -74,6 +74,7 @@ test_script:
     rmdir /s /q ansi-c\Universal_characters1
     rmdir /s /q ansi-c\function_return1
     rmdir /s /q ansi-c\gcc_attributes7
+    rmdir /s /q ansi-c\gcc_version1
     rmdir /s /q ansi-c\struct6
     rmdir /s /q ansi-c\struct7
     rmdir /s /q cbmc\Malloc23
diff --git a/regression/ansi-c/float_constant1/main.c b/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)));
diff --git a/regression/ansi-c/gcc_types_compatible_p1/main.c b/regression/ansi-c/gcc_types_compatible_p1/main.c
@@ -67,8 +67,8 @@ STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot) *, int *));
 STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot), typeof (janette)));
 STATIC_ASSERT(__builtin_types_compatible_p(__int128, signed __int128));
 
-#ifndef __clang__
 // clang doesn't have these
+#if !defined(__clang__) && __GNUC__ >= 7
 #if defined(__x86_64__) || defined(__i386__)
 STATIC_ASSERT(__builtin_types_compatible_p(__float128, _Float128));
 #endif
@@ -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
 
diff --git a/regression/ansi-c/gcc_version1/fake-gcc-4 b/regression/ansi-c/gcc_version1/fake-gcc-4
@@ -0,0 +1,4 @@
+#!/bin/sh
+
+gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=4 -D __GNUC_MINOR__=9 -D __GNUC_PATCHLEVEL__=1 $*
+
diff --git a/regression/ansi-c/gcc_version1/fake-gcc-7 b/regression/ansi-c/gcc_version1/fake-gcc-7
@@ -0,0 +1,4 @@
+#!/bin/sh
+
+gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=7 -D __GNUC_MINOR__=0 -D __GNUC_PATCHLEVEL__=0 $*
+
diff --git a/regression/ansi-c/gcc_version1/gcc-4.c b/regression/ansi-c/gcc_version1/gcc-4.c
@@ -0,0 +1,2 @@
+typedef double _Float64;
+
diff --git a/regression/ansi-c/gcc_version1/gcc-7.c b/regression/ansi-c/gcc_version1/gcc-7.c
@@ -0,0 +1,2 @@
+_Float64 some_var;
+
diff --git a/regression/ansi-c/gcc_version1/test-gcc-4.desc b/regression/ansi-c/gcc_version1/test-gcc-4.desc
@@ -0,0 +1,7 @@
+CORE
+gcc-4.c
+--native-compiler ./fake-gcc-4
+^EXIT=0$
+^SIGNAL=0$
+--
+^CONVERSION ERROR$
diff --git a/regression/ansi-c/gcc_version1/test-gcc-7.desc b/regression/ansi-c/gcc_version1/test-gcc-7.desc
@@ -0,0 +1,7 @@
+CORE
+gcc-7.c
+--native-compiler ./fake-gcc-7
+^EXIT=0$
+^SIGNAL=0$
+--
+^CONVERSION ERROR$
diff --git a/src/ansi-c/ansi_c_language.cpp b/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.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
   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.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
   ansi_c_scanner_init();
 
   bool result=ansi_c_parser.parse();
diff --git a/src/ansi-c/ansi_c_parser.h b/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),
+    ts_18661_3_Floatn_types(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 ts_18661_3_Floatn_types;
+
   typedef ansi_c_identifiert identifiert;
   typedef ansi_c_scopet scopet;
 
diff --git a/src/ansi-c/scanner.l b/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.ts_18661_3_Floatn_types)
                   { 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.ts_18661_3_Floatn_types)
                   { 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.ts_18661_3_Floatn_types)
                   { 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.ts_18661_3_Floatn_types)
                   { 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.ts_18661_3_Floatn_types)
                   { 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.ts_18661_3_Floatn_types)
+                  { loc(); return TOK_GCC_FLOAT128; }
+                  else
+                    return make_identifier();
+                }
+
+"_Float128x"    { if(PARSER.ts_18661_3_Floatn_types)
                   { loc(); return TOK_GCC_FLOAT128X; }
                   else
                     return make_identifier();
diff --git a/src/cpp/cpp_parser.cpp b/src/cpp/cpp_parser.cpp
@@ -24,6 +24,7 @@ bool cpp_parsert::parse()
   ansi_c_parser.cpp11=
     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.in=in;
   ansi_c_parser.mode=mode;
   ansi_c_parser.set_file(get_file());
diff --git a/src/goto-cc/gcc_mode.cpp b/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.ts_18661_3_Floatn_types=true;
+
   // -fshort-double makes double the same as float
   if(cmdline.isset("fshort-double"))
     config.ansi_c.double_width=config.ansi_c.single_width;
diff --git a/src/util/config.cpp b/src/util/config.cpp
@@ -742,6 +742,7 @@ bool configt::set(const cmdlinet &cmdline)
 
   ansi_c.single_precision_constant=false;
   ansi_c.for_has_scope=true; // C99 or later
+  ansi_c.ts_18661_3_Floatn_types=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;
@@ -1139,8 +1140,9 @@ 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,
+  // ts_18661_3_Floatn_types are not architectural features,
+  // and thus not stored in namespace
 
   ansi_c.alignment=unsigned_from_ns(ns, "alignment");
 
diff --git a/src/util/config.h b/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 ts_18661_3_Floatn_types; // 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();

-Original file line number
+Diff line change
@@ @@ -0,0 +1,4 @@ @@
 +#!/bin/sh
++
 +gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=4 -D __GNUC_MINOR__=9 -D __GNUC_PATCHLEVEL__=1 $*
++