diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-24 14:30:57 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-24 14:34:59 +0200 |
| commit | 271a6f98809fbeac6cb04fb29fccbcf9c1e18335 (patch) | |
| tree | 219a059313829de5f54cdbff0d99a8652ad9f7e0 /ia32/Machregs.v | |
| parent | abec89a558d952dc1f4f39bda6a8e69a426a8dc0 (diff) | |
| download | compcert-kvx-271a6f98809fbeac6cb04fb29fccbcf9c1e18335.tar.gz compcert-kvx-271a6f98809fbeac6cb04fb29fccbcf9c1e18335.zip | |
ia32: add support for __builtin_bswap64 + a bit of DWARF for x86-64
__builtin_bswap64 is now available both in 32 and 64-bit mode.
The DWARF bit is the numbering of registers in ia32/Asmexpand.ml.
Diffstat (limited to 'ia32/Machregs.v')
| -rw-r--r-- | ia32/Machregs.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ia32/Machregs.v b/ia32/Machregs.v index c3cdaefb..741081a6 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -240,6 +240,8 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list (Some AX :: Some DX :: nil, Some DX :: Some AX :: nil) else if string_dec name "__builtin_va_start" then (Some DX :: nil, nil) + else if (negb Archi.ptr64) && string_dec name "__builtin_bswap64" then + (Some AX :: Some DX :: nil, Some DX :: Some AX :: nil) else (nil, nil) | _ => (nil, nil) |