diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-12 18:17:09 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:07 +0200 |
| commit | e3aed59a6d58f4486da40e0a7a381ea0bf10ba81 (patch) | |
| tree | de1643c22b3268506df583a177637f7cb6ea3a82 /mppa_k1c/Asm.v | |
| parent | e65ce82fa66afa7d4c6b4d664fd583cf12f8ca21 (diff) | |
| download | compcert-kvx-e3aed59a6d58f4486da40e0a7a381ea0bf10ba81.tar.gz compcert-kvx-e3aed59a6d58f4486da40e0a7a381ea0bf10ba81.zip | |
MPPA - Preuve de make_epilogue correct.
ça va un peu plus loin!
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index f5ff7c78..4122ac29 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -1019,7 +1019,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out 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 + | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R9 => GPR9 (*| 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 @@ -1186,6 +1186,7 @@ Definition data_preg (r: preg) : bool := match r with | RA => false | IR GPR31 => false (* FIXME - GPR31 is used as temporary in some instructions.. ??? *) + | IR GPR8 => false (* FIXME - idem *) | IR _ => true | FR _ => true | PC => false |