diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-19 09:54:40 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-19 09:54:40 +0000 |
commit | be4d6e42dfa287b93b1a35ec820ab2a5aaf8c7ec (patch) | |
tree | c51b66e9154bc64cf4fd4191251f29d102928841 /ia32/standard/Conventions1.v | |
parent | 60e1fd71c7e97b2214daf574e0f41b55a3e0bceb (diff) | |
download | compcert-be4d6e42dfa287b93b1a35ec820ab2a5aaf8c7ec.tar.gz compcert-be4d6e42dfa287b93b1a35ec820ab2a5aaf8c7ec.zip |
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
Diffstat (limited to 'ia32/standard/Conventions1.v')
-rw-r--r-- | ia32/standard/Conventions1.v | 7 |
1 files changed, 6 insertions, 1 deletions
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. |