cil
cil copied to clipboard
Support for `ARM64` architectures that have `long double` as 64bit
Currently, we do not have proper support for any architecture were float128 does not have the same size & alignment as long double. Unfortunately, this includes Apple's M1 architecture, which is gaining popularity as Mac users update their machines.
We should thus:
- [ ] Expose
float128as a distinctfkindon machines that have it.
This is urgently needed as we have some students with recent versions of OS X in the practical course at TUM.
I guess this is also why testrungcc/builtin_object_size fails on macos-homebrew-ocaml-4.14-arm64 in opam-repository CI:
# /opt/homebrew/Cellar/gcc/12.2.0/lib/gcc/current/gcc/aarch64-apple-darwin21/12/include/stddef.h:424: Error: float128 only supported on machines where it is an alias (w.r.t. to size and align) of long double: size: 8 align: 8
# Error on A.TYPEDEF (GoblintCil__Errormsg.Error)
# Error: Cabs2cil had some errors
# Fatal error: exception GoblintCil__Errormsg.Error
# make: *** [testrungcc/builtin_object_size] Error 2
Yes!
There is #119, but one would have to add support for that to Goblint.
This needs to be checked in practice such that we can relax the opam package availability constraints again: https://github.com/goblint/cil/commit/5a3b7bb7f4d9b67678826ab7698f8a9048891553. I suppose arm64 might be one, but #110 has a list of others we had to disable. Although all of those contain other failures as well, so probably cannot be re-enabled.
I think if we aim to re-enable tests for other architectures, we would need to wrap some of the tests into #ifdefs, as some features will simply not be available on all architectures.