From e73d255ec045983787ed935ad02d31d45353a2b1 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 11 Oct 2016 11:51:16 +0200
Subject: x86-64 MacOS X support

- Avoid absolute addressing for labels, use RIP-relative addressing
- Different, RIP-relative implementation of jump tables
---
 ia32/Machregs.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ia32/Machregs.v')

diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index 034fa4bb..c3cdaefb 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -157,7 +157,7 @@ Definition destroyed_by_cond (cond: condition): list mreg :=
   nil.
 
 Definition destroyed_by_jumptable: list mreg :=
-  nil.
+  AX :: DX :: nil.
 
 Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
   match cl with
-- 
cgit