summaryrefslogtreecommitdiff
path: root/ia32/Machregs.v
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-04-29 07:51:00 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-04-29 07:51:00 +0000
commitfbdff974fe7d2040c25dee1d35781f7e70d87d6c (patch)
tree14f112a70481f467e581ca59136eed42601ce725 /ia32/Machregs.v
parente1fc4beb37252b6248c0e0ca4cf5ec00a45190bf (diff)
Revert suppression of __builtin_{read,write}_reversed for x86 and ARM,
for compatibility with earlier CompCert versions. But don't use them in PackedStructs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2216 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Machregs.v')
-rw-r--r--ia32/Machregs.v11
1 files changed, 9 insertions, 2 deletions
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index a2f3c3e..31ea8ee 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -101,6 +101,11 @@ Definition destroyed_by_cond (cond: condition): list mreg :=
Definition destroyed_by_jumptable: list mreg :=
nil.
+Local Open Scope string_scope.
+
+Definition builtin_write16_reversed := ident_of_string "__builtin_write16_reversed".
+Definition builtin_write32_reversed := ident_of_string "__builtin_write32_reversed".
+
Definition destroyed_by_builtin (ef: external_function): list mreg :=
match ef with
| EF_memcpy sz al =>
@@ -109,6 +114,10 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
| EF_vstore Mfloat32 => X7 :: nil
| EF_vstore_global (Mint8unsigned|Mint8signed) _ _ => AX :: nil
| EF_vstore_global Mfloat32 _ _ => X7 :: nil
+ | EF_builtin id sg =>
+ if ident_eq id builtin_write16_reversed
+ || ident_eq id builtin_write32_reversed
+ then CX :: DX :: nil else nil
| _ => nil
end.
@@ -131,8 +140,6 @@ Definition mregs_for_operation (op: operation): list (option mreg) * option mreg
| _ => (nil, None)
end.
-Local Open Scope string_scope.
-
Definition builtin_negl := ident_of_string "__builtin_negl".
Definition builtin_addl := ident_of_string "__builtin_addl".
Definition builtin_subl := ident_of_string "__builtin_subl".