diff options
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) |