aboutsummaryrefslogtreecommitdiffstats
path: root/common
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2021-04-02 13:06:02 +0200
committerCyril SIX <cyril.six@kalray.eu>2021-04-02 13:06:02 +0200
commita4720c58a97c08b1f8852376c39f15dd44cd0f34 (patch)
tree0ae0f8cf6185853e2a2a0189c3afc5a129e901bd /common
parentb042bca17696a9cb6e2be7bbdac9f08953fff527 (diff)
downloadcompcert-kvx-a4720c58a97c08b1f8852376c39f15dd44cd0f34.tar.gz
compcert-kvx-a4720c58a97c08b1f8852376c39f15dd44cd0f34.zip
Getting all loop bodies
Diffstat (limited to 'common')
-rw-r--r--common/DebugPrint.ml14
1 files changed, 14 insertions, 0 deletions
diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml
index 931dfdf4..f68432d9 100644
--- a/common/DebugPrint.ml
+++ b/common/DebugPrint.ml
@@ -44,6 +44,20 @@ let print_intlist oc l =
end
end
+let print_ptree_oplist oc pt =
+ if !debug_flag then
+ let elements = PTree.elements pt in
+ begin
+ Printf.fprintf oc "[";
+ List.iter (fun (n, ol) ->
+ match ol with
+ | None -> ()
+ | Some l -> Printf.fprintf oc "%d -> %a,\n" (P.to_int n) print_intlist l
+ ) elements;
+ Printf.fprintf oc "]\n"
+ end
+ else ()
+
(* Adapted from backend/PrintRTL.ml: print_function *)
let print_code code = let open PrintRTL in let open Printf in
if (!debug_flag) then begin