From 3e47c1b17e8ff03400106a80117eb86d7e7f9da6 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 13:30:57 +0100
Subject: Expansion of Ccompimm in RTL [Admitted checker]

---
 scheduling/RTLpathCommon.ml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 scheduling/RTLpathCommon.ml

(limited to 'scheduling/RTLpathCommon.ml')

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
+}
+
-- 
cgit