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 is
  59    pragma Preelaborate;
  60    pragma Annotate (GNATprove, Always_Return, Unbounded);
  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   => Length (To_Unbounded_String'Result) = Source'Length,
  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      Post   =>
  97        Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length,
  98      Global => null;
  99    --  Returns an Unbounded_String that represents an uninitialized String
 100    --  whose length is Length.
 101
 102    function To_String (Source : Unbounded_String) return String with
 103      Post   => To_String'Result'Length = Length (Source),
 104      Global => null;
 105    --  Returns the String with lower bound 1 represented by Source
 106
 107    --  To_String and To_Unbounded_String are related as follows:
 108    --
 109    --  * If S is a String, then To_String (To_Unbounded_String (S)) = S.
 110    --
 111    --  * If U is an Unbounded_String, then
 112    --    To_Unbounded_String (To_String (U)) = U.
 113
 114    procedure Set_Unbounded_String
 115      (Target : out Unbounded_String;
 116       Source : String)
 117    with
 118      Global => null;
 119    pragma Ada_05 (Set_Unbounded_String);
 120    --  Sets Target to an Unbounded_String that represents Source
 121
 122    procedure Append
 123      (Source   : in out Unbounded_String;
 124       New_Item : Unbounded_String)
 125    with
 126      Pre    => Length (New_Item) <= Natural'Last - Length (Source),
 127      Post   => Length (Source) = Length (Source)'Old + Length (New_Item),
 128      Global => null;
 129
 130    procedure Append
 131      (Source   : in out Unbounded_String;
 132       New_Item : String)
 133    with
 134      Pre    => New_Item'Length <= Natural'Last - Length (Source),
 135      Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
 136      Global => null;
 137
 138    procedure Append
 139      (Source   : in out Unbounded_String;
 140       New_Item : Character)
 141    with
 142      Pre    => Length (Source) < Natural'Last,
 143      Post   => Length (Source) = Length (Source)'Old + 1,
 144      Global => null;
 145
 146    --  For each of the Append procedures, the resulting string represented by
 147    --  the Source parameter is given by the concatenation of the original value
 148    --  of Source and the value of New_Item.
 149
 150    function "&"
 151      (Left  : Unbounded_String;
 152       Right : Unbounded_String) return Unbounded_String
 153    with
 154      Pre    => Length (Right) <= Natural'Last - Length (Left),
 155      Post   => Length ("&"'Result) = Length (Left) + Length (Right),
 156      Global => null;
 157
 158    function "&"
 159      (Left  : Unbounded_String;
 160       Right : String) return Unbounded_String
 161    with
 162      Pre    => Right'Length <= Natural'Last - Length (Left),
 163      Post   => Length ("&"'Result) = Length (Left) + Right'Length,
 164      Global => null;
 165
 166    function "&"
 167      (Left  : String;
 168       Right : Unbounded_String) return Unbounded_String
 169    with
 170      Pre    => Left'Length <= Natural'Last - Length (Right),
 171      Post   => Length ("&"'Result) = Left'Length + Length (Right),
 172      Global => null;
 173
 174    function "&"
 175      (Left  : Unbounded_String;
 176       Right : Character) return Unbounded_String
 177    with
 178      Pre    => Length (Left) < Natural'Last,
 179      Post   => Length ("&"'Result) = Length (Left) + 1,
 180      Global => null;
 181
 182    function "&"
 183      (Left  : Character;
 184       Right : Unbounded_String) return Unbounded_String
 185    with
 186      Pre    => Length (Right) < Natural'Last,
 187      Post   => Length ("&"'Result) = Length (Right) + 1,
 188      Global => null;
 189
 190    --  Each of the "&" functions returns an Unbounded_String obtained by
 191    --  concatenating the string or character given or represented by one of the
 192    --  parameters, with the string or character given or represented by the
 193    --  other parameter, and applying To_Unbounded_String to the concatenation
 194    --  result string.
 195
 196    function Element
 197      (Source : Unbounded_String;
 198       Index  : Positive) return Character
 199    with
 200      Pre    => Index <= Length (Source),
 201      Global => null;
 202    --  Returns the character at position Index in the string represented by
 203    --  Source; propagates Index_Error if Index > Length (Source).
 204
 205    procedure Replace_Element
 206      (Source : in out Unbounded_String;
 207       Index  : Positive;
 208       By     : Character)
 209    with
 210      Pre    => Index <= Length (Source),
 211      Post   => Length (Source) = Length (Source)'Old,
 212      Global => null;
 213    --  Updates Source such that the character at position Index in the string
 214    --  represented by Source is By; propagates Index_Error if
 215    --  Index > Length (Source).
 216
 217    function Slice
 218      (Source : Unbounded_String;
 219       Low    : Positive;
 220       High   : Natural) return String
 221    with
 222      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
 223      Post   => Slice'Result'Length = Natural'Max (0, High - Low + 1),
 224      Global => null;
 225    --  Returns the slice at positions Low through High in the string
 226    --  represented by Source; propagates Index_Error if
 227    --  Low > Length (Source) + 1 or High > Length (Source). The bounds of the
 228    --  returned string are Low and High.
 229
 230    function Unbounded_Slice
 231      (Source : Unbounded_String;
 232       Low    : Positive;
 233       High   : Natural) return Unbounded_String
 234    with
 235      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
 236      Post   =>
 237        Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
 238      Global => null;
 239    pragma Ada_05 (Unbounded_Slice);
 240    --  Returns the slice at positions Low through High in the string
 241    --  represented by Source as an Unbounded_String. This propagates
 242    --  Index_Error if Low > Length(Source) + 1 or High > Length (Source).
 243
 244    procedure Unbounded_Slice
 245      (Source : Unbounded_String;
 246       Target : out Unbounded_String;
 247       Low    : Positive;
 248       High   : Natural)
 249    with
 250      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
 251      Post   => Length (Target) = Natural'Max (0, High - Low + 1),
 252      Global => null;
 253    pragma Ada_05 (Unbounded_Slice);
 254    --  Sets Target to the Unbounded_String representing the slice at positions
 255    --  Low through High in the string represented by Source. This propagates
 256    --  Index_Error if Low > Length(Source) + 1 or High > Length (Source).
 257
 258    function "="
 259      (Left  : Unbounded_String;
 260       Right : Unbounded_String) return Boolean
 261    with
 262      Global => null;
 263
 264    function "="
 265      (Left  : Unbounded_String;
 266       Right : String) return Boolean
 267    with
 268      Global => null;
 269
 270    function "="
 271      (Left  : String;
 272       Right : Unbounded_String) return Boolean
 273    with
 274      Global => null;
 275
 276    function "<"
 277      (Left  : Unbounded_String;
 278       Right : Unbounded_String) return Boolean
 279    with
 280      Global => null;
 281
 282    function "<"
 283      (Left  : Unbounded_String;
 284       Right : String) return Boolean
 285    with
 286      Global => null;
 287
 288    function "<"
 289      (Left  : String;
 290       Right : Unbounded_String) return Boolean
 291    with
 292      Global => null;
 293
 294    function "<="
 295      (Left  : Unbounded_String;
 296       Right : Unbounded_String) return Boolean
 297    with
 298      Global => null;
 299
 300    function "<="
 301      (Left  : Unbounded_String;
 302       Right : String) return Boolean
 303    with
 304      Global => null;
 305
 306    function "<="
 307      (Left  : String;
 308       Right : Unbounded_String) return Boolean
 309    with
 310      Global => null;
 311
 312    function ">"
 313      (Left  : Unbounded_String;
 314       Right : Unbounded_String) return Boolean
 315    with
 316      Global => null;
 317
 318    function ">"
 319      (Left  : Unbounded_String;
 320       Right : String) return Boolean
 321    with
 322      Global => null;
 323
 324    function ">"
 325      (Left  : String;
 326       Right : Unbounded_String) return Boolean
 327    with
 328      Global => null;
 329
 330    function ">="
 331      (Left  : Unbounded_String;
 332       Right : Unbounded_String) return Boolean
 333    with
 334      Global => null;
 335
 336    function ">="
 337      (Left  : Unbounded_String;
 338       Right : String) return Boolean
 339    with
 340      Global => null;
 341
 342    function ">="
 343      (Left  : String;
 344       Right : Unbounded_String) return Boolean
 345    with
 346      Global => null;
 347
 348    --  Each of the functions "=", "<", ">", "<=", and ">=" returns the same
 349    --  result as the corresponding String operation applied to the String
 350    --  values given or represented by Left and Right.
 351
 352    ------------------------
 353    -- Search Subprograms --
 354    ------------------------
 355
 356    function Index
 357      (Source  : Unbounded_String;
 358       Pattern : String;
 359       Going   : Direction := Forward;
 360       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
 361    with
 362      Pre    => Pattern'Length /= 0,
 363      Global => null;
 364
 365    function Index
 366      (Source  : Unbounded_String;
 367       Pattern : String;
 368       Going   : Direction := Forward;
 369       Mapping : Maps.Character_Mapping_Function) return Natural
 370    with
 371      Pre    => Pattern'Length /= 0,
 372      Global => null;
 373
 374    function Index
 375      (Source : Unbounded_String;
 376       Set    : Maps.Character_Set;
 377       Test   : Membership := Inside;
 378       Going  : Direction  := Forward) return Natural
 379    with
 380      Global => null;
 381
 382    function Index
 383      (Source  : Unbounded_String;
 384       Pattern : String;
 385       From    : Positive;
 386       Going   : Direction := Forward;
 387       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
 388    with
 389      Pre    => (if Length (Source) /= 0 then From <= Length (Source))
 390                and then Pattern'Length /= 0,
 391      Global => null;
 392    pragma Ada_05 (Index);
 393
 394    function Index
 395      (Source  : Unbounded_String;
 396       Pattern : String;
 397       From    : Positive;
 398       Going   : Direction := Forward;
 399       Mapping : Maps.Character_Mapping_Function) return Natural
 400    with
 401      Pre    => (if Length (Source) /= 0 then From <= Length (Source))
 402                and then Pattern'Length /= 0,
 403      Global => null;
 404    pragma Ada_05 (Index);
 405
 406    function Index
 407      (Source  : Unbounded_String;
 408       Set     : Maps.Character_Set;
 409       From    : Positive;
 410       Test    : Membership := Inside;
 411       Going   : Direction := Forward) return Natural
 412    with
 413      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
 414      Global => null;
 415    pragma Ada_05 (Index);
 416
 417    function Index_Non_Blank
 418      (Source : Unbounded_String;
 419       Going  : Direction := Forward) return Natural
 420    with
 421      Global => null;
 422
 423    function Index_Non_Blank
 424      (Source : Unbounded_String;
 425       From   : Positive;
 426       Going  : Direction := Forward) return Natural
 427    with
 428      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
 429      Global => null;
 430    pragma Ada_05 (Index_Non_Blank);
 431
 432    function Count
 433      (Source  : Unbounded_String;
 434       Pattern : String;
 435       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
 436    with
 437      Pre    => Pattern'Length /= 0,
 438      Global => null;
 439
 440    function Count
 441      (Source  : Unbounded_String;
 442       Pattern : String;
 443       Mapping : Maps.Character_Mapping_Function) return Natural
 444    with
 445      Pre    => Pattern'Length /= 0,
 446      Global => null;
 447
 448    function Count
 449      (Source : Unbounded_String;
 450       Set    : Maps.Character_Set) return Natural
 451    with
 452      Global => null;
 453
 454    procedure Find_Token
 455      (Source : Unbounded_String;
 456       Set    : Maps.Character_Set;
 457       From   : Positive;
 458       Test   : Membership;
 459       First  : out Positive;
 460       Last   : out Natural)
 461    with
 462      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
 463      Global => null;
 464    pragma Ada_2012 (Find_Token);
 465
 466    procedure Find_Token
 467      (Source : Unbounded_String;
 468       Set    : Maps.Character_Set;
 469       Test   : Membership;
 470       First  : out Positive;
 471       Last   : out Natural)
 472    with
 473      Global => null;
 474
 475    --  Each of the search subprograms (Index, Index_Non_Blank, Count,
 476    --  Find_Token) has the same effect as the corresponding subprogram in
 477    --  Strings.Fixed applied to the string represented by the Unbounded_String
 478    --  parameter.
 479
 480    ------------------------------------
 481    -- String Translation Subprograms --
 482    ------------------------------------
 483
 484    function Translate
 485      (Source  : Unbounded_String;
 486       Mapping : Maps.Character_Mapping) return Unbounded_String
 487    with
 488      Post   => Length (Translate'Result) = Length (Source),
 489      Global => null;
 490
 491    procedure Translate
 492      (Source  : in out Unbounded_String;
 493       Mapping : Maps.Character_Mapping)
 494    with
 495      Post   => Length (Source) = Length (Source)'Old,
 496      Global => null;
 497
 498    function Translate
 499      (Source  : Unbounded_String;
 500       Mapping : Maps.Character_Mapping_Function) return Unbounded_String
 501    with
 502      Post   => Length (Translate'Result) = Length (Source),
 503      Global => null;
 504
 505    procedure Translate
 506      (Source  : in out Unbounded_String;
 507       Mapping : Maps.Character_Mapping_Function)
 508    with
 509      Post   => Length (Source) = Length (Source)'Old,
 510      Global => null;
 511
 512    --  The Translate function has an analogous effect to the corresponding
 513    --  subprogram in Strings.Fixed. The translation is applied to the string
 514    --  represented by the Unbounded_String parameter, and the result is
 515    --  converted (via To_Unbounded_String) to an Unbounded_String.
 516
 517    ---------------------------------------
 518    -- String Transformation Subprograms --
 519    ---------------------------------------
 520
 521    function Replace_Slice
 522      (Source : Unbounded_String;
 523       Low    : Positive;
 524       High   : Natural;
 525       By     : String) return Unbounded_String
 526    with
 527      Pre            =>
 528        Low - 1 <= Length (Source)
 529          and then (if High >= Low
 530                    then Low - 1
 531                      <= Natural'Last - By'Length
 532                       - Natural'Max (Length (Source) - High, 0)
 533                    else Length (Source) <= Natural'Last - By'Length),
 534      Contract_Cases =>
 535        (High >= Low =>
 536           Length (Replace_Slice'Result)
 537         = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
 538         others      =>
 539           Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
 540      Global         => null;
 541
 542    procedure Replace_Slice
 543      (Source : in out Unbounded_String;
 544       Low    : Positive;
 545       High   : Natural;
 546       By     : String)
 547    with
 548      Pre            =>
 549        Low - 1 <= Length (Source)
 550          and then (if High >= Low
 551                    then Low - 1
 552                      <= Natural'Last - By'Length
 553                       - Natural'Max (Length (Source) - High, 0)
 554                    else Length (Source) <= Natural'Last - By'Length),
 555      Contract_Cases =>
 556        (High >= Low =>
 557           Length (Source)
 558         = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
 559         others      =>
 560           Length (Source) = Length (Source)'Old + By'Length),
 561      Global         => null;
 562
 563    function Insert
 564      (Source   : Unbounded_String;
 565       Before   : Positive;
 566       New_Item : String) return Unbounded_String
 567    with
 568      Pre    => Before - 1 <= Length (Source)
 569                  and then New_Item'Length <= Natural'Last - Length (Source),
 570      Post   => Length (Insert'Result) = Length (Source) + New_Item'Length,
 571      Global => null;
 572
 573    procedure Insert
 574      (Source   : in out Unbounded_String;
 575       Before   : Positive;
 576       New_Item : String)
 577    with
 578      Pre    => Before - 1 <= Length (Source)
 579                  and then New_Item'Length <= Natural'Last - Length (Source),
 580      Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
 581      Global => null;
 582
 583    function Overwrite
 584      (Source   : Unbounded_String;
 585       Position : Positive;
 586       New_Item : String) return Unbounded_String
 587    with
 588      Pre    => Position - 1 <= Length (Source)
 589                  and then (if New_Item'Length /= 0
 590                            then
 591                              New_Item'Length <= Natural'Last - (Position - 1)),
 592      Post   =>
 593        Length (Overwrite'Result)
 594      = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
 595      Global => null;
 596
 597    procedure Overwrite
 598      (Source   : in out Unbounded_String;
 599       Position : Positive;
 600       New_Item : String)
 601    with
 602      Pre    => Position - 1 <= Length (Source)
 603                  and then (if New_Item'Length /= 0
 604                            then
 605                              New_Item'Length <= Natural'Last - (Position - 1)),
 606      Post   =>
 607        Length (Source)
 608      = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
 609
 610      Global => null;
 611
 612    function Delete
 613      (Source  : Unbounded_String;
 614       From    : Positive;
 615       Through : Natural) return Unbounded_String
 616    with
 617      Pre            => (if Through <= From then From - 1 <= Length (Source)),
 618      Contract_Cases =>
 619        (Through >= From =>
 620           Length (Delete'Result) = Length (Source) - (Through - From + 1),
 621         others          =>
 622           Length (Delete'Result) = Length (Source)),
 623      Global         => null;
 624
 625    procedure Delete
 626      (Source  : in out Unbounded_String;
 627       From    : Positive;
 628       Through : Natural)
 629    with
 630      Pre            => (if Through <= From then From - 1 <= Length (Source)),
 631      Contract_Cases =>
 632        (Through >= From =>
 633           Length (Source) = Length (Source)'Old - (Through - From + 1),
 634         others          =>
 635           Length (Source) = Length (Source)'Old),
 636      Global         => null;
 637
 638    function Trim
 639      (Source : Unbounded_String;
 640       Side   : Trim_End) return Unbounded_String
 641    with
 642      Post   => Length (Trim'Result) <= Length (Source),
 643      Global => null;
 644
 645    procedure Trim
 646      (Source : in out Unbounded_String;
 647       Side   : Trim_End)
 648    with
 649      Post   => Length (Source) <= Length (Source)'Old,
 650      Global => null;
 651
 652    function Trim
 653      (Source : Unbounded_String;
 654       Left   : Maps.Character_Set;
 655       Right  : Maps.Character_Set) return Unbounded_String
 656    with
 657      Post   => Length (Trim'Result) <= Length (Source),
 658      Global => null;
 659
 660    procedure Trim
 661      (Source : in out Unbounded_String;
 662       Left   : Maps.Character_Set;
 663       Right  : Maps.Character_Set)
 664    with
 665      Post   => Length (Source) <= Length (Source)'Old,
 666      Global => null;
 667
 668    function Head
 669      (Source : Unbounded_String;
 670       Count  : Natural;
 671       Pad    : Character := Space) return Unbounded_String
 672    with
 673      Post   => Length (Head'Result) = Count,
 674      Global => null;
 675
 676    procedure Head
 677      (Source : in out Unbounded_String;
 678       Count  : Natural;
 679       Pad    : Character := Space)
 680    with
 681      Post   => Length (Source) = Count,
 682      Global => null;
 683
 684    function Tail
 685      (Source : Unbounded_String;
 686       Count  : Natural;
 687       Pad    : Character := Space) return Unbounded_String
 688    with
 689      Post   => Length (Tail'Result) = Count,
 690      Global => null;
 691
 692    procedure Tail
 693      (Source : in out Unbounded_String;
 694       Count  : Natural;
 695       Pad    : Character := Space)
 696    with
 697      Post   => Length (Source) = Count,
 698      Global => null;
 699
 700    function "*"
 701      (Left  : Natural;
 702       Right : Character) return Unbounded_String
 703    with
 704      Pre    => Left <= Natural'Last,
 705      Post   => Length ("*"'Result) = Left,
 706      Global => null;
 707
 708    function "*"
 709      (Left  : Natural;
 710       Right : String) return Unbounded_String
 711    with
 712      Pre    => (if Left /= 0 then Right'Length <= Natural'Last / Left),
 713      Post   => Length ("*"'Result) = Left * Right'Length,
 714      Global => null;
 715
 716    function "*"
 717      (Left  : Natural;
 718       Right : Unbounded_String) return Unbounded_String
 719    with
 720      Pre    => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
 721      Post   => Length ("*"'Result) = Left * Length (Right),
 722      Global => null;
 723
 724    --  Each of the transformation functions (Replace_Slice, Insert, Overwrite,
 725    --  Delete), selector functions (Trim, Head, Tail), and constructor
 726    --  functions ("*") is likewise analogous to its corresponding subprogram in
 727    --  Strings.Fixed. For each of the subprograms, the corresponding
 728    --  fixed-length string subprogram is applied to the string represented by
 729    --  the Unbounded_String parameter, and To_Unbounded_String is applied the
 730    --  result string.
 731    --
 732    --  For each of the procedures Translate, Replace_Slice, Insert, Overwrite,
 733    --  Delete, Trim, Head, and Tail, the resulting string represented by the
 734    --  Source parameter is given by the corresponding function for fixed-length
 735    --  strings applied to the string represented by Source's original value.
 736
 737 private
 738    pragma SPARK_Mode (Off);  --  Controlled types are not in SPARK
 739
 740    pragma Inline (Length);
 741
 742    package AF renames Ada.Finalization;
 743
 744    Null_String : aliased String := "";
 745
 746    function To_Unbounded (S : String) return Unbounded_String
 747      renames To_Unbounded_String;
 748
 749    type Unbounded_String is new AF.Controlled with record
 750       Reference : not null String_Access := Null_String'Access;
 751       Last      : Natural                := 0;
 752    end record with Put_Image => Put_Image;
 753
 754    procedure Put_Image
 755      (S : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class;
 756       V : Unbounded_String);
 757
 758    --  The Unbounded_String is using a buffered implementation to increase
 759    --  speed of the Append/Delete/Insert procedures. The Reference string
 760    --  pointer above contains the current string value and extra room at the
 761    --  end to be used by the next Append routine. Last is the index of the
 762    --  string ending character. So the current string value is really
 763    --  Reference (1 .. Last).
 764
 765    pragma Stream_Convert (Unbounded_String, To_Unbounded, To_String);
 766    --  Provide stream routines without dragging in Ada.Streams
 767
 768    pragma Finalize_Storage_Only (Unbounded_String);
 769    --  Finalization is required only for freeing storage
 770
 771    procedure Initialize (Object : in out Unbounded_String);
 772    procedure Adjust     (Object : in out Unbounded_String);
 773    procedure Finalize   (Object : in out Unbounded_String);
 774
 775    procedure Realloc_For_Chunk
 776      (Source     : in out Unbounded_String;
 777       Chunk_Size : Natural);
 778    pragma Inline (Realloc_For_Chunk);
 779    --  Adjust the size allocated for the string. Add at least Chunk_Size so it
 780    --  is safe to add a string of this size at the end of the current content.
 781    --  The real size allocated for the string is Chunk_Size + x of the current
 782    --  string size. This buffered handling makes the Append unbounded string
 783    --  routines very fast. This spec is in the private part so that it can be
 784    --  accessed from children (e.g. from Unbounded.Text_IO).
 785
 786    Null_Unbounded_String : constant Unbounded_String :=
 787                              (AF.Controlled with
 788                                 Reference => Null_String'Access,
 789                                 Last      => 0);
 790 end Ada.Strings.Unbounded;