diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-04 16:23:25 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-04 16:23:25 +0100 |
| commit | 993d6692b722bf366aadbed3b36f7ef51de6cafd (patch) | |
| tree | 282223798ed33e93f8b3ef06149bd810a5e4c53a /mppa_k1c/PostpassSchedulingproof.v | |
| parent | baeaefa7e1c24e38b3ed41bd894db45057d0eb2b (diff) | |
| download | compcert-kvx-993d6692b722bf366aadbed3b36f7ef51de6cafd.tar.gz compcert-kvx-993d6692b722bf366aadbed3b36f7ef51de6cafd.zip | |
Proof of transf_exec_control \o/
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 08f6f1be..0ab62578 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -709,8 +709,11 @@ Proof. pose symbol_address_preserved.
exploreInst; simpl; auto; try congruence.
- unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
-Admitted.
-
+ - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+ - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+ - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+ - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+Qed.
Lemma transf_exec_bblock:
forall f tf bb rs m,
|