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/Machregs.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/Machregs.v')
| -rw-r--r-- | mppa_k1c/Machregs.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 09a6a237..d30cdbbd 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -41,7 +41,7 @@ Require Import Op. (* FIXME - no R31 *) Inductive mreg: Type := (* Allocatable General Purpose regs. *) - | R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R8 | R9 + | R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R9 (* R10 to R14 are reserved *) | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 | R24 | R25 | R26 | R27 | R28 | R29 | R30 | R32 | R33 | R34 | R35 | R36 | R37 | R38 | R39 @@ -54,7 +54,7 @@ Proof. decide equality. Defined. Global Opaque mreg_eq. Definition all_mregs := - R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 + R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R9 :: R15 :: R16 :: R17 :: R18 :: R19 :: R20 :: R21 :: R22 :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 :: R30 :: R32 :: R33 :: R34 :: R35 :: R36 :: R37 :: R38 :: R39 @@ -86,7 +86,7 @@ Module IndexedMreg <: INDEXED_TYPE. Definition index (r: mreg): positive := match r with R0 => 1 | R1 => 2 | R2 => 3 | R3 => 4 | R4 => 5 - | R5 => 6 | R6 => 7 | R7 => 8 | R8 => 9 | R9 => 10 + | R5 => 6 | R6 => 7 | R7 => 8 | R9 => 10 | R15 => 16 | R16 => 17 | R17 => 18 | R18 => 19 | R19 => 20 | R20 => 21 | R21 => 22 | R22 => 23 | R23 => 24 | R24 => 25 | R25 => 26 | R26 => 27 | R27 => 28 | R28 => 29 | R29 => 30 @@ -113,7 +113,7 @@ Local Open Scope string_scope. Definition register_names := ("R0", R0) :: ("R1", R1) :: ("R2", R2) :: ("R3", R3) :: ("R4", R4) - :: ("R5", R5) :: ("R6", R6) :: ("R7", R7) :: ("R8", R8) :: ("R9", R9) + :: ("R5", R5) :: ("R6", R6) :: ("R7", R7) :: ("R9", R9) :: ("R15", R15) :: ("R16", R16) :: ("R17", R17) :: ("R18", R18) :: ("R19", R19) :: ("R20", R20) :: ("R21", R21) :: ("R22", R22) :: ("R23", R23) :: ("R24", R24) :: ("R25", R25) :: ("R26", R26) :: ("R27", R27) :: ("R28", R28) :: ("R29", R29) @@ -175,7 +175,7 @@ Definition destroyed_by_setstack (ty: typ): list mreg := nil. (* Definition destroyed_at_function_entry: list mreg := R30 :: nil. *) Definition destroyed_at_function_entry: list mreg := nil. -Definition temp_for_parent_frame: mreg := R8. (* FIXME - and R9 ?? *) +Definition temp_for_parent_frame: mreg := R9. (* FIXME - and R8 ?? *) Definition destroyed_at_indirect_call: list mreg := nil. (* R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: R16 :: R17 :: nil. *) |