-
Notifications
You must be signed in to change notification settings - Fork 273
Some goto-cc regression tests fail when native compiler is clang-6.0 #2370
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Labels
Comments
I also repeated these tests with clang-3.9, the oldest Clang readily available to me, and found the MMX2 test does not fail, but the gcc_builtins4 and ts18661 tests fail in the same way. |
BTW, is this now fixed? |
No, all three failures are as described still |
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 15, 2022
Our C front-end seeks to conform to whatever interpretation of the C standard the underlying host C compiler has. To avoid incompatibilities as documented in diffblue#2370, run regression tests using both Clang and GCC, if available on a particular system.
3 tasks
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 15, 2022
…ration The preprocessor variant is only relevant for c_preprocess, and isn't actually set by goto-cc (which does not use c_preprocess). Fixes: diffblue#2370
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 15, 2022
Our C front-end seeks to conform to whatever interpretation of the C standard the underlying host C compiler has. To avoid incompatibilities as documented in diffblue#2370, run regression tests using both Clang and GCC, if available on a particular system.
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 16, 2022
…ration The preprocessor variant is only relevant for c_preprocess, and isn't actually set by goto-cc (which does not use c_preprocess). Fixes: diffblue#2370
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 16, 2022
Our C front-end seeks to conform to whatever interpretation of the C standard the underlying host C compiler has. To avoid incompatibilities as documented in diffblue#2370, run regression tests using both Clang and GCC, if available on a particular system.
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 26, 2022
…ration The preprocessor variant is only relevant for c_preprocess, and isn't actually set by goto-cc (which does not use c_preprocess). Fixes: diffblue#2370
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 26, 2022
Our C front-end seeks to conform to whatever interpretation of the C standard the underlying host C compiler has. To avoid incompatibilities as documented in diffblue#2370, run regression tests using both Clang and GCC, if available on a particular system.
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Feb 26, 2022
Our C front-end seeks to conform to whatever interpretation of the C standard the underlying host C compiler has. To avoid incompatibilities as documented in diffblue#2370, run regression tests using both Clang and GCC, if available on a particular system.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Failing tests:
regression/ansi-c/MMX2
:regression/ansi-c/gcc_builtins4
:STATIC_ASSERT(__builtin_classify_type((_Bool)0)==4)
fails. Someone expected Clang would classify_Bool
as a logical rather than an integer type, which may be true for some Clangs, but evidently not 6.0, at least not 6.0 + glibc-2.27 (if libc is even responsible for defining_Bool
). Need to check which compilers classify it which way.regression/cbmc/ts18661_typedefs
: conflicting type modifiers when trying to overwrite a builtin type (_Float128
) with a typedef. This is expected, as cbmc doesn't usegcc_versiont
yet to check what the native compiler defines -- when it does, it should mimic Clang's support or otherwise for_Float128
et al.The text was updated successfully, but these errors were encountered: