diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-04 13:06:52 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-04 13:06:52 +0200 |
| commit | a345b9ff0ff90a3b90b20c13c472d52361ddcea6 (patch) | |
| tree | b3bba6ca9b1a16f1ef6055933c22600303b29523 /scheduling/BTLtoRTLproof.v | |
| parent | f592b3b46908a97e2181f270cf631e9f8d60d726 (diff) | |
| download | compcert-kvx-a345b9ff0ff90a3b90b20c13c472d52361ddcea6.tar.gz compcert-kvx-a345b9ff0ff90a3b90b20c13c472d52361ddcea6.zip | |
builtin case OK, call and tailcall started but not finished
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. |