aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/eabi/Conventions1.v
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc/eabi/Conventions1.v')
-rw-r--r--powerpc/eabi/Conventions1.v9
1 files changed, 7 insertions, 2 deletions
diff --git a/powerpc/eabi/Conventions1.v b/powerpc/eabi/Conventions1.v
index b25f2a5d..652f4a1b 100644
--- a/powerpc/eabi/Conventions1.v
+++ b/powerpc/eabi/Conventions1.v
@@ -55,8 +55,13 @@ Definition int_temporaries := IT1 :: IT2 :: nil.
Definition float_temporaries := FT1 :: FT2 :: FT3 :: nil.
-Definition temporaries :=
- R IT1 :: R IT2 :: R FT1 :: R FT2 :: R FT3 :: nil.
+Definition temporary_regs := int_temporaries ++ float_temporaries.
+
+Definition temporaries := List.map R temporary_regs.
+
+Definition destroyed_at_move_regs: list mreg := nil.
+
+Definition destroyed_at_move := List.map R destroyed_at_move_regs.
Definition dummy_int_reg := R3. (**r Used in [Coloring]. *)
Definition dummy_float_reg := F1. (**r Used in [Coloring]. *)