From 378ac3925503e6efd24cc34796e85d95c031e72d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 13 Sep 2015 11:44:32 +0200 Subject: Use PowerPC 64 bits instructions (when available) for int<->FP conversions. Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence. Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-". --- powerpc/Machregs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc/Machregs.v') diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index a2017dca..e4006523 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -134,7 +134,7 @@ Definition destroyed_by_op (op: operation): list mreg := match op with | Ofloatconst _ => R12 :: nil | Osingleconst _ => R12 :: nil - | Ointoffloat => F13 :: nil + | Ointoffloat | Ointuoffloat => F13 :: nil | _ => nil end. -- cgit From f5bb397acd12292f6b41438778f2df7391d6f2fe Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:26:56 +0200 Subject: bug 17392: remove trailing whitespace in source files --- powerpc/Machregs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc/Machregs.v') diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 20bec532..8d3976f4 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -21,7 +21,7 @@ Require Import Op. (** The following type defines the machine registers that can be referenced as locations. These include: - Integer registers that can be allocated to RTL pseudo-registers ([Rxx]). -- Floating-point registers that can be allocated to RTL pseudo-registers +- Floating-point registers that can be allocated to RTL pseudo-registers ([Fxx]). The type [mreg] does not include special-purpose or reserved -- cgit