diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-07-30 11:15:15 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-07-30 11:15:15 +0200 |
| commit | 211382d21013c038c3c716454fcfa5a375dba8ba (patch) | |
| tree | 8eff5ce39ad3909c397ca157bc91e9b1e1cf3800 /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 98c22a6f37c7230faf80b6366aaa1c2476f9e67c (diff) | |
| download | compcert-kvx-211382d21013c038c3c716454fcfa5a375dba8ba.tar.gz compcert-kvx-211382d21013c038c3c716454fcfa5a375dba8ba.zip | |
(#139) - Predicate is_concat
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 0edaf4e2..2207a2fa 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -736,7 +736,7 @@ Proof. induction 1; intros; inv MS. - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL). - exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ). + exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ). inv CONC. rename H3 into CONC. assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned). eapply transf_function_no_overflow; eauto. |