From ab520acd80f7d39aa14fdda6932accbb2a787ebf Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 19 May 2021 12:47:22 +0200 Subject: Grouping common RTL functions, printer improvement --- backend/Duplicateaux.ml | 2 +- backend/LICMaux.ml | 5 +---- 2 files changed, 2 insertions(+), 5 deletions(-) (limited to 'backend') diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index d55da64a..e8e60a4f 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -23,6 +23,7 @@ open RTL open Maps open Camlcoq open DebugPrint +open AuxTools let stats_oc = ref None @@ -95,7 +96,6 @@ let write_stats_oc () = end let get_loop_headers = LICMaux.get_loop_headers -let get_some = LICMaux.get_some let rtl_successors = LICMaux.rtl_successors (* Get list of nodes following a BFS of the code *) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index b88dbc2d..df609505 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -17,16 +17,13 @@ open Kildall;; open HashedSet;; open Inject;; open DebugPrint;; +open AuxTools;; type reg = P.t;; (** get_loop_headers moved from Duplicateaux.ml to LICMaux.ml to prevent cycle dependencies *) type vstate = Unvisited | Processed | Visited -let get_some = function -| None -> failwith "Did not get some" -| Some thing -> thing - let rtl_successors = function | Itailcall _ | Ireturn _ -> [] | Icall(_,_,_,_,n) | Ibuiltin(_,_,_,n) | Inop n | Iop (_,_,_,n) -- cgit