From be4d6e42dfa287b93b1a35ec820ab2a5aaf8c7ec Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 19 May 2013 09:54:40 +0000 Subject: 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 --- ia32/standard/Conventions1.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'ia32/standard/Conventions1.v') diff --git a/ia32/standard/Conventions1.v b/ia32/standard/Conventions1.v index cae20f6e..e097e855 100644 --- a/ia32/standard/Conventions1.v +++ b/ia32/standard/Conventions1.v @@ -220,7 +220,7 @@ Definition loc_result (s: signature) : list mreg := match s.(sig_res) with | None => AX :: nil | Some Tint => AX :: nil - | Some Tfloat => FP0 :: nil + | Some (Tfloat | Tsingle) => FP0 :: nil | Some Tlong => DX :: AX :: nil end. @@ -261,6 +261,7 @@ Fixpoint loc_arguments_rec | nil => nil | Tint :: tys => S Outgoing ofs Tint :: loc_arguments_rec tys (ofs + 1) | Tfloat :: tys => S Outgoing ofs Tfloat :: loc_arguments_rec tys (ofs + 2) + | Tsingle :: tys => S Outgoing ofs Tsingle :: loc_arguments_rec tys (ofs + 1) | Tlong :: tys => S Outgoing (ofs + 1) Tint :: S Outgoing ofs Tint :: loc_arguments_rec tys (ofs + 2) end. @@ -314,6 +315,9 @@ Proof. destruct H. subst l; split; [omega|congruence]. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. +- destruct H. subst l. split. omega. congruence. + exploit IHtyl; eauto. + destruct l; auto. destruct sl; auto. intuition omega. Qed. Lemma loc_arguments_acceptable: @@ -362,6 +366,7 @@ Proof. destruct H. inv H. simpl typesize. apply Zle_trans with (ofs + 2). omega. apply size_arguments_rec_above. auto. + destruct H. inv H. apply size_arguments_rec_above. auto. Qed. -- cgit