sig type rg val compute : Wp.Conditions.sequence -> Wp.Auto.Range.rg val ranges : Wp.Auto.Range.rg -> (int * int) Wp.Lang.F.Tmap.t val bounds : Wp.Auto.Range.rg -> (int option * int option) Wp.Lang.F.Tmap.t end