diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-09-24 12:48:02 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-09-24 12:48:02 +0200 |
| commit | 4d5a6d22a6e10c30bae0b19fb6059a5c6e8de2fa (patch) | |
| tree | 65c3122bca3d1ae7e12c4eb999062523f327249f /mppa_k1c/Asmblockgenproof.v | |
| parent | 1f46c2ef4d9080357f37ccb6aa9847ecb8def582 (diff) | |
| download | compcert-kvx-4d5a6d22a6e10c30bae0b19fb6059a5c6e8de2fa.tar.gz compcert-kvx-4d5a6d22a6e10c30bae0b19fb6059a5c6e8de2fa.zip | |
relecture
Diffstat (limited to 'mppa_k1c/Asmblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 13 |
1 files changed, 1 insertions, 12 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 79a51d16..c2a609c9 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1087,7 +1087,7 @@ Proof. right. split. omega. split. auto. rewrite <- ATPC in H5. econstructor; eauto. congruence. -Admitted. +Qed. Lemma transf_initial_states: forall st1, MB.initial_state prog st1 -> @@ -1132,15 +1132,4 @@ Proof. - exact step_simulation. Qed. -(* -Theorem transf_program_correct: - forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). -Proof. - eapply forward_simulation_star with (measure := measure). - apply senv_preserved. - eexact transf_initial_states. - eexact transf_final_states. - exact step_simulation. -Qed. *) - End PRESERVATION. |