diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-28 11:44:11 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-28 11:44:11 +0200 |
| commit | 05b24fdb11414100b9b04867e6e2d3a1a9054162 (patch) | |
| tree | 6ae4a50a2f311c6b2786e64de12d4d5f7755f865 /scheduling/BTLcommonaux.ml | |
| parent | 56901933d110adef341312e1c7630b672827b41d (diff) | |
| download | compcert-kvx-05b24fdb11414100b9b04867e6e2d3a1a9054162.tar.gz compcert-kvx-05b24fdb11414100b9b04867e6e2d3a1a9054162.zip | |
Improvements in scheduling and renumbering BTL code
Diffstat (limited to 'scheduling/BTLcommonaux.ml')
| -rw-r--r-- | scheduling/BTLcommonaux.ml | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/scheduling/BTLcommonaux.ml b/scheduling/BTLcommonaux.ml index dabf760a..4605d613 100644 --- a/scheduling/BTLcommonaux.ml +++ b/scheduling/BTLcommonaux.ml @@ -68,17 +68,3 @@ let rec get_inumb_or_next = function iinfo.inumb | Bseq (ib1, _) -> get_inumb_or_next ib1 | _ -> failwith "get_inumb_or_next: Bnop None" - -let rec set_next_inumb btl pos = function - | BF (Bgoto s, _) -> - let ib' = (get_some @@ PTree.get s btl).entry in - set_next_inumb btl pos ib' - | BF (_, iinfo) - | Bnop (Some iinfo) - | Bop (_, _, _, iinfo) - | Bload (_, _, _, _, _, iinfo) - | Bstore (_, _, _, _, iinfo) - | Bcond (_, _, _, _, iinfo) -> - iinfo.inumb <- pos - | Bseq (ib1, _) -> set_next_inumb btl pos ib1 - | _ -> failwith "get_inumb_or_next: Bnop None" |