diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-17 16:11:43 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-17 16:11:43 +0100 |
| commit | fa0c79015c3ecd2ad63dbf1b50f60039cf043151 (patch) | |
| tree | 93a34c8602948adb99462f7a971283df32796dc5 /aarch64/PostpassScheduling.v | |
| parent | 376315dae506e496d1613934ea6e0e9d056c6526 (diff) | |
| download | compcert-kvx-fa0c79015c3ecd2ad63dbf1b50f60039cf043151.tar.gz compcert-kvx-fa0c79015c3ecd2ad63dbf1b50f60039cf043151.zip | |
Builtin mem spec in scheduler and some needed proof in Postpasssch.v
Diffstat (limited to 'aarch64/PostpassScheduling.v')
| -rw-r--r-- | aarch64/PostpassScheduling.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v index c84b327b..a9473789 100644 --- a/aarch64/PostpassScheduling.v +++ b/aarch64/PostpassScheduling.v @@ -336,8 +336,9 @@ Program Definition schedule_to_bblock (lb: list basic) (oc: option control) : re | Some c => OK {| header := nil; body := lb; exit := Some c |} end. Next Obligation. - (* TODO *) -Admitted. + unfold Is_true, AB.non_empty_bblockb. + unfold AB.non_empty_exit. rewrite orb_true_r. reflexivity. +Qed. Definition do_schedule (bb: bblock) : res bblock := if (Z.eqb (size bb) 1) then OK (bb) |