diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-02 13:30:57 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-02 13:30:57 +0100 |
| commit | 3e47c1b17e8ff03400106a80117eb86d7e7f9da6 (patch) | |
| tree | 6e3695f24009ada53da34e13896148244e10774c /scheduling/RTLpathCommon.ml | |
| parent | 8d4cfe798fb548b4f670fdbe6ebac5bf893276b4 (diff) | |
| download | compcert-kvx-3e47c1b17e8ff03400106a80117eb86d7e7f9da6.tar.gz compcert-kvx-3e47c1b17e8ff03400106a80117eb86d7e7f9da6.zip | |
Expansion of Ccompimm in RTL [Admitted checker]
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 +} + |