diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-20 10:23:43 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-20 10:23:43 +0200 |
| commit | 1153ff98a18c1730b17444ce3dc4953b886cf9f0 (patch) | |
| tree | d1327d79693ebab026131af6ddc42122df4fd91f | |
| parent | 16e932213b7cad49e2942ae93434398cf4a72c59 (diff) | |
| download | compcert-kvx-1153ff98a18c1730b17444ce3dc4953b886cf9f0.tar.gz compcert-kvx-1153ff98a18c1730b17444ce3dc4953b886cf9f0.zip | |
m
| -rw-r--r-- | mppa_k1c/Machblockgenproof.v | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v index f0618cfe..64eeadbc 100644 --- a/mppa_k1c/Machblockgenproof.v +++ b/mppa_k1c/Machblockgenproof.v @@ -704,10 +704,16 @@ Lemma cfi_dist_end_block i c: (* TODO: raccourcir *) (exists cfi, trans_inst i = MB_cfi cfi) -> dist_end_block_code (i :: c) = 0. Proof. - pose t'. + unfold dist_end_block_code. intro H. destruct H as [cfi H]. - destruct i;simpl in H;try(congruence). - + destruct (e (Mcall s s0) c) as [bl Ht]. + destruct i;simpl in H;try(congruence); ( + remember (trans_code _) as bl; + rewrite <- is_trans_code_inv in Heqbl; + inversion Heqbl; subst; simpl in * |- *; try (reflexivity || congruence)). +Qed. +(* + - simpl. + destruct (e (Mcall s s0) c) as [bl Ht]. unfold dist_end_block_code, trans_code; simpl. rewrite Ht. unfold trans_code_rev, add_to_code; simpl. @@ -743,7 +749,7 @@ Proof. unfold trans_code_rev, add_to_code; simpl. destruct bl; vm_compute; eauto. Qed. - +*) Theorem transf_program_correct: forward_simulation (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog). Proof. |