diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-11-26 07:38:20 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-11-26 07:38:20 +0100 |
| commit | e2341e779ca6bf734b9ed103156949db588fbbdc (patch) | |
| tree | abb56db58e15dcb5d7598e1accf11f7c334f52ec /backend/Duplicateproof.v | |
| parent | afcda39ab5d9aaf9dcce0d7ea9fc50acc9d318ed (diff) | |
| download | compcert-kvx-e2341e779ca6bf734b9ed103156949db588fbbdc.tar.gz compcert-kvx-e2341e779ca6bf734b9ed103156949db588fbbdc.zip | |
Duplicateproof: minor edit
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 9d56e86f..39b7a353 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -344,15 +344,16 @@ Proof. intros. inv H. exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF). eexists. split. - - econstructor. + - econstructor; eauto. + eapply (Genv.init_mem_transf_partial TRANSL); eauto. + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. symmetry. eapply match_program_main. eauto. - + exploit function_ptr_translated; eauto. + destruct f. * monadInv TRANSF. rewrite <- H3. symmetry; eapply transf_function_preserves. assumption. * monadInv TRANSF. assumption. - - constructor; eauto. constructor. apply transf_fundef_correct; auto. + - constructor; eauto. + + constructor. + + apply transf_fundef_correct; auto. Qed. Theorem transf_final_states: |