diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-29 16:12:40 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-29 16:12:40 +0100 |
commit | f72f1e1bdee98a2fecffd2d0a4beb5e70b650ab0 (patch) | |
tree | 010b5c0cbf71eefeebde9101f4ffba126283f61c | |
parent | 0dc6f0aadfa95c722324b10c56768900760337a0 (diff) | |
parent | 10462d01d7ed4585cece61f756f12d2978593b1a (diff) | |
download | compcert-kvx-f72f1e1bdee98a2fecffd2d0a4beb5e70b650ab0.tar.gz compcert-kvx-f72f1e1bdee98a2fecffd2d0a4beb5e70b650ab0.zip |
Merge remote-tracking branch 'origin/mppa-jumptable' into mppa-jumptable
-rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 2a238c7c..63f4c136 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1383,7 +1383,10 @@ Proof. rewrite H7. simpl extract_ctl. simpl. Simpl. rewrite <- H1. unfold Mach.label in H14. unfold label. rewrite H14. eapply A.
econstructor; eauto.
eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen.
- { admit. }
+ { assert (destroyed_by_jumptable = R62 :: R63 :: nil) by auto. rewrite H2 in H0. simpl in H0. inv H0.
+ destruct (preg_eq r' GPR63). subst. contradiction.
+ destruct (preg_eq r' GPR62). subst. contradiction.
+ destruct r'; Simpl. }
discriminate.
+ (* MBreturn *)
destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
@@ -1419,7 +1422,7 @@ Proof. generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. eauto.
eapply agree_exten; eauto. intros. Simpl.
discriminate.
-Admitted.
+Qed.
Definition mb_remove_first (bb: MB.bblock) :=
{| MB.header := MB.header bb; MB.body := tail (MB.body bb); MB.exit := MB.exit bb |}.
|