blob: 37c946620aa3e23719b053b86f0e21fb91aeda0d [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- GNAT RUN-TIME COMPONENTS --
-- --
-- A D A . S T R I N G S . U N B O U N D E D --
-- --
-- S p e c --
-- --
-- Copyright (C) 1992-2022, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- apply solely to the contents of the part following the private keyword. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
-- --
-- GNAT was originally developed by the GNAT team at New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc. --
-- --
------------------------------------------------------------------------------
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
-- setting the corresponding assertion policy to Ignore.
pragma Assertion_Policy (Pre => Ignore);
with Ada.Strings.Maps;
with Ada.Finalization;
private with Ada.Strings.Text_Buffers;
-- The language-defined package Strings.Unbounded provides a private type
-- Unbounded_String and a set of operations. An object of type
-- Unbounded_String represents a String whose low bound is 1 and whose length
-- can vary conceptually between 0 and Natural'Last. The subprograms for
-- fixed-length string handling are either overloaded directly for
-- Unbounded_String, or are modified as needed to reflect the flexibility in
-- length. Since the Unbounded_String type is private, relevant constructor
-- and selector operations are provided.
package Ada.Strings.Unbounded with
SPARK_Mode,
Initial_Condition => Length (Null_Unbounded_String) = 0
is
pragma Preelaborate;
type Unbounded_String is private with
Default_Initial_Condition => Length (Unbounded_String) = 0;
pragma Preelaborable_Initialization (Unbounded_String);
Null_Unbounded_String : constant Unbounded_String;
-- Represents the null String. If an object of type Unbounded_String is not
-- otherwise initialized, it will be initialized to the same value as
-- Null_Unbounded_String.
function Length (Source : Unbounded_String) return Natural with
Global => null;
-- Returns the length of the String represented by Source
type String_Access is access all String;
-- Provides a (nonprivate) access type for explicit processing of
-- unbounded-length strings.
procedure Free (X : in out String_Access) with SPARK_Mode => Off;
-- Performs an unchecked deallocation of an object of type String_Access
--------------------------------------------------------
-- Conversion, Concatenation, and Selection Functions --
--------------------------------------------------------
function To_Unbounded_String
(Source : String) return Unbounded_String
with
Post => Length (To_Unbounded_String'Result) = Source'Length,
Global => null;
-- Returns an Unbounded_String that represents Source
function To_Unbounded_String
(Length : Natural) return Unbounded_String
with
Post =>
Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length,
Global => null;
-- Returns an Unbounded_String that represents an uninitialized String
-- whose length is Length.
function To_String (Source : Unbounded_String) return String with
Post => To_String'Result'Length = Length (Source),
Global => null;
-- Returns the String with lower bound 1 represented by Source
-- To_String and To_Unbounded_String are related as follows:
--
-- * If S is a String, then To_String (To_Unbounded_String (S)) = S.
--
-- * If U is an Unbounded_String, then
-- To_Unbounded_String (To_String (U)) = U.
procedure Set_Unbounded_String
(Target : out Unbounded_String;
Source : String)
with
Global => null;
pragma Ada_05 (Set_Unbounded_String);
-- Sets Target to an Unbounded_String that represents Source
procedure Append
(Source : in out Unbounded_String;
New_Item : Unbounded_String)
with
Pre => Length (New_Item) <= Natural'Last - Length (Source),
Post => Length (Source) = Length (Source)'Old + Length (New_Item),
Global => null;
procedure Append
(Source : in out Unbounded_String;
New_Item : String)
with
Pre => New_Item'Length <= Natural'Last - Length (Source),
Post => Length (Source) = Length (Source)'Old + New_Item'Length,
Global => null;
procedure Append
(Source : in out Unbounded_String;
New_Item : Character)
with
Pre => Length (Source) < Natural'Last,
Post => Length (Source) = Length (Source)'Old + 1,
Global => null;
-- For each of the Append procedures, the resulting string represented by
-- the Source parameter is given by the concatenation of the original value
-- of Source and the value of New_Item.
function "&"
(Left : Unbounded_String;
Right : Unbounded_String) return Unbounded_String
with
Pre => Length (Right) <= Natural'Last - Length (Left),
Post => Length ("&"'Result) = Length (Left) + Length (Right),
Global => null;
function "&"
(Left : Unbounded_String;
Right : String) return Unbounded_String
with
Pre => Right'Length <= Natural'Last - Length (Left),
Post => Length ("&"'Result) = Length (Left) + Right'Length,
Global => null;
function "&"
(Left : String;
Right : Unbounded_String) return Unbounded_String
with
Pre => Left'Length <= Natural'Last - Length (Right),
Post => Length ("&"'Result) = Left'Length + Length (Right),
Global => null;
function "&"
(Left : Unbounded_String;
Right : Character) return Unbounded_String
with
Pre => Length (Left) < Natural'Last,
Post => Length ("&"'Result) = Length (Left) + 1,
Global => null;
function "&"
(Left : Character;
Right : Unbounded_String) return Unbounded_String
with
Pre => Length (Right) < Natural'Last,
Post => Length ("&"'Result) = Length (Right) + 1,
Global => null;
-- Each of the "&" functions returns an Unbounded_String obtained by
-- concatenating the string or character given or represented by one of the
-- parameters, with the string or character given or represented by the
-- other parameter, and applying To_Unbounded_String to the concatenation
-- result string.
function Element
(Source : Unbounded_String;
Index : Positive) return Character
with
Pre => Index <= Length (Source),
Global => null;
-- Returns the character at position Index in the string represented by
-- Source; propagates Index_Error if Index > Length (Source).
procedure Replace_Element
(Source : in out Unbounded_String;
Index : Positive;
By : Character)
with
Pre => Index <= Length (Source),
Post => Length (Source) = Length (Source)'Old,
Global => null;
-- Updates Source such that the character at position Index in the string
-- represented by Source is By; propagates Index_Error if
-- Index > Length (Source).
function Slice
(Source : Unbounded_String;
Low : Positive;
High : Natural) return String
with
Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
Post => Slice'Result'Length = Natural'Max (0, High - Low + 1),
Global => null;
-- Returns the slice at positions Low through High in the string
-- represented by Source; propagates Index_Error if
-- Low > Length (Source) + 1 or High > Length (Source). The bounds of the
-- returned string are Low and High.
function Unbounded_Slice
(Source : Unbounded_String;
Low : Positive;
High : Natural) return Unbounded_String
with
Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
Post =>
Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
Global => null;
pragma Ada_05 (Unbounded_Slice);
-- Returns the slice at positions Low through High in the string
-- represented by Source as an Unbounded_String. This propagates
-- Index_Error if Low > Length(Source) + 1 or High > Length (Source).
procedure Unbounded_Slice
(Source : Unbounded_String;
Target : out Unbounded_String;
Low : Positive;
High : Natural)
with
Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
Post => Length (Target) = Natural'Max (0, High - Low + 1),
Global => null;
pragma Ada_05 (Unbounded_Slice);
-- Sets Target to the Unbounded_String representing the slice at positions
-- Low through High in the string represented by Source. This propagates
-- Index_Error if Low > Length(Source) + 1 or High > Length (Source).
function "="
(Left : Unbounded_String;
Right : Unbounded_String) return Boolean
with
Global => null;
function "="
(Left : Unbounded_String;
Right : String) return Boolean
with
Global => null;
function "="
(Left : String;
Right : Unbounded_String) return Boolean
with
Global => null;
function "<"
(Left : Unbounded_String;
Right : Unbounded_String) return Boolean
with
Global => null;
function "<"
(Left : Unbounded_String;
Right : String) return Boolean
with
Global => null;
function "<"
(Left : String;
Right : Unbounded_String) return Boolean
with
Global => null;
function "<="
(Left : Unbounded_String;
Right : Unbounded_String) return Boolean
with
Global => null;
function "<="
(Left : Unbounded_String;
Right : String) return Boolean
with
Global => null;
function "<="
(Left : String;
Right : Unbounded_String) return Boolean
with
Global => null;
function ">"
(Left : Unbounded_String;
Right : Unbounded_String) return Boolean
with
Global => null;
function ">"
(Left : Unbounded_String;
Right : String) return Boolean
with
Global => null;
function ">"
(Left : String;
Right : Unbounded_String) return Boolean
with
Global => null;
function ">="
(Left : Unbounded_String;
Right : Unbounded_String) return Boolean
with
Global => null;
function ">="
(Left : Unbounded_String;
Right : String) return Boolean
with
Global => null;
function ">="
(Left : String;
Right : Unbounded_String) return Boolean
with
Global => null;
-- Each of the functions "=", "<", ">", "<=", and ">=" returns the same
-- result as the corresponding String operation applied to the String
-- values given or represented by Left and Right.
------------------------
-- Search Subprograms --
------------------------
function Index
(Source : Unbounded_String;
Pattern : String;
Going : Direction := Forward;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
with
Pre => Pattern'Length /= 0,
Global => null;
function Index
(Source : Unbounded_String;
Pattern : String;
Going : Direction := Forward;
Mapping : Maps.Character_Mapping_Function) return Natural
with
Pre => Pattern'Length /= 0,
Global => null;
function Index
(Source : Unbounded_String;
Set : Maps.Character_Set;
Test : Membership := Inside;
Going : Direction := Forward) return Natural
with
Global => null;
function Index
(Source : Unbounded_String;
Pattern : String;
From : Positive;
Going : Direction := Forward;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
with
Pre => (if Length (Source) /= 0 then From <= Length (Source))
and then Pattern'Length /= 0,
Global => null;
pragma Ada_05 (Index);
function Index
(Source : Unbounded_String;
Pattern : String;
From : Positive;
Going : Direction := Forward;
Mapping : Maps.Character_Mapping_Function) return Natural
with
Pre => (if Length (Source) /= 0 then From <= Length (Source))
and then Pattern'Length /= 0,
Global => null;
pragma Ada_05 (Index);
function Index
(Source : Unbounded_String;
Set : Maps.Character_Set;
From : Positive;
Test : Membership := Inside;
Going : Direction := Forward) return Natural
with
Pre => (if Length (Source) /= 0 then From <= Length (Source)),
Global => null;
pragma Ada_05 (Index);
function Index_Non_Blank
(Source : Unbounded_String;
Going : Direction := Forward) return Natural
with
Global => null;
function Index_Non_Blank
(Source : Unbounded_String;
From : Positive;
Going : Direction := Forward) return Natural
with
Pre => (if Length (Source) /= 0 then From <= Length (Source)),
Global => null;
pragma Ada_05 (Index_Non_Blank);
function Count
(Source : Unbounded_String;
Pattern : String;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
with
Pre => Pattern'Length /= 0,
Global => null;
function Count
(Source : Unbounded_String;
Pattern : String;
Mapping : Maps.Character_Mapping_Function) return Natural
with
Pre => Pattern'Length /= 0,
Global => null;
function Count
(Source : Unbounded_String;
Set : Maps.Character_Set) return Natural
with
Global => null;
procedure Find_Token
(Source : Unbounded_String;
Set : Maps.Character_Set;
From : Positive;
Test : Membership;
First : out Positive;
Last : out Natural)
with
Pre => (if Length (Source) /= 0 then From <= Length (Source)),
Global => null;
pragma Ada_2012 (Find_Token);
procedure Find_Token
(Source : Unbounded_String;
Set : Maps.Character_Set;
Test : Membership;
First : out Positive;
Last : out Natural)
with
Global => null;
-- Each of the search subprograms (Index, Index_Non_Blank, Count,
-- Find_Token) has the same effect as the corresponding subprogram in
-- Strings.Fixed applied to the string represented by the Unbounded_String
-- parameter.
------------------------------------
-- String Translation Subprograms --
------------------------------------
function Translate
(Source : Unbounded_String;
Mapping : Maps.Character_Mapping) return Unbounded_String
with
Post => Length (Translate'Result) = Length (Source),
Global => null;
procedure Translate
(Source : in out Unbounded_String;
Mapping : Maps.Character_Mapping)
with
Post => Length (Source) = Length (Source)'Old,
Global => null;
function Translate
(Source : Unbounded_String;
Mapping : Maps.Character_Mapping_Function) return Unbounded_String
with
Post => Length (Translate'Result) = Length (Source),
Global => null;
procedure Translate
(Source : in out Unbounded_String;
Mapping : Maps.Character_Mapping_Function)
with
Post => Length (Source) = Length (Source)'Old,
Global => null;
-- The Translate function has an analogous effect to the corresponding
-- subprogram in Strings.Fixed. The translation is applied to the string
-- represented by the Unbounded_String parameter, and the result is
-- converted (via To_Unbounded_String) to an Unbounded_String.
---------------------------------------
-- String Transformation Subprograms --
---------------------------------------
function Replace_Slice
(Source : Unbounded_String;
Low : Positive;
High : Natural;
By : String) return Unbounded_String
with
Pre =>
Low - 1 <= Length (Source)
and then (if High >= Low
then Low - 1
<= Natural'Last - By'Length
- Natural'Max (Length (Source) - High, 0)
else Length (Source) <= Natural'Last - By'Length),
Contract_Cases =>
(High >= Low =>
Length (Replace_Slice'Result)
= Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
others =>
Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
Global => null;
procedure Replace_Slice
(Source : in out Unbounded_String;
Low : Positive;
High : Natural;
By : String)
with
Pre =>
Low - 1 <= Length (Source)
and then (if High >= Low
then Low - 1
<= Natural'Last - By'Length
- Natural'Max (Length (Source) - High, 0)
else Length (Source) <= Natural'Last - By'Length),
Contract_Cases =>
(High >= Low =>
Length (Source)
= Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
others =>
Length (Source) = Length (Source)'Old + By'Length),
Global => null;
function Insert
(Source : Unbounded_String;
Before : Positive;
New_Item : String) return Unbounded_String
with
Pre => Before - 1 <= Length (Source)
and then New_Item'Length <= Natural'Last - Length (Source),
Post => Length (Insert'Result) = Length (Source) + New_Item'Length,
Global => null;
procedure Insert
(Source : in out Unbounded_String;
Before : Positive;
New_Item : String)
with
Pre => Before - 1 <= Length (Source)
and then New_Item'Length <= Natural'Last - Length (Source),
Post => Length (Source) = Length (Source)'Old + New_Item'Length,
Global => null;
function Overwrite
(Source : Unbounded_String;
Position : Positive;
New_Item : String) return Unbounded_String
with
Pre => Position - 1 <= Length (Source)
and then (if New_Item'Length /= 0
then
New_Item'Length <= Natural'Last - (Position - 1)),
Post =>
Length (Overwrite'Result)
= Natural'Max (Length (Source), Position - 1 + New_Item'Length),
Global => null;
procedure Overwrite
(Source : in out Unbounded_String;
Position : Positive;
New_Item : String)
with
Pre => Position - 1 <= Length (Source)
and then (if New_Item'Length /= 0
then
New_Item'Length <= Natural'Last - (Position - 1)),
Post =>
Length (Source)
= Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
Global => null;
function Delete
(Source : Unbounded_String;
From : Positive;
Through : Natural) return Unbounded_String
with
Pre => (if Through <= From then From - 1 <= Length (Source)),
Contract_Cases =>
(Through >= From =>
Length (Delete'Result) = Length (Source) - (Through - From + 1),
others =>
Length (Delete'Result) = Length (Source)),
Global => null;
procedure Delete
(Source : in out Unbounded_String;
From : Positive;
Through : Natural)
with
Pre => (if Through <= From then From - 1 <= Length (Source)),
Contract_Cases =>
(Through >= From =>
Length (Source) = Length (Source)'Old - (Through - From + 1),
others =>
Length (Source) = Length (Source)'Old),
Global => null;
function Trim
(Source : Unbounded_String;
Side : Trim_End) return Unbounded_String
with
Post => Length (Trim'Result) <= Length (Source),
Global => null;
procedure Trim
(Source : in out Unbounded_String;
Side : Trim_End)
with
Post => Length (Source) <= Length (Source)'Old,
Global => null;
function Trim
(Source : Unbounded_String;
Left : Maps.Character_Set;
Right : Maps.Character_Set) return Unbounded_String
with
Post => Length (Trim'Result) <= Length (Source),
Global => null;
procedure Trim
(Source : in out Unbounded_String;
Left : Maps.Character_Set;
Right : Maps.Character_Set)
with
Post => Length (Source) <= Length (Source)'Old,
Global => null;
function Head
(Source : Unbounded_String;
Count : Natural;
Pad : Character := Space) return Unbounded_String
with
Post => Length (Head'Result) = Count,
Global => null;
procedure Head
(Source : in out Unbounded_String;
Count : Natural;
Pad : Character := Space)
with
Post => Length (Source) = Count,
Global => null;
function Tail
(Source : Unbounded_String;
Count : Natural;
Pad : Character := Space) return Unbounded_String
with
Post => Length (Tail'Result) = Count,
Global => null;
procedure Tail
(Source : in out Unbounded_String;
Count : Natural;
Pad : Character := Space)
with
Post => Length (Source) = Count,
Global => null;
function "*"
(Left : Natural;
Right : Character) return Unbounded_String
with
Pre => Left <= Natural'Last,
Post => Length ("*"'Result) = Left,
Global => null;
function "*"
(Left : Natural;
Right : String) return Unbounded_String
with
Pre => (if Left /= 0 then Right'Length <= Natural'Last / Left),
Post => Length ("*"'Result) = Left * Right'Length,
Global => null;
function "*"
(Left : Natural;
Right : Unbounded_String) return Unbounded_String
with
Pre => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
Post => Length ("*"'Result) = Left * Length (Right),
Global => null;
-- Each of the transformation functions (Replace_Slice, Insert, Overwrite,
-- Delete), selector functions (Trim, Head, Tail), and constructor
-- functions ("*") is likewise analogous to its corresponding subprogram in
-- Strings.Fixed. For each of the subprograms, the corresponding
-- fixed-length string subprogram is applied to the string represented by
-- the Unbounded_String parameter, and To_Unbounded_String is applied the
-- result string.
--
-- For each of the procedures Translate, Replace_Slice, Insert, Overwrite,
-- Delete, Trim, Head, and Tail, the resulting string represented by the
-- Source parameter is given by the corresponding function for fixed-length
-- strings applied to the string represented by Source's original value.
private
pragma SPARK_Mode (Off); -- Controlled types are not in SPARK
pragma Inline (Length);
package AF renames Ada.Finalization;
Null_String : aliased String := "";
function To_Unbounded (S : String) return Unbounded_String
renames To_Unbounded_String;
type Unbounded_String is new AF.Controlled with record
Reference : not null String_Access := Null_String'Access;
Last : Natural := 0;
end record with Put_Image => Put_Image;
procedure Put_Image
(S : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class;
V : Unbounded_String);
-- The Unbounded_String is using a buffered implementation to increase
-- speed of the Append/Delete/Insert procedures. The Reference string
-- pointer above contains the current string value and extra room at the
-- end to be used by the next Append routine. Last is the index of the
-- string ending character. So the current string value is really
-- Reference (1 .. Last).
pragma Stream_Convert (Unbounded_String, To_Unbounded, To_String);
-- Provide stream routines without dragging in Ada.Streams
pragma Finalize_Storage_Only (Unbounded_String);
-- Finalization is required only for freeing storage
procedure Initialize (Object : in out Unbounded_String);
procedure Adjust (Object : in out Unbounded_String);
procedure Finalize (Object : in out Unbounded_String);
procedure Realloc_For_Chunk
(Source : in out Unbounded_String;
Chunk_Size : Natural);
pragma Inline (Realloc_For_Chunk);
-- Adjust the size allocated for the string. Add at least Chunk_Size so it
-- is safe to add a string of this size at the end of the current content.
-- The real size allocated for the string is Chunk_Size + x of the current
-- string size. This buffered handling makes the Append unbounded string
-- routines very fast. This spec is in the private part so that it can be
-- accessed from children (e.g. from Unbounded.Text_IO).
Null_Unbounded_String : constant Unbounded_String :=
(AF.Controlled with
Reference => Null_String'Access,
Last => 0);
end Ada.Strings.Unbounded;