diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-05 10:48:03 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-05 10:48:03 +0100 |
| commit | cd69b24565713610d0ea5a613f4871af6e18e9d4 (patch) | |
| tree | 83b17653996bdacfa64b529a542e8269d30461ac /mppa_k1c/PostpassSchedulingproof.v | |
| parent | e9859d89510e6593c83f954b8b9580fff0dd51f4 (diff) | |
| download | compcert-kvx-cd69b24565713610d0ea5a613f4871af6e18e9d4.tar.gz compcert-kvx-cd69b24565713610d0ea5a613f4871af6e18e9d4.zip | |
No more axiom remaining in PostpassScheduling.v (but still a couple remaining in Asmblockdeps)
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 2ecb494d..f969e5b4 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -38,18 +38,6 @@ Proof. eapply H1; eauto. Qed. -Lemma verified_schedule_builtin_idem (ge: Genv.t fundef unit) (fn: function): - forall bb ef args res lbb, - exit bb = Some (PExpand (Pbuiltin ef args res)) -> - verified_schedule bb = OK lbb -> - lbb = bb :: nil. -Proof. - intros. exploit builtin_body_nil; eauto. intros. - rewrite verified_schedule_single_inst in H0; auto. - - inv H0. auto. - - unfold size. rewrite H. rewrite H1. simpl. auto. -Qed. - Lemma exec_body_app: forall l l' ge rs m rs'' m'', exec_body ge (l ++ l') rs m = Next rs'' m'' -> |