undo parts of diffblue#2185

regression/cbmc/ts18661_typedefs/main.c

@@ -1,9 +1,18 @@
+#if defined(__clang__)
+#elif defined(__GNUC__)
+#if __GNUC__ >= 7
+#define HAS_FLOATN
+#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
 
 int main(int argc, char** argv) {
 }

src/ansi-c/ansi_c_convert_type.cpp

@@ -346,22 +346,9 @@ void ansi_c_convert_typet::write(typet &type)
        gcc_float64_cnt+gcc_float64x_cnt+
        gcc_float128_cnt+gcc_float128x_cnt>=2)
     {
-      // 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;
-      }
+      error().source_location=source_location;
+      error() << "conflicting type modifiers" << eom;
+      throw 0;
     }
 
     // _not_ the same as float, double, long double