goblint / cil

C Intermediate Language
https://goblint.github.io/cil/
Other
136 stars 20 forks source link

Support for `ARM64` architectures that have `long double` as 64bit #118

Closed michael-schwarz closed 1 year ago

michael-schwarz commented 2 years ago

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:

This is urgently needed as we have some students with recent versions of OS X in the practical course at TUM.

sim642 commented 1 year ago

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
michael-schwarz commented 1 year ago

Yes!

michael-schwarz commented 1 year ago

There is #119, but one would have to add support for that to Goblint.

sim642 commented 1 year ago

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.

michael-schwarz commented 1 year ago

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.