summaryrefslogtreecommitdiff
path: root/ia32
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-08-22 09:28:08 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-08-22 09:28:08 +0000
commit261ef24f7fd2ef443f73c468b9b1fa496371f3bf (patch)
tree42f33af682816dc9762f1b41a9dc04dc0526354f /ia32
parent9096c5c513aba868970a3e792fd5237d74547c05 (diff)
Fixed 2 errors in revised builtin_vstore.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2035 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32')
-rw-r--r--ia32/PrintAsm.ml5
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;