From e2341e779ca6bf734b9ed103156949db588fbbdc Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 26 Nov 2019 07:38:20 +0100 Subject: Duplicateproof: minor edit --- backend/Duplicateproof.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'backend/Duplicateproof.v') 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: -- cgit