Test failures with GCC 14 about cbmc HOT 4 CLOSED

Hi @lzaoral

Thanks for reporting this. Would it be possible for you to test this with GCC 13 or earlier and the latest CBMC?

from cbmc.

For the first issue it would seem that __builtin_shufflevector is now also supported by GCC, and not just Clang. We added support for it in de4557f, but now seemingly need to remove the restriction to Clang.

For the second issue we need to add support for bf16 constants as seen here:

typedef __decltype(0.0bf16) __bfloat16_t;

from cbmc.

For the first issue it would seem that __builtin_shufflevector is now also supported by GCC, and not just Clang. We added support for it in de4557f, but now seemingly need to remove the restriction to Clang.

Fixed in #8170.

For the second issue we need to add support for bf16 constants as seen here:

typedef __decltype(0.0bf16) __bfloat16_t;

Done in #8169.

from cbmc.

All relevant PRs have now been merged, closing.

from cbmc.