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)
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
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_argsit prints its numeric value, 28)