diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-18 19:15:39 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-18 19:15:39 +0200 |
| commit | af2208a2c7126d4d101fb07c40920e12c9ebbab3 (patch) | |
| tree | 945013a06b820324a72a0a243181ec3a0578473e /scheduling/PrintBTL.ml | |
| parent | c27d87ffe33242840964dd9bd67090409eea79a5 (diff) | |
| download | compcert-kvx-af2208a2c7126d4d101fb07c40920e12c9ebbab3.tar.gz compcert-kvx-af2208a2c7126d4d101fb07c40920e12c9ebbab3.zip | |
first oracle seems ok
Diffstat (limited to 'scheduling/PrintBTL.ml')
| -rw-r--r-- | scheduling/PrintBTL.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml index 8f61380e..781dcaf3 100644 --- a/scheduling/PrintBTL.ml +++ b/scheduling/PrintBTL.ml @@ -83,6 +83,9 @@ let rec print_iblock pp is_rec pref ib = print_iblock pp is_rec pref ib2) else fprintf pp "Bseq...\n" +let print_btl_inst pp ib = + print_iblock pp false " " ib + let print_btl_code pp btl is_rec = fprintf pp "\n"; List.iter (fun (n,ibf) -> |