diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-10-05 15:52:58 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-10-05 15:52:58 +0200 |
| commit | 26ddb90280b45e92d90eead89edb237f2922824a (patch) | |
| tree | ff18b31abdbb97133f9708ca085467f25758e507 /x86/Asm.v | |
| parent | e9c738e3bd156f68905968e25c70ec796d3119c4 (diff) | |
| download | compcert-kvx-26ddb90280b45e92d90eead89edb237f2922824a.tar.gz compcert-kvx-26ddb90280b45e92d90eead89edb237f2922824a.zip | |
Support Cygwin 64 bits
- Add support for the Win64 ABI to the x86_64 port
- Update vararg support to handle Win64 conventions
- Configure support for x86_64-cygwin64
Diffstat (limited to 'x86/Asm.v')
| -rw-r--r-- | x86/Asm.v | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -279,6 +279,7 @@ Inductive instruction: Type := | Pmaxsd (rd: freg) (r2: freg) | Pminsd (rd: freg) (r2: freg) | Pmovb_rm (rd: ireg) (a: addrmode) + | Pmovq_rf (rd: ireg) (r1: freg) | Pmovsq_mr (a: addrmode) (rs: freg) | Pmovsq_rm (rd: freg) (a: addrmode) | Pmovsb @@ -998,6 +999,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmaxsd _ _ | Pminsd _ _ | Pmovb_rm _ _ + | Pmovq_rf _ _ | Pmovsq_rm _ _ | Pmovsq_mr _ _ | Pmovsb |