diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-02 17:19:15 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:07 +0200 |
| commit | a80a8b9ee92c9dd015d53d8de03b99c0d228d390 (patch) | |
| tree | 962123c4c33a38ae42ba3218f09329349ff3887b /mppa_k1c/Conventions1.v | |
| parent | 917859721f6423b24788ec6219774b5196b02ec1 (diff) | |
| download | compcert-kvx-a80a8b9ee92c9dd015d53d8de03b99c0d228d390.tar.gz compcert-kvx-a80a8b9ee92c9dd015d53d8de03b99c0d228d390.zip | |
MPPA - Started Asm.v + Asmgen.v, commenting out some instructions
Diffstat (limited to 'mppa_k1c/Conventions1.v')
| -rw-r--r-- | mppa_k1c/Conventions1.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v index 400168ab..42905b30 100644 --- a/mppa_k1c/Conventions1.v +++ b/mppa_k1c/Conventions1.v @@ -35,7 +35,7 @@ Require Import AST Machregs Locations. Definition is_callee_save (r: mreg): bool := match r with | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 - | R23 | R24 | R25 | R26 | R27 | R28 | R29 | R30 | R31 => true + | R23 | R24 | R25 | R26 | R27 | R28 | R29 | R30 => true | _ => false end. @@ -50,7 +50,7 @@ Definition float_caller_save_regs := @nil mreg. Definition int_callee_save_regs := R15 :: R16 :: R17 :: R18 :: R19 :: R20 :: R21 :: R22 - :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 :: R30 :: R31 :: nil. + :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 :: R30 :: nil. Definition float_callee_save_regs := @nil mreg. |