aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblock.v
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2019-03-18 16:13:22 +0100
committerCyril SIX <cyril.six@kalray.eu>2019-03-18 16:13:22 +0100
commitaa400a9eed939578917810d32ef4fcf79944729d (patch)
tree73015b7cf217f2ed172829ee9a68084ff26d4b16 /mppa_k1c/Asmblock.v
parent4d25fa871e9960d6e01dd4b63acdf367fee5431b (diff)
downloadcompcert-kvx-aa400a9eed939578917810d32ef4fcf79944729d.tar.gz
compcert-kvx-aa400a9eed939578917810d32ef4fcf79944729d.zip
The parent frame pointer is now R17 instead of R14
Diffstat (limited to 'mppa_k1c/Asmblock.v')
-rw-r--r--mppa_k1c/Asmblock.v5
1 files changed, 3 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 5279bd29..4757b9fc 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -85,7 +85,8 @@ Module Pregmap := EMap(PregEq).
(** Conventional names for stack pointer ([SP]) and return address ([RA]). *)
Notation "'SP'" := GPR12 (only parsing) : asm.
-Notation "'FP'" := GPR14 (only parsing) : asm.
+Notation "'FP'" := GPR17 (only parsing) : asm.
+Notation "'MFP'" := R17 (only parsing) : asm.
Notation "'GPRA'" := GPR16 (only parsing) : asm.
Notation "'RTMP'" := GPR32 (only parsing) : asm.
@@ -1445,7 +1446,7 @@ Definition preg_of (r: mreg) : preg :=
match r with
| R0 => GPR0 | R1 => GPR1 | R2 => GPR2 | R3 => GPR3 | R4 => GPR4
| R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R8 => GPR8 | R9 => GPR9
- | R10 => GPR10 | R11 => GPR11 (* | R12 => GPR12 | R13 => GPR13 | *) | R14 => GPR14
+ | R10 => GPR10 | R11 => GPR11 (* | R12 => GPR12 | R13 => GPR13 | 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 | R29 => GPR29