From 271a6f98809fbeac6cb04fb29fccbcf9c1e18335 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 24 Oct 2016 14:30:57 +0200 Subject: 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. --- ia32/Machregs.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'ia32/Machregs.v') 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) -- cgit