diff options
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 30 |
1 files changed, 29 insertions, 1 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 94ec84bf..4595eb83 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -226,6 +226,7 @@ Proof. + inv STAR; try discriminate. eexists; split. eauto. econstructor; eauto. + - inv MI. inv STAR. + inv H5. eexists; split. @@ -237,8 +238,35 @@ Proof. eapply plus_one. eapply exec_Ireturn; eauto. erewrite <- preserv_fnstacksize; eauto. eauto. econstructor; eauto. + - inv MI. + inv STAR. + + inv H5. + pose symbols_preserved as SYMPRES. + destruct ros. + * simpl in H. apply functions_translated in H. + destruct H as (tf & cunit & TFUN & GFIND & LO). + eexists; split. + eapply plus_one. eapply exec_Icall; eauto. + apply function_sig_translated. assumption. + admit. + (* TODO ?? *) + * admit. + + admit. - admit. - - admit. + - inv MI. pose symbols_preserved as SYMPRES. + inv STAR. + + inv H5. eexists; split. + eapply plus_one. eapply exec_Ibuiltin; eauto. + eapply eval_builtin_args_preserved; eauto. + eapply external_call_symbols_preserved; eauto. eapply senv_preserved. + econstructor; eauto. + + inv H5. eexists; split. + eapply plus_trans. eauto. + eapply plus_one. eapply exec_Ibuiltin; eauto. + eapply eval_builtin_args_preserved; eauto. + eapply external_call_symbols_preserved; eauto. eapply senv_preserved. + eauto. econstructor; eauto. +(* Icond *) - admit. - admit. Admitted. |