diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-17 23:19:16 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-17 23:19:16 +0200 |
| commit | bf443e2f2bf38c30c9b68020c7c43cd7b3e10549 (patch) | |
| tree | 87696f4b78894ceb46d44b1d7e2aea9375865c5d /scheduling/RTLtoBTLproof.v | |
| parent | ee558407e59c6794daad70aab2e1e7794535367e (diff) | |
| download | compcert-kvx-bf443e2f2bf38c30c9b68020c7c43cd7b3e10549.tar.gz compcert-kvx-bf443e2f2bf38c30c9b68020c7c43cd7b3e10549.zip | |
preparing compiler passes and ml oracles
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 633e1b8e..5cebd33c 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -231,6 +231,7 @@ Proof. induction ib; simpl; auto; lia. Qed. +(* TODO gourdinl remove useless lemma? *) Lemma entry_isnt_goto dupmap f pc ib: match_iblock dupmap (RTL.fn_code f) true pc (entry ib) None -> is_goto (entry ib) = false. @@ -244,12 +245,10 @@ Lemma expand_entry_isnt_goto dupmap f pc ib: match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) None) None -> is_goto (expand (entry ib) None) = false. Proof. - destruct (is_goto (expand (entry ib) None))eqn:EQG. - - destruct (expand (entry ib) None); - try destruct fi; try discriminate; trivial. - intros; inv H; inv H4. - - destruct (expand (entry ib) None); - try destruct fi; try discriminate; trivial. + destruct (is_goto (expand (entry ib) None))eqn:EQG; + destruct (expand (entry ib) None); + try destruct fi; try discriminate; trivial. + intros; inv H; inv H4. Qed. Lemma list_nth_z_rev_dupmap: |