aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/RTLpathScheduleraux.ml
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-02-10 10:34:38 +0100
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-02-10 10:34:38 +0100
commit84cb4939653e5355c2039ed62a140aa392e21162 (patch)
tree156a6a78208983cf7fca540899313144f36687e0 /scheduling/RTLpathScheduleraux.ml
parent3104e551bf87abeab9a257c955cf9b180769dc64 (diff)
downloadcompcert-kvx-84cb4939653e5355c2039ed62a140aa392e21162.tar.gz
compcert-kvx-84cb4939653e5355c2039ed62a140aa392e21162.zip
[Admitted checker] Checker expansion for reg Ocmp (without scratch)
Diffstat (limited to 'scheduling/RTLpathScheduleraux.ml')
-rw-r--r--scheduling/RTLpathScheduleraux.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml
index 19b05741..5e4999db 100644
--- a/scheduling/RTLpathScheduleraux.ml
+++ b/scheduling/RTLpathScheduleraux.ml
@@ -319,10 +319,11 @@ let scheduler f =
debug "Pathmap:\n"; debug "\n";
print_path_map pm;
debug "Superblocks:\n";
- print_superblocks lsb code; debug "\n";
(*debug_flag := true; *)
+ (*print_code code; flush stdout; flush stderr;*)
+ (*debug_flag := false;*)
+ (*print_superblocks lsb code; debug "\n";*)
find_last_node_reg (PTree.elements code);
- (*print_code code;*)
let (tc, pm) = do_schedule code pm lsb in
(((tc, entry), pm), id_ptree)
end