diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-28 05:05:47 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-28 05:05:47 +0100 |
| commit | 251e184d2d972e2bfbf6f36d0c607e6d89801a30 (patch) | |
| tree | 5876f4ba816b5403f87e60ac1735864b5d4ecf1a /mppa_k1c/PostpassScheduling.v | |
| parent | 061c1a394b0c540d2c8bf996b2ef2776549e74bf (diff) | |
| parent | 4c39f19e2bb7de48ad9f3252f38fd4a035c1b787 (diff) | |
| download | compcert-kvx-251e184d2d972e2bfbf6f36d0c607e6d89801a30.tar.gz compcert-kvx-251e184d2d972e2bfbf6f36d0c607e6d89801a30.zip | |
Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpass
Diffstat (limited to 'mppa_k1c/PostpassScheduling.v')
| -rw-r--r-- | mppa_k1c/PostpassScheduling.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 6700e684..ab4bc9c9 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -352,8 +352,9 @@ Definition verified_schedule_nob (bb : bblock) : res (list bblock) := do tbb <- concat_all lbb; do sizecheck <- verify_size bb lbb; do schedcheck <- verify_schedule bb' tbb; - do parcheck <- verify_par lbb; - stick_header_code (header bb) lbb. + do res <- stick_header_code (header bb) lbb; + do parcheck <- verify_par res; + OK res. Lemma verified_schedule_nob_size: forall bb lbb, verified_schedule_nob bb = OK lbb -> size bb = size_blocks lbb. @@ -379,7 +380,7 @@ Lemma verified_schedule_nob_header: /\ Forall (fun b => header b = nil) lbb. Proof. intros. split. - - monadInv H. unfold stick_header_code in EQ4. destruct (hd_error _); try discriminate. inv EQ4. + - monadInv H. unfold stick_header_code in EQ2. destruct (hd_error _); try discriminate. inv EQ2. simpl. reflexivity. - apply verified_schedule_nob_no_header_in_middle in H. assumption. Qed. |