diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-01-22 17:51:08 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-01-22 17:51:08 +0100 |
| commit | f58bec109f818aacd04a27bb08fa9bbe64dccaf9 (patch) | |
| tree | 35e5e6a1381992b0565e994349d5122e94f290f0 /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 6acefcbbc51aa7d2edb7b2098a5b15d06e742604 (diff) | |
| download | compcert-kvx-f58bec109f818aacd04a27bb08fa9bbe64dccaf9.tar.gz compcert-kvx-f58bec109f818aacd04a27bb08fa9bbe64dccaf9.zip | |
Léger avancement PostpassSchedulingproof.v
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index f1eb26f1..5aedbf04 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -230,6 +230,12 @@ Proof. exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL).
exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ).
erewrite transf_exec_bblock in H2; eauto.
+ inv BBEQ. rewrite H3 in H2.
+ eexists. split.
+ eapply plus_one. econstructor; eauto.
+ eapply find_bblock_tail. (* TODO - continue in this direction ? *)
+ all: destruct TODO.
+(* OLD VERSION
exploit concat_exec_straight; eauto.
{ inv BBEQ. erewrite <- H3. eauto. }
{ destruct TODO. }
@@ -238,7 +244,7 @@ Proof. eexists. split.
+ eapply exec_straight_steps_1; eauto.
monadInv EQ. destruct (zlt _ _). discriminate. monadInv EQ1. omega.
- + econstructor; eauto.
+ + econstructor; eauto. *)
- destruct TODO.
- destruct TODO.
Admitted.
|