diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-11-21 09:04:39 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-11-21 09:04:39 +0100 |
| commit | 1d14f7a805e376f1adb1236acb0c7afbbe9cb208 (patch) | |
| tree | 693141068f314e634a6805cf3a86d44c9535a38b | |
| parent | 5b80eaa2d5141eb4f157d3296b8d92e022386777 (diff) | |
| download | compcert-1d14f7a805e376f1adb1236acb0c7afbbe9cb208.tar.gz compcert-1d14f7a805e376f1adb1236acb0c7afbbe9cb208.zip | |
Emit the Tag_ABI_VFP attribute appropriate to the calling conventions used
Fixes: #461
| -rw-r--r-- | arm/TargetPrinter.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index b6362ca9..953bc4f4 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -579,7 +579,12 @@ struct | _ -> "armv7"); fprintf oc " .fpu %s\n" (if Opt.vfpv3 then "vfpv3-d16" else "vfpv2"); - fprintf oc " .%s\n" (if !Clflags.option_mthumb then "thumb" else "arm"); + fprintf oc " .eabi_attribute Tag_ABI_VFP_args, %d\n" + (match Configuration.abi with + | "hardfloat" -> 1 + | _ -> 0); + fprintf oc " .%s\n" + (if !Clflags.option_mthumb then "thumb" else "arm"); if !Clflags.option_g then begin section oc Section_text; cfi_section oc |