From da19abe85bbb68d3cf3af7bc0d9073a9275520ae Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Wed, 16 May 2018 09:49:55 +0100
Subject: [PATCH] Tolerate TS 18661 (_Float32 et al) types

Because we currently claim GCC 4.2.1 support, but also define the TS 18661 floating point types,
we confuse Glibc 2.27+, which checks for GCC >= 7.0 and otherwise defines the types itself.
In the long run we should either upgrade our support to GCC 7.0 standard, or else stop providing
these types and simply ask users interested in these types to use Glibc 2.27 or provide their own
headers; in the meantime this workaround permits us to avoid crashing whenever math.h is included.
---
 regression/cbmc/ts18661_typedefs/main.c    |  9 +++++++++
 regression/cbmc/ts18661_typedefs/test.desc |  8 ++++++++
 src/ansi-c/ansi_c_convert_type.cpp         | 19 ++++++++++++++++---
 3 files changed, 33 insertions(+), 3 deletions(-)
 create mode 100644 regression/cbmc/ts18661_typedefs/main.c
 create mode 100644 regression/cbmc/ts18661_typedefs/test.desc

diff --git a/regression/cbmc/ts18661_typedefs/main.c b/regression/cbmc/ts18661_typedefs/main.c
new file mode 100644
index 00000000000..06ef87fbc72
--- /dev/null
+++ b/regression/cbmc/ts18661_typedefs/main.c
@@ -0,0 +1,9 @@
+typedef float _Float32;
+typedef double _Float32x;
+typedef double _Float64;
+typedef long double _Float64x;
+typedef long double _Float128;
+typedef long double _Float128x;
+
+int main(int argc, char** argv) {
+}
diff --git a/regression/cbmc/ts18661_typedefs/test.desc b/regression/cbmc/ts18661_typedefs/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/ts18661_typedefs/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
index 0ac703eebee..aa541a9d6e8 100644
--- a/src/ansi-c/ansi_c_convert_type.cpp
+++ b/src/ansi-c/ansi_c_convert_type.cpp
@@ -344,9 +344,22 @@ void ansi_c_convert_typet::write(typet &type)
        gcc_float64_cnt+gcc_float64x_cnt+
        gcc_float128_cnt+gcc_float128x_cnt>=2)
     {
-      error().source_location=source_location;
-      error() << "conflicting type modifiers" << eom;
-      throw 0;
+      // Temporary workaround for our glibc versions that try to define TS 18661
+      // types (for example, typedef float _Float32). This can be removed once
+      // upgrade cbmc's GCC support to at least 7.0 (when glibc will expect us
+      // to provide these types natively), or disable parsing them ourselves
+      // when our preprocessor stage claims support <7.0.
+      if(c_storage_spec.is_typedef)
+      {
+        warning().source_location = source_location;
+        warning() << "ignoring typedef for TS 18661 (_FloatNNx) type. If you need these, try using goto-cc instead." << eom;
+      }
+      else
+      {
+        error().source_location=source_location;
+        error() << "conflicting type modifiers" << eom;
+        throw 0;
+      }
     }
 
     // _not_ the same as float, double, long double