diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-09-01 16:57:12 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-09-01 16:57:12 +0200 |
| commit | ddc17a17408541efa8b23afa3e6ccad1e6ce0b6e (patch) | |
| tree | ab479fba4e57dc9d8ca131d485e9ec626815eee4 /scheduling/RTLpathCommon.ml | |
| parent | a4c7a7240a93e874779027a6a3d41ccebc81b396 (diff) | |
| download | compcert-kvx-ddc17a17408541efa8b23afa3e6ccad1e6ce0b6e.tar.gz compcert-kvx-ddc17a17408541efa8b23afa3e6ccad1e6ce0b6e.zip | |
cleanup
Diffstat (limited to 'scheduling/RTLpathCommon.ml')
| -rw-r--r-- | scheduling/RTLpathCommon.ml | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/scheduling/RTLpathCommon.ml b/scheduling/RTLpathCommon.ml deleted file mode 100644 index 3d123ba8..00000000 --- a/scheduling/RTLpathCommon.ml +++ /dev/null @@ -1,14 +0,0 @@ -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 *) - mutable liveins: Regset.t PTree.t; - (* Union of the input_regs of the last successors *) - s_output_regs: Regset.t; - typing: RTLtyping.regenv -} - |