New _Float32 type conflicts with libc Ubuntu GLIBC 2.27-3ubuntu1

[smowton]

Ubuntu glibc version 2.27-3ubuntu1, file bits/floatn-common.h contains:

#  if !__GNUC_PREREQ (7, 0) || defined __cplusplus
typedef float _Float32;
#  endif

As of the recent past, cbmc supports the _Float32 and similar types (an extension to C supported by gcc (https://www.iso.org/standard/65615.html / https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html))

Unfortunately cbmc only claims compatibility with GCC 4.2.1 (in c_preprocess.cpp), so libc tries to define _Float32 itself, and so anything that includes floatn-common.h fails to compile.

Simply altering c_preprocess.cpp to claim GCC 7 compatibility solves this particular problem, but exposes another: if GCC 4.4+ is detected, the same libc directs fpclassify to __builtin_fpclassify, which we don't support. No doubt there are other featurelets we don't have that GCC has gained between version 4.2 and 7.0.

Possible choices:

1. Tolerate the redundant typedef
2. Raise our support to GCC 7.0; provide __builtin_fpclassify and whatever else we need to
3. Revert our support for _Float32; require anyone wanting those types to use a new enough libc that is defines them, or include their own support header that defines those types appropriately.

[tautschnig]

I think we should go for option 2. My rationale is that right now using goto-cc + cbmc vs. cbmc directly will yield different results. (May I actually ask you to confirm this on the example you are looking at?)

[smowton]

On my system goto-cc behaves just like cbmc modified to declare GCC version 7.0 (unsurprisingly, since GCC 7 is currently my default version, and goto-cc uses the real GCC for preprocessing). Thus goto-cc does not have this problem, but does have the fpclassify problem. That we hadn't noticed the fpclassify problem before presumably indicates a shortcoming of the goto-cc testsuite.

[TGWDB]

Closing as this appears to not longer be producible (using regression example from #2185 although the associated code seems to have moved or changed since then). If you believe this is erroneous of have a working example please reopen and post the example.