Failing tests on M1-Arm64 on develop #5828
Description
CBMC version: 5.23.0 (cbmc-5.21.3-exp-254-g268f8864e)
Operating system: macOS 11.0
Exact command line resulting in the issue: cbmc/regression/ansi-c/gcc_version1 $ clang gcc-5.c
What behaviour did you expect: Binary is compiled without issue.
What happened instead: Clang fails with error: __float128 is not supported on this target.
Running the regression test-suite under make on macOS Big Sur, on top of the new m1 platform is causing some of the regression tests to fail. Specifically, regression/ansi-c/gcc-version1 and regression/ansi-c/gcc-version2 are failing.
On closer inspection, invoking clang directly on the binary gives me this:
fotiskoutoulakis@Fotiss-Mac-mini gcc_version1 % clang gcc-5.c
gcc-5.c:10:1: error: __float128 is not supported on this target
__float128 f128;
^Querying clang about version and target produces this:
fotiskoutoulakis@Fotiss-Mac-mini gcc_version1 % clang -v
Apple clang version 12.0.0 (clang-1200.0.32.27)
Target: arm64-apple-darwin20.1.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/binI have two questions/remarks:
- It seems like it is assumed that
__float128is going to be supported on other platforms, but this looks like an unsafe assumption. Should we change the test/deactivate it on some platforms? - It looks like a subset of the tests in
regression/ansi-care markedgcc-only. Do we need to run them under MacOS where the default compiler is going to beclang/llvm? If not we may need to make changes to our CI infrastructure, as we currently do run them under themacOS-cmakeandmacOS-makebuilds.