From a1c535b67ea8d66caa771a7a360c11990ff9c461 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 15 Apr 2020 23:12:10 +0200 Subject: notrap cases --- mppa_k1c/lib/RTLpathLivegen.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'mppa_k1c') 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). -- cgit