diff options
Diffstat (limited to 'scheduling/RTLpathCommon.ml')
-rw-r--r-- | scheduling/RTLpathCommon.ml | 14 |
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 +} + |