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/Conventions1.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/Conventions1.v')
| -rw-r--r-- | mppa_k1c/Conventions1.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v index 42905b30..6bb616c8 100644 --- a/mppa_k1c/Conventions1.v +++ b/mppa_k1c/Conventions1.v @@ -40,7 +40,7 @@ Definition is_callee_save (r: mreg): bool := end. Definition int_caller_save_regs := - R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 + R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R9 :: R32 :: R33 :: R34 :: R35 :: R36 :: R37 :: R38 :: R39 :: R40 :: R41 :: R42 :: R43 :: R44 :: R45 :: R46 :: R47 :: R48 :: R49 :: R50 :: R51 :: R52 :: R53 :: R54 :: R55 :: R56 :: R57 :: R58 :: R59 :: R60 :: R61 |