CBMC fails to co-exist with GCC 13

[rod-chapman]

CBMC version: 6.0.0-alpha
Operating system: macOS
Exact command line resulting in the issue: any goto-cc command
What behaviour did you expect: success
What happened instead:

CBMC fails to work with GCC 13

rodchap@f4d4889dcf6d arrays % make TARGET=ctcc
rm -f *.goto
goto-cc --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
make: *** [ar.goto] Error 1

This is rather annoying, since I have to disable my standard GCC 13 install whenever I want to use CBMC.

[kroening]

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

[rod-chapman]

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

[rod-chapman]

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

[tautschnig]

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?

[rod-chapman]

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

[kroening]

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.

[tautschnig]

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.)

[kroening]

#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.

[tautschnig]

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.