aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/RTLpathScheduleraux.ml
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-03-02 18:48:53 +0100
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-03-02 18:48:53 +0100
commit801cd27eb78a9ba9dce6f62626288531905fcfed (patch)
tree83a5811930ebb3fa659fa2e531fc270f1e145b38 /scheduling/RTLpathScheduleraux.ml
parent3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff)
downloadcompcert-kvx-801cd27eb78a9ba9dce6f62626288531905fcfed.tar.gz
compcert-kvx-801cd27eb78a9ba9dce6f62626288531905fcfed.zip
[Admitted checker] Oracle expansion for float/float32 constant init
Diffstat (limited to 'scheduling/RTLpathScheduleraux.ml')
-rw-r--r--scheduling/RTLpathScheduleraux.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml
index 378bf097..c2183937 100644
--- a/scheduling/RTLpathScheduleraux.ml
+++ b/scheduling/RTLpathScheduleraux.ml
@@ -300,10 +300,10 @@ let rec do_schedule code pm = function
(*debug_flag := true;*)
debug "Old Code: "; print_code code;
debug "Exp Code: "; print_code code_exp;
+ (*debug_flag := false; *)
debug "\nSchedule to apply: "; print_arrayp schedule;
debug "\nNew Code: "; print_code new_code;
debug "\n";
- (*debug_flag := false; *)
do_schedule new_code pm lsb
end