Merge of the float32 branch:

- added RTL type "Tsingle"
- ABI-compatible passing of single-precision floats on ARM and x86


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 7 insertions, 1 deletions

diff --git a/arm/Machregs.v b/arm/Machregs.v
index 50535f0b..d4439efa 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -109,6 +109,12 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
   | _ => nil
   end.
 
+Definition destroyed_by_setstack (ty: typ): list mreg :=
+  match ty with
+  | Tsingle => F6 :: nil
+  | _ => nil
+  end.
+
 Definition destroyed_at_function_entry: list mreg :=
   R12 :: nil.
 
@@ -131,7 +137,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list(
 Global Opaque
     destroyed_by_op destroyed_by_load destroyed_by_store
     destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin
-    destroyed_at_function_entry temp_for_parent_frame
+    destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame
     mregs_for_operation mregs_for_builtin.
 
 (** Two-address operations.  Return [true] if the first argument and