Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

emitting .eabi_attribute on ARM #461

Closed
monniaux opened this issue Nov 11, 2022 · 1 comment
Closed

emitting .eabi_attribute on ARM #461

monniaux opened this issue Nov 11, 2022 · 1 comment

Comments

@monniaux
Copy link
Contributor

monniaux commented Nov 11, 2022

Certain embedded toolchains (for assembling and linking) for ARM assume that if a file contains no eabi attribute for floating-point, then it uses soft float. Furthermore, the linker checks that all modules have the same soft/hard float ABI settings. Since CompCert does not emit this attribute, this prevents linking CompCert's output with libraries compiled for hard float.

Solution: emit

  .eabi_attribute Tag_ABI_VFP_args, 1

for hard float parameters (0 for soft float, 3 to say there are no floating-point parameters anyway in this file so it's compatible with both).

See https://reviews.llvm.org/D49993

gcc does set this attribute (instead of printing Tag_ABI_VFP_args it prints its numeric value, 28)

@xavierleroy
Copy link
Contributor

Thanks for the tip. Should be fixed by 1d14f7a .

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants