diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-29 14:54:05 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-29 14:54:05 +0100 |
| commit | 10462d01d7ed4585cece61f756f12d2978593b1a (patch) | |
| tree | 9291e27304fbc198e7a488bb5408e7d95b761d48 | |
| parent | e9a05f4ca3157a88a03f71ab31ef59bd96650142 (diff) | |
| download | compcert-kvx-10462d01d7ed4585cece61f756f12d2978593b1a.tar.gz compcert-kvx-10462d01d7ed4585cece61f756f12d2978593b1a.zip | |
Finition de la preuve de Asmblockgenproof
| -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 |}.
|