diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-12-05 16:35:17 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-12-05 16:35:17 +0100 |
| commit | f9de154cde1974a8fa9afec9ad83653384ec912f (patch) | |
| tree | 855226f565376e5634bb6e525e8ed9424695dd2b /mppa_k1c/Asmblock.v | |
| parent | f136beaf95fda574f120619b0d6b2dba46072032 (diff) | |
| download | compcert-kvx-f9de154cde1974a8fa9afec9ad83653384ec912f.tar.gz compcert-kvx-f9de154cde1974a8fa9afec9ad83653384ec912f.zip | |
Generalizing PostpassScheduling to include bblock splitting
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 912a02d5..c11d043b 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -403,12 +403,16 @@ Definition non_empty_bblockb (body: list basic) (exit: option control): bool := Lemma non_empty_bblock_refl: forall body exit, - non_empty_bblock body exit -> + non_empty_bblock body exit <-> Is_true (non_empty_bblockb body exit). Proof. - intros. destruct body; destruct exit. - all: simpl; auto. - inv H; contradiction. + intros. split. + - destruct body; destruct exit. + all: simpl; auto. intros. inversion H; contradiction. + - destruct body; destruct exit. + all: simpl; auto. + all: intros; try (right; discriminate); try (left; discriminate). + contradiction. Qed. (* Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res, |