gcc/ada/libgnat/a-strunb.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                 A D A . S T R I N G S . U N B O U N D E D                --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 1992-2023, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- This specification is derived from the Ada Reference Manual for use with --
  12 -- GNAT. The copyright notice above, and the license provisions that follow --
  13 -- apply solely to the  contents of the part following the private keyword. --
  14 --                                                                          --
  15 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  16 -- terms of the  GNU General Public License as published  by the Free Soft- --
  17 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  18 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  19 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  20 -- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
  21 --                                                                          --
  22 -- As a special exception under Section 7 of GPL version 3, you are granted --
  23 -- additional permissions described in the GCC Runtime Library Exception,   --
  24 -- version 3.1, as published by the Free Software Foundation.               --
  25 --                                                                          --
  26 -- You should have received a copy of the GNU General Public License and    --
  27 -- a copy of the GCC Runtime Library Exception along with this program;     --
  28 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
  29 -- <http://www.gnu.org/licenses/>.                                          --
  30 --                                                                          --
  31 -- GNAT was originally developed  by the GNAT team at  New York University. --
  32 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  33 --                                                                          --
  34 ------------------------------------------------------------------------------
  35
  36 --  Preconditions in this unit are meant for analysis only, not for run-time
  37 --  checking, so that the expected exceptions are raised. This is enforced by
  38 --  setting the corresponding assertion policy to Ignore.
  39
  40 pragma Assertion_Policy (Pre => Ignore);
  41
  42 with Ada.Strings.Maps;
  43 with Ada.Finalization;
  44 private with Ada.Strings.Text_Buffers;
  45
  46 --  The language-defined package Strings.Unbounded provides a private type
  47 --  Unbounded_String and a set of operations. An object of type
  48 --  Unbounded_String represents a String whose low bound is 1 and whose length
  49 --  can vary conceptually between 0 and Natural'Last. The subprograms for
  50 --  fixed-length string handling are either overloaded directly for
  51 --  Unbounded_String, or are modified as needed to reflect the flexibility in
  52 --  length. Since the Unbounded_String type is private, relevant constructor
  53 --  and selector operations are provided.
  54
  55 package Ada.Strings.Unbounded with
  56   SPARK_Mode,
  57   Initial_Condition => Length (Null_Unbounded_String) = 0,
  58   Always_Terminates
  59 is
  60    pragma Preelaborate;
  61
  62    type Unbounded_String is private with
  63      Default_Initial_Condition => Length (Unbounded_String) = 0;
  64    pragma Preelaborable_Initialization (Unbounded_String);
  65
  66    Null_Unbounded_String : constant Unbounded_String;
  67    --  Represents the null String. If an object of type Unbounded_String is not
  68    --  otherwise initialized, it will be initialized to the same value as
  69    --  Null_Unbounded_String.
  70
  71    function Length (Source : Unbounded_String) return Natural with
  72      Global => null;
  73    --  Returns the length of the String represented by Source
  74
  75    type String_Access is access all String;
  76    --  Provides a (nonprivate) access type for explicit processing of
  77    --  unbounded-length strings.
  78
  79    procedure Free (X : in out String_Access) with SPARK_Mode => Off;
  80    --  Performs an unchecked deallocation of an object of type String_Access
  81
  82    --------------------------------------------------------
  83    -- Conversion, Concatenation, and Selection Functions --
  84    --------------------------------------------------------
  85
  86    function To_Unbounded_String
  87      (Source : String)  return Unbounded_String
  88    with
  89      Post   => To_String (To_Unbounded_String'Result) = Source,
  90      Global => null;
  91    --  Returns an Unbounded_String that represents Source
  92
  93    function To_Unbounded_String
  94      (Length : Natural) return Unbounded_String
  95    with
  96      SPARK_Mode => Off,
  97      Global     => null;
  98    --  Returns an Unbounded_String that represents an uninitialized String
  99    --  whose length is Length.
 100
 101    function To_String (Source : Unbounded_String) return String with
 102      Post   =>
 103        To_String'Result'First = 1
 104          and then To_String'Result'Length = Length (Source),
 105      Global => null;
 106    --  Returns the String with lower bound 1 represented by Source
 107
 108    --  To_String and To_Unbounded_String are related as follows:
 109    --
 110    --  * If S is a String, then To_String (To_Unbounded_String (S)) = S.
 111    --
 112    --  * If U is an Unbounded_String, then
 113    --    To_Unbounded_String (To_String (U)) = U.
 114
 115    procedure Set_Unbounded_String
 116      (Target : out Unbounded_String;
 117       Source : String)
 118    with
 119      Post   => To_String (Target) = Source,
 120      Global => null;
 121    pragma Ada_05 (Set_Unbounded_String);
 122    --  Sets Target to an Unbounded_String that represents Source
 123
 124    procedure Append
 125      (Source   : in out Unbounded_String;
 126       New_Item : Unbounded_String)
 127    with
 128      Pre    => Length (New_Item) <= Natural'Last - Length (Source),
 129      Post   => Length (Source) = Length (Source)'Old + Length (New_Item),
 130      Global => null;
 131
 132    procedure Append
 133      (Source   : in out Unbounded_String;
 134       New_Item : String)
 135    with
 136      Pre    => New_Item'Length <= Natural'Last - Length (Source),
 137      Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
 138      Global => null;
 139
 140    procedure Append
 141      (Source   : in out Unbounded_String;
 142       New_Item : Character)
 143    with
 144      Pre    => Length (Source) < Natural'Last,
 145      Post   => Length (Source) = Length (Source)'Old + 1,
 146      Global => null;
 147
 148    --  For each of the Append procedures, the resulting string represented by
 149    --  the Source parameter is given by the concatenation of the original value
 150    --  of Source and the value of New_Item.
 151
 152    function "&"
 153      (Left  : Unbounded_String;
 154       Right : Unbounded_String) return Unbounded_String
 155    with
 156      Pre    => Length (Right) <= Natural'Last - Length (Left),
 157      Post   => Length ("&"'Result) = Length (Left) + Length (Right),
 158      Global => null;
 159
 160    function "&"
 161      (Left  : Unbounded_String;
 162       Right : String) return Unbounded_String
 163    with
 164      Pre    => Right'Length <= Natural'Last - Length (Left),
 165      Post   => Length ("&"'Result) = Length (Left) + Right'Length,
 166      Global => null;
 167
 168    function "&"
 169      (Left  : String;
 170       Right : Unbounded_String) return Unbounded_String
 171    with
 172      Pre    => Left'Length <= Natural'Last - Length (Right),
 173      Post   => Length ("&"'Result) = Left'Length + Length (Right),
 174      Global => null;
 175
 176    function "&"
 177      (Left  : Unbounded_String;
 178       Right : Character) return Unbounded_String
 179    with
 180      Pre    => Length (Left) < Natural'Last,
 181      Post   => Length ("&"'Result) = Length (Left) + 1,
 182      Global => null;
 183
 184    function "&"
 185      (Left  : Character;
 186       Right : Unbounded_String) return Unbounded_String
 187    with
 188      Pre    => Length (Right) < Natural'Last,
 189      Post   => Length ("&"'Result) = Length (Right) + 1,
 190      Global => null;
 191
 192    --  Each of the "&" functions returns an Unbounded_String obtained by
 193    --  concatenating the string or character given or represented by one of the
 194    --  parameters, with the string or character given or represented by the
 195    --  other parameter, and applying To_Unbounded_String to the concatenation
 196    --  result string.
 197
 198    function Element
 199      (Source : Unbounded_String;
 200       Index  : Positive) return Character
 201    with
 202      Pre    => Index <= Length (Source),
 203      Post   => Element'Result = To_String (Source) (Index),
 204      Global => null;
 205    --  Returns the character at position Index in the string represented by
 206    --  Source; propagates Index_Error if Index > Length (Source).
 207
 208    procedure Replace_Element
 209      (Source : in out Unbounded_String;
 210       Index  : Positive;
 211       By     : Character)
 212    with
 213      Pre    => Index <= Length (Source),
 214      Post   => Length (Source) = Length (Source)'Old,
 215      Global => null;
 216    --  Updates Source such that the character at position Index in the string
 217    --  represented by Source is By; propagates Index_Error if
 218    --  Index > Length (Source).
 219
 220    function Slice
 221      (Source : Unbounded_String;
 222       Low    : Positive;
 223       High   : Natural) return String
 224    with
 225      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
 226      Post   => Slice'Result'Length = Natural'Max (0, High - Low + 1),
 227      Global => null;
 228    --  Returns the slice at positions Low through High in the string
 229    --  represented by Source; propagates Index_Error if
 230    --  Low > Length (Source) + 1 or High > Length (Source). The bounds of the
 231    --  returned string are Low and High.
 232
 233    function Unbounded_Slice
 234      (Source : Unbounded_String;
 235       Low    : Positive;
 236       High   : Natural) return Unbounded_String
 237    with
 238      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
 239      Post   =>
 240        Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
 241      Global => null;
 242    pragma Ada_05 (Unbounded_Slice);
 243    --  Returns the slice at positions Low through High in the string
 244    --  represented by Source as an Unbounded_String. This propagates
 245    --  Index_Error if Low > Length(Source) + 1 or High > Length (Source).
 246
 247    procedure Unbounded_Slice
 248      (Source : Unbounded_String;
 249       Target : out Unbounded_String;
 250       Low    : Positive;
 251       High   : Natural)
 252    with
 253      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
 254      Post   => Length (Target) = Natural'Max (0, High - Low + 1),
 255      Global => null;
 256    pragma Ada_05 (Unbounded_Slice);
 257    --  Sets Target to the Unbounded_String representing the slice at positions
 258    --  Low through High in the string represented by Source. This propagates
 259    --  Index_Error if Low > Length(Source) + 1 or High > Length (Source).
 260
 261    function "="
 262      (Left  : Unbounded_String;
 263       Right : Unbounded_String) return Boolean
 264    with
 265      Post   => "="'Result = (To_String (Left) = To_String (Right)),
 266      Global => null;
 267
 268    function "="
 269      (Left  : Unbounded_String;
 270       Right : String) return Boolean
 271    with
 272      Post   => "="'Result = (To_String (Left) = Right),
 273      Global => null;
 274
 275    function "="
 276      (Left  : String;
 277       Right : Unbounded_String) return Boolean
 278    with
 279      Post   => "="'Result = (Left = To_String (Right)),
 280      Global => null;
 281
 282    function "<"
 283      (Left  : Unbounded_String;
 284       Right : Unbounded_String) return Boolean
 285    with
 286      Global => null;
 287
 288    function "<"
 289      (Left  : Unbounded_String;
 290       Right : String) return Boolean
 291    with
 292      Global => null;
 293
 294    function "<"
 295      (Left  : String;
 296       Right : Unbounded_String) return Boolean
 297    with
 298      Global => null;
 299
 300    function "<="
 301      (Left  : Unbounded_String;
 302       Right : Unbounded_String) return Boolean
 303    with
 304      Global => null;
 305
 306    function "<="
 307      (Left  : Unbounded_String;
 308       Right : String) return Boolean
 309    with
 310      Global => null;
 311
 312    function "<="
 313      (Left  : String;
 314       Right : Unbounded_String) return Boolean
 315    with
 316      Global => null;
 317
 318    function ">"
 319      (Left  : Unbounded_String;
 320       Right : Unbounded_String) return Boolean
 321    with
 322      Global => null;
 323
 324    function ">"
 325      (Left  : Unbounded_String;
 326       Right : String) return Boolean
 327    with
 328      Global => null;
 329
 330    function ">"
 331      (Left  : String;
 332       Right : Unbounded_String) return Boolean
 333    with
 334      Global => null;
 335
 336    function ">="
 337      (Left  : Unbounded_String;
 338       Right : Unbounded_String) return Boolean
 339    with
 340      Global => null;
 341
 342    function ">="
 343      (Left  : Unbounded_String;
 344       Right : String) return Boolean
 345    with
 346      Global => null;
 347
 348    function ">="
 349      (Left  : String;
 350       Right : Unbounded_String) return Boolean
 351    with
 352      Global => null;
 353
 354    --  Each of the functions "=", "<", ">", "<=", and ">=" returns the same
 355    --  result as the corresponding String operation applied to the String
 356    --  values given or represented by Left and Right.
 357
 358    ------------------------
 359    -- Search Subprograms --
 360    ------------------------
 361
 362    function Index
 363      (Source  : Unbounded_String;
 364       Pattern : String;
 365       Going   : Direction := Forward;
 366       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
 367    with
 368      Pre    => Pattern'Length /= 0,
 369      Global => null;
 370
 371    function Index
 372      (Source  : Unbounded_String;
 373       Pattern : String;
 374       Going   : Direction := Forward;
 375       Mapping : Maps.Character_Mapping_Function) return Natural
 376    with
 377      Pre    => Pattern'Length /= 0,
 378      Global => null;
 379
 380    function Index
 381      (Source : Unbounded_String;
 382       Set    : Maps.Character_Set;
 383       Test   : Membership := Inside;
 384       Going  : Direction  := Forward) return Natural
 385    with
 386      Global => null;
 387
 388    function Index
 389      (Source  : Unbounded_String;
 390       Pattern : String;
 391       From    : Positive;
 392       Going   : Direction := Forward;
 393       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
 394    with
 395      Pre    => (if Length (Source) /= 0 then From <= Length (Source))
 396                and then Pattern'Length /= 0,
 397      Global => null;
 398    pragma Ada_05 (Index);
 399
 400    function Index
 401      (Source  : Unbounded_String;
 402       Pattern : String;
 403       From    : Positive;
 404       Going   : Direction := Forward;
 405       Mapping : Maps.Character_Mapping_Function) return Natural
 406    with
 407      Pre    => (if Length (Source) /= 0 then From <= Length (Source))
 408                and then Pattern'Length /= 0,
 409      Global => null;
 410    pragma Ada_05 (Index);
 411
 412    function Index
 413      (Source  : Unbounded_String;
 414       Set     : Maps.Character_Set;
 415       From    : Positive;
 416       Test    : Membership := Inside;
 417       Going   : Direction := Forward) return Natural
 418    with
 419      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
 420      Global => null;
 421    pragma Ada_05 (Index);
 422
 423    function Index_Non_Blank
 424      (Source : Unbounded_String;
 425       Going  : Direction := Forward) return Natural
 426    with
 427      Global => null;
 428
 429    function Index_Non_Blank
 430      (Source : Unbounded_String;
 431       From   : Positive;
 432       Going  : Direction := Forward) return Natural
 433    with
 434      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
 435      Global => null;
 436    pragma Ada_05 (Index_Non_Blank);
 437
 438    function Count
 439      (Source  : Unbounded_String;
 440       Pattern : String;
 441       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
 442    with
 443      Pre    => Pattern'Length /= 0,
 444      Global => null;
 445
 446    function Count
 447      (Source  : Unbounded_String;
 448       Pattern : String;
 449       Mapping : Maps.Character_Mapping_Function) return Natural
 450    with
 451      Pre    => Pattern'Length /= 0,
 452      Global => null;
 453
 454    function Count
 455      (Source : Unbounded_String;
 456       Set    : Maps.Character_Set) return Natural
 457    with
 458      Global => null;
 459
 460    procedure Find_Token
 461      (Source : Unbounded_String;
 462       Set    : Maps.Character_Set;
 463       From   : Positive;
 464       Test   : Membership;
 465       First  : out Positive;
 466       Last   : out Natural)
 467    with
 468      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
 469      Global => null;
 470    pragma Ada_2012 (Find_Token);
 471
 472    procedure Find_Token
 473      (Source : Unbounded_String;
 474       Set    : Maps.Character_Set;
 475       Test   : Membership;
 476       First  : out Positive;
 477       Last   : out Natural)
 478    with
 479      Global => null;
 480
 481    --  Each of the search subprograms (Index, Index_Non_Blank, Count,
 482    --  Find_Token) has the same effect as the corresponding subprogram in
 483    --  Strings.Fixed applied to the string represented by the Unbounded_String
 484    --  parameter.
 485
 486    ------------------------------------
 487    -- String Translation Subprograms --
 488    ------------------------------------
 489
 490    function Translate
 491      (Source  : Unbounded_String;
 492       Mapping : Maps.Character_Mapping) return Unbounded_String
 493    with
 494      Post   => Length (Translate'Result) = Length (Source),
 495      Global => null;
 496
 497    procedure Translate
 498      (Source  : in out Unbounded_String;
 499       Mapping : Maps.Character_Mapping)
 500    with
 501      Post   => Length (Source) = Length (Source)'Old,
 502      Global => null;
 503
 504    function Translate
 505      (Source  : Unbounded_String;
 506       Mapping : Maps.Character_Mapping_Function) return Unbounded_String
 507    with
 508      Post   => Length (Translate'Result) = Length (Source),
 509      Global => null;
 510
 511    procedure Translate
 512      (Source  : in out Unbounded_String;
 513       Mapping : Maps.Character_Mapping_Function)
 514    with
 515      Post   => Length (Source) = Length (Source)'Old,
 516      Global => null;
 517
 518    --  The Translate function has an analogous effect to the corresponding
 519    --  subprogram in Strings.Fixed. The translation is applied to the string
 520    --  represented by the Unbounded_String parameter, and the result is
 521    --  converted (via To_Unbounded_String) to an Unbounded_String.
 522
 523    ---------------------------------------
 524    -- String Transformation Subprograms --
 525    ---------------------------------------
 526
 527    function Replace_Slice
 528      (Source : Unbounded_String;
 529       Low    : Positive;
 530       High   : Natural;
 531       By     : String) return Unbounded_String
 532    with
 533      Pre            =>
 534        Low - 1 <= Length (Source)
 535          and then (if High >= Low
 536                    then Low - 1
 537                      <= Natural'Last - By'Length
 538                       - Natural'Max (Length (Source) - High, 0)
 539                    else Length (Source) <= Natural'Last - By'Length),
 540      Contract_Cases =>
 541        (High >= Low =>
 542           Length (Replace_Slice'Result)
 543         = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
 544         others      =>
 545           Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
 546      Global         => null;
 547
 548    procedure Replace_Slice
 549      (Source : in out Unbounded_String;
 550       Low    : Positive;
 551       High   : Natural;
 552       By     : String)
 553    with
 554      Pre            =>
 555        Low - 1 <= Length (Source)
 556          and then (if High >= Low
 557                    then Low - 1
 558                      <= Natural'Last - By'Length
 559                       - Natural'Max (Length (Source) - High, 0)
 560                    else Length (Source) <= Natural'Last - By'Length),
 561      Contract_Cases =>
 562        (High >= Low =>
 563           Length (Source)
 564         = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
 565         others      =>
 566           Length (Source) = Length (Source)'Old + By'Length),
 567      Global         => null;
 568
 569    function Insert
 570      (Source   : Unbounded_String;
 571       Before   : Positive;
 572       New_Item : String) return Unbounded_String
 573    with
 574      Pre    => Before - 1 <= Length (Source)
 575                  and then New_Item'Length <= Natural'Last - Length (Source),
 576      Post   => Length (Insert'Result) = Length (Source) + New_Item'Length,
 577      Global => null;
 578
 579    procedure Insert
 580      (Source   : in out Unbounded_String;
 581       Before   : Positive;
 582       New_Item : String)
 583    with
 584      Pre    => Before - 1 <= Length (Source)
 585                  and then New_Item'Length <= Natural'Last - Length (Source),
 586      Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
 587      Global => null;
 588
 589    function Overwrite
 590      (Source   : Unbounded_String;
 591       Position : Positive;
 592       New_Item : String) return Unbounded_String
 593    with
 594      Pre    => Position - 1 <= Length (Source)
 595                  and then (if New_Item'Length /= 0
 596                            then
 597                              New_Item'Length <= Natural'Last - (Position - 1)),
 598      Post   =>
 599        Length (Overwrite'Result)
 600      = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
 601      Global => null;
 602
 603    procedure Overwrite
 604      (Source   : in out Unbounded_String;
 605       Position : Positive;
 606       New_Item : String)
 607    with
 608      Pre    => Position - 1 <= Length (Source)
 609                  and then (if New_Item'Length /= 0
 610                            then
 611                              New_Item'Length <= Natural'Last - (Position - 1)),
 612      Post   =>
 613        Length (Source)
 614      = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
 615
 616      Global => null;
 617
 618    function Delete
 619      (Source  : Unbounded_String;
 620       From    : Positive;
 621       Through : Natural) return Unbounded_String
 622    with
 623      Pre            => (if Through <= From then From - 1 <= Length (Source)),
 624      Contract_Cases =>
 625        (Through >= From =>
 626           Length (Delete'Result) = Length (Source) - (Through - From + 1),
 627         others          =>
 628           Length (Delete'Result) = Length (Source)),
 629      Global         => null;
 630
 631    procedure Delete
 632      (Source  : in out Unbounded_String;
 633       From    : Positive;
 634       Through : Natural)
 635    with
 636      Pre            => (if Through <= From then From - 1 <= Length (Source)),
 637      Contract_Cases =>
 638        (Through >= From =>
 639           Length (Source) = Length (Source)'Old - (Through - From + 1),
 640         others          =>
 641           Length (Source) = Length (Source)'Old),
 642      Global         => null;
 643
 644    function Trim
 645      (Source : Unbounded_String;
 646       Side   : Trim_End) return Unbounded_String
 647    with
 648      Post   => Length (Trim'Result) <= Length (Source),
 649      Global => null;
 650
 651    procedure Trim
 652      (Source : in out Unbounded_String;
 653       Side   : Trim_End)
 654    with
 655      Post   => Length (Source) <= Length (Source)'Old,
 656      Global => null;
 657
 658    function Trim
 659      (Source : Unbounded_String;
 660       Left   : Maps.Character_Set;
 661       Right  : Maps.Character_Set) return Unbounded_String
 662    with
 663      Post   => Length (Trim'Result) <= Length (Source),
 664      Global => null;
 665
 666    procedure Trim
 667      (Source : in out Unbounded_String;
 668       Left   : Maps.Character_Set;
 669       Right  : Maps.Character_Set)
 670    with
 671      Post   => Length (Source) <= Length (Source)'Old,
 672      Global => null;
 673
 674    function Head
 675      (Source : Unbounded_String;
 676       Count  : Natural;
 677       Pad    : Character := Space) return Unbounded_String
 678    with
 679      Post   => Length (Head'Result) = Count,
 680      Global => null;
 681
 682    procedure Head
 683      (Source : in out Unbounded_String;
 684       Count  : Natural;
 685       Pad    : Character := Space)
 686    with
 687      Post   => Length (Source) = Count,
 688      Global => null;
 689
 690    function Tail
 691      (Source : Unbounded_String;
 692       Count  : Natural;
 693       Pad    : Character := Space) return Unbounded_String
 694    with
 695      Post   => Length (Tail'Result) = Count,
 696      Global => null;
 697
 698    procedure Tail
 699      (Source : in out Unbounded_String;
 700       Count  : Natural;
 701       Pad    : Character := Space)
 702    with
 703      Post   => Length (Source) = Count,
 704      Global => null;
 705
 706    function "*"
 707      (Left  : Natural;
 708       Right : Character) return Unbounded_String
 709    with
 710      Pre    => Left <= Natural'Last,
 711      Post   => Length ("*"'Result) = Left,
 712      Global => null;
 713
 714    function "*"
 715      (Left  : Natural;
 716       Right : String) return Unbounded_String
 717    with
 718      Pre    => (if Left /= 0 then Right'Length <= Natural'Last / Left),
 719      Post   => Length ("*"'Result) = Left * Right'Length,
 720      Global => null;
 721
 722    function "*"
 723      (Left  : Natural;
 724       Right : Unbounded_String) return Unbounded_String
 725    with
 726      Pre    => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
 727      Post   => Length ("*"'Result) = Left * Length (Right),
 728      Global => null;
 729
 730    --  Each of the transformation functions (Replace_Slice, Insert, Overwrite,
 731    --  Delete), selector functions (Trim, Head, Tail), and constructor
 732    --  functions ("*") is likewise analogous to its corresponding subprogram in
 733    --  Strings.Fixed. For each of the subprograms, the corresponding
 734    --  fixed-length string subprogram is applied to the string represented by
 735    --  the Unbounded_String parameter, and To_Unbounded_String is applied the
 736    --  result string.
 737    --
 738    --  For each of the procedures Translate, Replace_Slice, Insert, Overwrite,
 739    --  Delete, Trim, Head, and Tail, the resulting string represented by the
 740    --  Source parameter is given by the corresponding function for fixed-length
 741    --  strings applied to the string represented by Source's original value.
 742
 743 private
 744    pragma SPARK_Mode (Off);  --  Controlled types are not in SPARK
 745
 746    pragma Inline (Length);
 747
 748    package AF renames Ada.Finalization;
 749
 750    Null_String : aliased String := "";
 751
 752    function To_Unbounded (S : String) return Unbounded_String
 753      renames To_Unbounded_String;
 754
 755    type Unbounded_String is new AF.Controlled with record
 756       Reference : not null String_Access := Null_String'Access;
 757       Last      : Natural                := 0;
 758    end record with Put_Image => Put_Image;
 759
 760    procedure Put_Image
 761      (S : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class;
 762       V : Unbounded_String);
 763
 764    --  The Unbounded_String is using a buffered implementation to increase
 765    --  speed of the Append/Delete/Insert procedures. The Reference string
 766    --  pointer above contains the current string value and extra room at the
 767    --  end to be used by the next Append routine. Last is the index of the
 768    --  string ending character. So the current string value is really
 769    --  Reference (1 .. Last).
 770
 771    pragma Stream_Convert (Unbounded_String, To_Unbounded, To_String);
 772    --  Provide stream routines without dragging in Ada.Streams
 773
 774    pragma Finalize_Storage_Only (Unbounded_String);
 775    --  Finalization is required only for freeing storage
 776
 777    procedure Initialize (Object : in out Unbounded_String);
 778    procedure Adjust     (Object : in out Unbounded_String);
 779    procedure Finalize   (Object : in out Unbounded_String);
 780
 781    procedure Realloc_For_Chunk
 782      (Source     : in out Unbounded_String;
 783       Chunk_Size : Natural);
 784    pragma Inline (Realloc_For_Chunk);
 785    --  Adjust the size allocated for the string. Add at least Chunk_Size so it
 786    --  is safe to add a string of this size at the end of the current content.
 787    --  The real size allocated for the string is Chunk_Size + x of the current
 788    --  string size. This buffered handling makes the Append unbounded string
 789    --  routines very fast. This spec is in the private part so that it can be
 790    --  accessed from children (e.g. from Unbounded.Text_IO).
 791
 792    Null_Unbounded_String : constant Unbounded_String :=
 793                              (AF.Controlled with
 794                                 Reference => Null_String'Access,
 795                                 Last      => 0);
 796 end Ada.Strings.Unbounded;