From 1d14f7a805e376f1adb1236acb0c7afbbe9cb208 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 21 Nov 2022 09:04:39 +0100
Subject: Emit the Tag_ABI_VFP attribute appropriate to the calling conventions
 used

Fixes: #461
---
 arm/TargetPrinter.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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
-- 
cgit