1 files changed, 14 insertions, 0 deletions
diff --git a/scheduling/RTLpathCommon.ml b/scheduling/RTLpathCommon.ml
new file mode 100644
index 00000000..748a02f1
--- /dev/null
+++ b/scheduling/RTLpathCommon.ml
@@ -0,0 +1,14 @@
+open Maps
+open Registers
+open Camlcoq
+
+type superblock = {
+  mutable instructions: P.t array; (* pointers to code instructions *)
+  (* each predicted Pcb has its attached liveins *)
+  (* This is indexed by the pc value *)
+  liveins: Regset.t PTree.t;
+  (* Union of the input_regs of the last successors *)
+  s_output_regs: Regset.t;
+  typing: RTLtyping.regenv
+}
+