diff options
Diffstat (limited to 'aarch64/PostpassScheduling.v')
-rw-r--r-- | aarch64/PostpassScheduling.v | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v index eeca4e54..c84b327b 100644 --- a/aarch64/PostpassScheduling.v +++ b/aarch64/PostpassScheduling.v @@ -210,12 +210,11 @@ Inductive is_concat : bblock -> list bblock -> Prop := *) (** * Remainder of the verified scheduler *) -(*Definition verify_schedule (bb bb' : bblock) : res unit :=*) - (*match bblock_simub bb bb' with*) - (*| true => OK tt*) - (*| false => Error (msg "PostpassScheduling.verify_schedule")*) - (*end.*) - +Definition verify_schedule (bb bb' : bblock) : res unit := + match bblock_simub bb bb' with + | true => OK tt + | false => Error (msg "PostpassScheduling.verify_schedule") + end. (*Definition verify_size bb lbb := if (Z.eqb (size bb) (size_blocks lbb)) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size").*) @@ -359,7 +358,7 @@ Definition verified_schedule (bb : bblock) : res bblock := do lb <- do_schedule bb'; (*do tbb <- concat_all lbb;*) (*do sizecheck <- verify_size bb lbb;*) - (*do schedcheck <- verify_schedule bb' tbb;*) (* TODO Keep this one *) + do schedcheck <- verify_schedule bb' lb; (* TODO Keep this one *) (*do parcheck <- verify_par res;*) OK (stick_header (header bb) lb). |