Merge pull request #2296 from smowton/smowton/fix/restore-float128

Daniel Kroening · web-flow · commit c5de7bab6c8c · 2018-06-07T12:42:16.000+01:00
Restore _Float128 support by default
diff --git a/regression/ansi-c/gcc_version1/fake-gcc-4 b/regression/ansi-c/gcc_version1/fake-gcc-4
@@ -1,4 +1,4 @@
 #!/bin/sh
 
-gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=4 -D __GNUC_MINOR__=9 -D __GNUC_PATCHLEVEL__=1 $*
+gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=4 -D __GNUC_MINOR__=2 -D __GNUC_PATCHLEVEL__=1 "$@"
 
diff --git a/regression/ansi-c/gcc_version1/fake-gcc-5 b/regression/ansi-c/gcc_version1/fake-gcc-5
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=5 -D __GNUC_MINOR__=0 -D __GNUC_PATCHLEVEL__=0 "$@"
diff --git a/regression/ansi-c/gcc_version1/fake-gcc-7 b/regression/ansi-c/gcc_version1/fake-gcc-7
@@ -1,4 +1,4 @@
 #!/bin/sh
 
-gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=7 -D __GNUC_MINOR__=0 -D __GNUC_PATCHLEVEL__=0 $*
+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
@@ -1,2 +1,8 @@
-typedef double _Float64;
+// None of these types should be defined when emulating gcc-4:
 
+typedef float _Float32;
+typedef double _Float32x;
+typedef double _Float64;
+typedef long double _Float64x;
+typedef long double _Float128;
+typedef long double _Float128x;
diff --git a/regression/ansi-c/gcc_version1/gcc-5.c b/regression/ansi-c/gcc_version1/gcc-5.c
@@ -0,0 +1,9 @@
+// These types should *not* be provided when emulating gcc-5:
+typedef float _Float32;
+typedef double _Float32x;
+typedef double _Float64;
+typedef long double _Float64x;
+typedef long double _Float128x;
+
+// But this type should:
+_Float128 f128;
diff --git a/regression/ansi-c/gcc_version1/gcc-7.c b/regression/ansi-c/gcc_version1/gcc-7.c
@@ -1,2 +1,7 @@
-_Float64 some_var;
-
+// All these types should be provided when emulating gcc-7:
+_Float32 f32;
+_Float32x f32x;
+_Float64 f64;
+_Float64x f64x;
+_Float128 f128;
+_Float128x f128x;
diff --git a/regression/ansi-c/gcc_version1/test-gcc-5.desc b/regression/ansi-c/gcc_version1/test-gcc-5.desc
@@ -0,0 +1,7 @@
+CORE
+gcc-5.c
+--native-compiler ./fake-gcc-5
+^EXIT=0$
+^SIGNAL=0$
+--
+^CONVERSION ERROR$
diff --git a/regression/cbmc/ts18661_typedefs/main.c b/regression/cbmc/ts18661_typedefs/main.c
@@ -1,18 +1,32 @@
-#if defined(__clang__)
-#elif defined(__GNUC__)
+#if defined(__GNUC__) && !defined(__clang__)
+
+#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
+#elif __GNUC_PREREQ(4, FLOAT128_MINOR_VERSION)
+#define HAS_FLOAT128
 #endif
+
 #endif
 
 #ifndef HAS_FLOATN
 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;
+#endif
+
 int main(int argc, char** argv) {
 }
diff --git a/src/ansi-c/ansi_c_language.cpp b/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;
diff --git a/src/ansi-c/ansi_c_parser.h b/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;
 
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
@@ -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();
diff --git a/src/cpp/cpp_parser.cpp b/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());
diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp
@@ -530,6 +530,12 @@ 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;
diff --git a/src/util/config.cpp b/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")
diff --git a/src/util/config.h b/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();

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