diff options
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" |