diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-02-26 14:48:59 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-02-26 14:48:59 +0000 |
| commit | a745efa7f07a10cec625b9c302eb0196b7bfaefb (patch) | |
| tree | af32acc8865cf704b63bd27b8eb21da6b29d83b6 /powerpc/Asm.v | |
| parent | 26fcc4dbd92f367ecb20f4457cdf887eea0b6568 (diff) | |
Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >= 0' and 'x < 0'.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@999 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 69085aa..63f0232 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -759,7 +759,7 @@ Definition ireg_of (r: mreg) : ireg := match r with | R3 => GPR3 | R4 => GPR4 | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R8 => GPR8 | R9 => GPR9 | R10 => GPR10 - | R13 => GPR13 | R14 => GPR14 | R15 => GPR15 | R16 => GPR16 + | R14 => GPR14 | R15 => GPR15 | R16 => GPR16 | R17 => GPR17 | R18 => GPR18 | R19 => GPR19 | R20 => GPR20 | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24 | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 |