diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-09-19 17:40:38 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-09-19 17:40:38 +0200 |
| commit | 2e2e6eec5f1e929db4d822024e301e1373bb7877 (patch) | |
| tree | 7683a7b09e7f41a28014f28d19b94fc905f6ffda /mppa_k1c/Asmblockgenproof.v | |
| parent | 191305d4cfc1416dd50080c93a7c3e16768934b4 (diff) | |
| download | compcert-kvx-2e2e6eec5f1e929db4d822024e301e1373bb7877.tar.gz compcert-kvx-2e2e6eec5f1e929db4d822024e301e1373bb7877.zip | |
return_address suite
Diffstat (limited to 'mppa_k1c/Asmblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 0476e76a..92d813b2 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -479,14 +479,17 @@ Proof. generalize (transf_function_no_overflow _ _ H0). omega. intros. apply Pregmap.gso; auto. Qed. +*) (** Existence of return addresses *) Lemma return_address_exists: - forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> + forall b f sg ros c, b.(MB.exit) = Some (MBcall sg ros) -> is_tail (b :: c) f.(MB.fn_code) -> exists ra, return_address_offset f c ra. Proof. - intros. eapply Asmgenproof0.return_address_exists; eauto. + intros. eapply Asmblockgenproof0.return_address_exists; eauto. +Admitted. +(* - intros. exploit transl_instr_label; eauto. destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. - intros. monadInv H0. @@ -496,7 +499,8 @@ Proof. constructor. apply is_tail_cons. apply (storeind_ptr_label GPR8 GPR12 (fn_retaddr_ofs f0) x). - exact transf_function_no_overflow. Qed. - *) +*) + (** * Proof of semantic preservation *) (** Semantic preservation is proved using simulation diagrams |