diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-11 11:51:16 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-11 11:51:16 +0200 |
commit | e73d255ec045983787ed935ad02d31d45353a2b1 (patch) | |
tree | 7a935f55c4c037863e607802c8f557ad13e8ed0b /ia32/Machregs.v | |
parent | 3c605199ab0d096cd66ba671a4e23eac9e79bbc2 (diff) | |
download | compcert-e73d255ec045983787ed935ad02d31d45353a2b1.tar.gz compcert-e73d255ec045983787ed935ad02d31d45353a2b1.zip |
x86-64 MacOS X support
- Avoid absolute addressing for labels, use RIP-relative addressing
- Different, RIP-relative implementation of jump tables
Diffstat (limited to 'ia32/Machregs.v')
-rw-r--r-- | ia32/Machregs.v | 2 |
1 files changed, 1 insertions, 1 deletions
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 |