diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-09-04 12:05:59 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-09-04 12:05:59 +0200 |
| commit | f06898fc9711736b3b2e373941d762f90d8fa253 (patch) | |
| tree | 8268676bc97280225885f387f0747c7d421f8143 /backend/Duplicateproof.v | |
| parent | 4a5f1db8abe7831649f6f15178958e0c57955a25 (diff) | |
| download | compcert-kvx-f06898fc9711736b3b2e373941d762f90d8fa253.tar.gz compcert-kvx-f06898fc9711736b3b2e373941d762f90d8fa253.zip | |
Duplicate: exec_function_external et exec_return
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 10 |
1 files changed, 7 insertions, 3 deletions
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: |