diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-11 23:47:52 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-11 23:47:52 +0100 |
| commit | b387d68faae6cdc520a1ae4d213402de473f6022 (patch) | |
| tree | 8b4d40a0b54da04fa4c1901a8ed192a1f6bcc53f /aarch64/PostpassScheduling.v | |
| parent | ea3f2755c1c1a733c2a5886d8b82afce6fdcad03 (diff) | |
| download | compcert-kvx-b387d68faae6cdc520a1ae4d213402de473f6022.tar.gz compcert-kvx-b387d68faae6cdc520a1ae4d213402de473f6022.zip | |
Verifier is now enabled with debug prints
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). |