From 271f87ba08f42340900378c0797511d4071fc1b8 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 31 May 2021 16:55:18 +0200
Subject: BTL Scheduler oracle and some drafts

---
 scheduling/RTLtoBTLaux.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'scheduling/RTLtoBTLaux.ml')

diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index d04326ea..e709d846 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -6,7 +6,6 @@ open RTLcommonaux
 open DebugPrint
 open BTLtypes
 open BTLcommonaux
-open BTLScheduleraux
 
 let encaps_final inst osucc =
   match inst with
@@ -102,19 +101,16 @@ let rtl2btl (f : RTL.coq_function) =
   let btl = translate_function code entry join_points liveness in
   let dm = PTree.map (fun n i -> n) btl in
   (* TODO gourdinl move elsewhere *)
-  let btl' = btl_scheduler btl in
   debug "Entry %d\n" (p2i entry);
   (*debug_flag := true;*)
   debug "RTL Code: ";
   print_code code;
   debug "BTL Code:\n";
   print_btl_code stderr btl;
-  debug "Scheduled BTL Code:\n";
-  print_btl_code stderr btl';
   (*debug_flag := false;*)
   debug "Dupmap:\n";
   print_ptree print_pint dm;
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
-  ((btl', entry), dm)
+  ((btl, entry), dm)
-- 
cgit