diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-05 11:26:51 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-05 11:26:51 +0100 |
| commit | 0d709513e08aa36faae2fe3d006e7e4c23aa4aff (patch) | |
| tree | e7a7ee95fc06d7fbb5492741f552bde74732928f | |
| parent | 6c51fda9e503953a4f8ca3e2448b8040158ddc94 (diff) | |
| download | compcert-kvx-0d709513e08aa36faae2fe3d006e7e4c23aa4aff.tar.gz compcert-kvx-0d709513e08aa36faae2fe3d006e7e4c23aa4aff.zip | |
m
| -rw-r--r-- | mppa_k1c/Machblockgen.v | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v index 7206fb51..0a8b2ccd 100644 --- a/mppa_k1c/Machblockgen.v +++ b/mppa_k1c/Machblockgen.v @@ -126,7 +126,8 @@ Inductive is_trans_code: Mach.code -> code -> Prop := is_trans_code c (bh::bl) -> trans_inst i = MB_basic bi -> header bh = nil -> - is_trans_code (i::c) (add_basic bi bh::bl) + is_trans_code (i::c) (add_basic bi bh::bl). +(* Use Tr_end_block instead of: | Tr_empty_bblock c bh bl: is_trans_code c bl -> bh = empty_bblock -> @@ -135,6 +136,7 @@ Inductive is_trans_code: Mach.code -> code -> Prop := is_trans_code c bl -> trans_inst i = MB_cfi bi -> is_trans_code (i::c) (cfi_bblock bi :: bl). +*) Local Hint Resolve Tr_nil Tr_end_block. @@ -149,9 +151,12 @@ Proof. + intros; eapply Tr_add_label; eauto. destruct i; simpl in * |- *; congruence. + intros. remember (header bh0) as hbh0. destruct hbh0 as [|b]. * eapply Tr_add_basic; eauto. - * eapply Tr_add_basic; eauto. eapply Tr_empty_bblock. eauto. reflexivity. - + intros. eapply Tr_cfi. eauto. symmetry in Heqti. eauto. -Qed. (* A FINIR *) + * cutrewrite (add_basic bi empty_bblock = add_to_new_bblock (MB_basic bi)); auto. + rewrite Heqti; eapply Tr_end_block; eauto. + rewrite <- Heqti. + eapply End_basic. + (* + intros. eapply Tr_cfi. eauto. symmetry in Heqti. eauto. *) +Admitted. (* A FINIR *) Local Hint Resolve add_to_code_is_trans_code. |