diff options
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 27 |
1 files changed, 21 insertions, 6 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index aac7772c..79b7ca1a 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -252,10 +252,11 @@ Proof. inv H. + (* Internal function *) inv TRANSF. - rename H0 into MF. - eapply dupmap_entrypoint in MF as ENTRY. - eapply dupmap_correct in MF as DMC. unfold match_cfg in DMC. - apply DMC in ENTRY as DMC'. destruct DMC' as [ib [CENTRY MI]]. + rename H0 into TRANSF. + eapply dupmap_entrypoint in TRANSF as ENTRY. + eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. + apply DMC in ENTRY as DMC'. + destruct DMC' as [ib [CENTRY MI]]; clear DMC. eexists; left; eexists; split. * eapply exec_function_internal. erewrite preserv_fnstacksize; eauto. @@ -264,8 +265,22 @@ Proof. all: erewrite preserv_fnparams; eauto. constructor. + (* External function *) - admit. - - admit. + inv TRANSF. + eexists; left; eexists; split. + * eapply exec_function_external. + eapply external_call_symbols_preserved. + eapply senv_preserved. eauto. + * econstructor; eauto. + - (* Returnstate *) + inv H. inv STACKS. inv H1. + eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. + remember DUPLIC as ODUPLIC; clear HeqODUPLIC. + apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC. + eexists; left; eexists; split. + + eapply exec_return. + + econstructor; eauto. + eapply code_right_assoc; eauto. + constructor. Admitted. Local Hint Resolve plus_one star_refl: core. |