Fixed 2 errors in revised builtin_vstore.

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

1 files changed, 3 insertions, 2 deletions

diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index d6de2d1..9664be8 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -399,7 +399,8 @@ let print_builtin_vstore_common oc chunk addr src tmp =
   | Mint32, IR src ->
       fprintf oc "	movl	%a, %a\n" ireg src addressing addr
   | Mfloat32, FR src ->
-      fprintf oc "	cvtsd2ss %a, %a\n" freg src addressing addr
+      fprintf oc "      cvtsd2ss %a, %%xmm7\n" freg src;
+      fprintf oc "      movss   %%xmm7, %a\n" addressing addr
   | (Mfloat64 | Mfloat64al32), FR src ->
       fprintf oc "	movsd	%a, %a\n" freg src addressing addr
   | _ ->
@@ -411,7 +412,7 @@ let print_builtin_vstore oc chunk args =
   | [IR addr; src] ->
       print_builtin_vstore_common oc chunk
                  (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src
-                 (if addr = ECX then EDX else ECD)
+                 (if addr = ECX then EDX else ECX)
   | _ ->
       assert false
   end;