diff options
| -rw-r--r-- | mppa_k1c/lib/RTLpathLivegen.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/mppa_k1c/lib/RTLpathLivegen.v b/mppa_k1c/lib/RTLpathLivegen.v index 6a1d7176..80df6e7c 100644 --- a/mppa_k1c/lib/RTLpathLivegen.v +++ b/mppa_k1c/lib/RTLpathLivegen.v @@ -384,8 +384,10 @@ Proof. erewrite eval_operation_preserved; eauto. + (* Iload *) eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto. - + (* Iload notrap1 *) admit. - + (* Iload notrap2 *) admit. + + (* Iload notrap1 *) eapply exec_Iload_notrap1; eauto. + erewrite eval_addressing_preserved; eauto. + + (* Iload notrap2 *) eapply exec_Iload_notrap2; eauto. + erewrite eval_addressing_preserved; eauto. + (* Istore *) eapply exec_Istore; eauto. erewrite eval_addressing_preserved; eauto. + (* Icall *) @@ -411,7 +413,7 @@ Proof. eapply external_call_symbols_preserved; eauto. + (* exec_return *) eapply RTL.exec_return; eauto. -Admitted. +Qed. Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTLpath.semantics tprog). |