diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-15 23:12:10 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-15 23:12:10 +0200 |
| commit | a1c535b67ea8d66caa771a7a360c11990ff9c461 (patch) | |
| tree | 6e2cd1a1a985d0becf713285a2f2c02f99bc6631 /mppa_k1c | |
| parent | 98afe356cbad770511d243be8382a661e3ffe64e (diff) | |
| download | compcert-kvx-a1c535b67ea8d66caa771a7a360c11990ff9c461.tar.gz compcert-kvx-a1c535b67ea8d66caa771a7a360c11990ff9c461.zip | |
notrap cases
Diffstat (limited to 'mppa_k1c')
| -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). |