Skip to content

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

Closed
smowton opened this issue Jun 20, 2018 · 3 comments
Closed

Some goto-cc regression tests fail when native compiler is clang-6.0 #2370

smowton opened this issue Jun 20, 2018 · 3 comments

Comments

@smowton
Copy link
Contributor

smowton commented Jun 20, 2018

Failing tests:

regression/ansi-c/MMX2:

/usr/lib/llvm-6.0/lib/clang/6.0.0/include/emmintrin.h: In function '_mm_avg_epu8':
/usr/lib/llvm-6.0/lib/clang/6.0.0/include/emmintrin.h:2280:1: error: operator `+' not defined for types `unsigned short int __attribute__((vector_size (16l*sizeof(unsigned short int))))' and `signed int'

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 use gcc_versiont yet to check what the native compiler defines -- when it does, it should mimic Clang's support or otherwise for _Float128 et al.

@smowton
Copy link
Contributor Author

smowton commented Jun 20, 2018

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.

@kroening
Copy link
Member

BTW, is this now fixed?

@smowton
Copy link
Contributor Author

smowton commented Aug 20, 2018

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.
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
Projects
None yet
Development

No branches or pull requests

3 participants