diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-16 15:06:28 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:08 +0200 |
| commit | 348aa9268bb3f7f2fe4357586a4e1d3181e0c9b3 (patch) | |
| tree | f2b03f61284e350803a7dbd137cce34e106bf22e /mppa_k1c/Conventions1.v | |
| parent | f677664f63ca17c0a514c449f62ad958b5f9eb68 (diff) | |
| download | compcert-kvx-348aa9268bb3f7f2fe4357586a4e1d3181e0c9b3.tar.gz compcert-kvx-348aa9268bb3f7f2fe4357586a4e1d3181e0c9b3.zip | |
MPPA - code cleaning
Diffstat (limited to 'mppa_k1c/Conventions1.v')
| -rw-r--r-- | mppa_k1c/Conventions1.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v index 6bb616c8..68beb560 100644 --- a/mppa_k1c/Conventions1.v +++ b/mppa_k1c/Conventions1.v @@ -32,7 +32,7 @@ Require Import AST Machregs Locations. of callee- and caller-save registers. *) -Definition is_callee_save (r: mreg): bool := +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 => true @@ -90,7 +90,7 @@ Definition is_float_reg (r: mreg) := false. with one integer result. *) Definition loc_result (s: signature) : rpair mreg := - match s.(sig_res) with + match s.(sig_res) with | None => One R0 | Some (Tint | Tany32) => One R0 | Some (Tfloat | Tsingle | Tany64) => One R0 @@ -334,7 +334,10 @@ Proof. cut (forall va tyl rn ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl rn ofs)). unfold OK. eauto. - induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl. - red; simpl; tauto. - destruct ty1. + (* int *) apply A; auto. + induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl. + - red; simpl; tauto. + - destruct ty1. ++ (* int *) apply A; auto. + (* float *) apply A; auto. + (* long *) |