From f06898fc9711736b3b2e373941d762f90d8fa253 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 4 Sep 2019 12:05:59 +0200 Subject: Duplicate: exec_function_external et exec_return --- backend/Duplicateproof.v | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'backend/Duplicateproof.v') diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 69fc41ae..40e7493d 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -1,6 +1,6 @@ (** Correctness proof for code duplication *) Require Import AST Linking Errors Globalenvs Smallstep. -Require Import Coqlib Maps. +Require Import Coqlib Maps Events. Require Import RTL Duplicate. Definition match_prog (p tp: program) := @@ -182,9 +182,13 @@ Proof. erewrite transf_function_fnparams; eauto. econstructor; eauto. constructor. (* exec_function_external *) - - admit. + - monadInv TRANSF. eexists. split. + + econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor. assumption. (* exec_return *) - - admit. + - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split. + + constructor. + + inv H1. constructor; assumption. Admitted. Theorem transf_program_correct: -- cgit