aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/RTLpathLivegenaux.ml
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-02-16 13:24:41 +0100
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-02-16 13:24:41 +0100
commit8faafc7668b9423ba9bee1f4e725eab5b378c851 (patch)
tree23acb02e9a6733e539fd77185639622f451fbdc2 /scheduling/RTLpathLivegenaux.ml
parentaa51677a82301a6c5d65717c6d9799bc8f8a0fea (diff)
downloadcompcert-kvx-8faafc7668b9423ba9bee1f4e725eab5b378c851.tar.gz
compcert-kvx-8faafc7668b9423ba9bee1f4e725eab5b378c851.zip
quick fixcomments
Diffstat (limited to 'scheduling/RTLpathLivegenaux.ml')
-rw-r--r--scheduling/RTLpathLivegenaux.ml5
1 files changed, 1 insertions, 4 deletions
diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml
index db3fc9d4..8cb500b8 100644
--- a/scheduling/RTLpathLivegenaux.ml
+++ b/scheduling/RTLpathLivegenaux.ml
@@ -229,7 +229,6 @@ let get_outputs liveness f n pi =
fun n -> get_some @@ PTree.get n liveness
) path_last_successors in
let outputs = List.fold_left Regset.union Regset.empty list_input_regs in
-
match last_instruction with
| Icall (_, _, _, _, _) | Itailcall (_, _, _)
| Ibuiltin (_, _, _, _) | Ijumptable (_, _)
@@ -245,13 +244,12 @@ let set_pathmap_liveness f pm =
let inputs = get_some @@ PTree.get n liveness in
let (por, outputs) = get_outputs liveness f n pi in
new_pm := PTree.set n
- {psize=pi.psize; input_regs=inputs; pre_output_regs=por; output_regs=outputs} !new_pm (* FIXME: STUB *)
+ {psize=pi.psize; input_regs=inputs; pre_output_regs=por; output_regs=outputs} !new_pm
) (PTree.elements pm);
!new_pm
end
let print_path_info pi = begin
- (*debug_flag := true;*)
debug "(psize=%d; " (Camlcoq.Nat.to_int pi.psize);
debug "\ninput_regs=";
print_regset pi.input_regs;
@@ -260,7 +258,6 @@ let print_path_info pi = begin
debug "\n; output_regs=";
print_regset pi.output_regs;
debug ")\n"
- (*debug_flag := false*)
end
let print_path_map path_map = begin