From 261ef24f7fd2ef443f73c468b9b1fa496371f3bf Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 22 Aug 2012 09:28:08 +0000 Subject: Fixed 2 errors in revised builtin_vstore. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2035 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/PrintAsm.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'ia32/PrintAsm.ml') diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index d6de2d1b..9664be86 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; -- cgit