CBMC fails to co-exist with GCC 13 about cbmc HOT 10 CLOSED

Consider invoking it as goto-gcc (note the extra g).

from cbmc.

Nope... still fails with:

rodchap@f4d4889dcf6d arrays % goto-gcc --function ctcc_harness -DCBMC -o ar.goto ar.c
/opt/gcc-13.1.0-aarch64/lib/gcc/aarch64-apple-darwin21/13.1.0/include/stddef.h:433:1: error: syntax error before '__float128'
   __float128 __max_align_f128 __attribute__((__aligned__(__alignof(__float128))));
PARSING ERROR

from cbmc.

It seems that goto-cc predefines _Float128 but not __float128

The latter is expected by GCC's stddef.h when APPLE , aarch64 are defined and STDC_VERSION >= 201112

from cbmc.

I will try to reproduce - we have support for __float128 conditional on what compiler family and version we believe we are running under. Apparently we are messing something up (possibly because we assume clang when on macOS). I suppose you have GCC 13 installed via brew?

from cbmc.

No... it's from here: https://github.com/simonjwright/distributing-gcc/releases/tag/gcc-13.2.0-aarch64
This includes the Ada compiler.

from cbmc.

I will try to reproduce - we have support for __float128 conditional on what compiler family and version we believe we are running under. Apparently we are messing something up (possibly because we assume clang when on macOS). I suppose you have GCC 13 installed via brew?

We'll need to enable a few more types when on ARM. GCC has these as well, it's not just clang.

from cbmc.

We'll need to enable a few more types when on ARM. GCC has these as well, it's not just clang.

#8319 fixes __float128; I don't know which other types we might need to add? (__float80 is not supported by GCC it seems.)

from cbmc.

#8319 fixes __float128; I don't know which other types we might need to add? (__float80 is not supported by GCC it seems.)

We also need to check __fp16.

from cbmc.

We also need to check __fp16.

Hmm, yes, but that one we haven't yet got any support for. We need to figure out whether we can use the same conditions for enabling it as we do for __bf16.

from cbmc.

__fp16 support will be added by #8323.

from cbmc.