fix up __float128 and _Float128 support #4629
Conversation
kroening
requested review from
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
|
I thought we were explicitly testing different Clang and GCC versions in some build configurations. Did I get this wrong? |
|
@tautschnig This fix here is independent of that, meaning we did the wrong thing in response to a particular version. Independently, the current behavior is that goto-cc does check the gcc version, whereas cbmc does not. CBMC uses a default, which works for gcc >=4.3 and <7.0, i.e., this will fail with gcc >= 7. We could/should consider checking in cbmc as well. |
|
@kroening This is failing CI on CodeBuild (Linux). |
|
@tautschnig Yes, this is to be expected. I am investigating whether enabling _Float128 by default will break users who have gcc <7.0. |
|
@tautschnig Unfortunately, math.h in gcc-6 does the following: |
|
#4636 is meant to prepare for b). |
kroening
force-pushed
the
__float128
branch
2 times, most recently
from
89468e3 to
d724523
Compare
|
Now there! |
|
BTW, checking the gcc version will cost some performance. A viable alternative is to simply assume a version of gcc >=7, which is the case now for all major distributions. |
src/ansi-c/gcc_version.cpp
Outdated
| // ISO/IEC TS 18661-3:2015 support was introduced with gcc 7.0 | ||
| if( | ||
| gcc_version.flavor == gcc_versiont::flavort::GCC && | ||
| gcc_version.is_at_least(7)) |
There was a problem hiding this comment.
Nit pick: below there's always an explicit u suffix, so should this be used here as well? I'd just like to see consistency.
_Float128 is a keyword, defined in ISO/IEC TS 18661-3:2015. It's a typedef since gcc 6.0. It's a genuine keyword since gcc 7.0. clang does not offer it. __float128 is a typedef in gcc since 4.3/4.5, depending on architecture. __float128 is a keyword in clang. This PR attempts to clean this up.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: c5b0bd1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/111867719
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: c937b3f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/111868662
_Float128is a keyword, defined in ISO/IEC TS 18661-3:2015, and exists sincegcc 7.0. clang does not offer it.
__float128is a typedef in gcc since 4.3/4.5, depending on architecture.__float128is a keyword in clang.This PR attempts to clean this up.