Tolerate TS 18661 (_Float32 et al) types

smowton · smowton · commit da19abe85bbb · 2018-05-17T15:26:33.000+01:00
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 &gt;= 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.
diff --git a/regression/cbmc/ts18661_typedefs/main.c 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
@@ -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
@@ -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
