Closed
Description
CBMC version: 5.24
Operating system: macOS 10.15 / Ubuntu 20.04
Exact command line resulting in the issue: goto-cc simd.c
where simd.c contains the program
#include <immintrin.h>
#include <assert.h>
int main() {
__m128i values = _mm_setr_epi32(0x1234, 0x2345, 0x3456, 0x4567);
int val1 = _mm_extract_epi32(values, 0);
assert(val1 == 0x1234);
return 0;
}
What behaviour did you expect: Successful compilation.
What happened instead:
Got the following error on macOS 10.15:
/Library/Developer/CommandLineTools/usr/lib/clang/12.0.0/include/avx512fintrin.h: In function '_mm512_sqrt_pd':
/Library/Developer/CommandLineTools/usr/lib/clang/12.0.0/include/avx512fintrin.h:1503:1: error: wrong number of function arguments: expected 1, but got 2
return (__m512d)__builtin_ia32_sqrtpd512((__v8df)__A,
CONVERSION ERROR
and the following error on Ubuntu 20.04:
/usr/lib/gcc/x86_64-linux-gnu/9/include/avx512fintrin.h: In function '_mm512_reduce_add_epi32':
/usr/lib/gcc/x86_64-linux-gnu/9/include/avx512fintrin.h:15496:1: error: in expression '__builtin_shuffle(__T6, { 2, 3, 0, 1 })':
conversion from 'signed int' to '__gcc_v4si': implicit conversion not permitted
__MM512_REDUCE_OP (+);
CONVERSION ERROR