From: Yannick Moy Date: Tue, 27 Jul 2021 14:19:05 +0000 (+0200) Subject: [Ada] Add Ada RM description of Ada.Strings.Bounded as comments in the spec X-Git-Tag: basepoints/gcc-13~4188 X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=448a20ee501f177aff829804bce51487b20efcfb;p=thirdparty%2Fgcc.git [Ada] Add Ada RM description of Ada.Strings.Bounded as comments in the spec gcc/ada/ * libgnat/a-strbou.ads: Add comments. --- diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads index 31c1cc97093e..e8201843f7a8 100644 --- a/gcc/ada/libgnat/a-strbou.ads +++ b/gcc/ada/libgnat/a-strbou.ads @@ -33,6 +33,16 @@ -- -- ------------------------------------------------------------------------------ +-- The language-defined package Strings.Bounded provides a generic package +-- each of whose instances yields a private type Bounded_String and a set +-- of operations. An object of a particular Bounded_String type represents +-- a String whose low bound is 1 and whose length can vary conceptually +-- between 0 and a maximum size established at the generic instantiation. The +-- subprograms for fixed-length string handling are either overloaded directly +-- for Bounded_String, or are modified as needed to reflect the variability in +-- length. Additionally, since the Bounded_String type is private, appropriate +-- constructor and selector operations are provided. + with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; with Ada.Strings.Superbounded; with Ada.Strings.Search; @@ -65,11 +75,16 @@ package Ada.Strings.Bounded with SPARK_Mode is pragma Preelaborable_Initialization (Bounded_String); Null_Bounded_String : constant Bounded_String; + -- Null_Bounded_String represents the null string. If an object of type + -- Bounded_String is not otherwise initialized, it will be initialized + -- to the same value as Null_Bounded_String. subtype Length_Range is Natural range 0 .. Max_Length; function Length (Source : Bounded_String) return Length_Range with Global => null; + -- The Length function returns the length of the string represented by + -- Source. -------------------------------------------------------- -- Conversion, Concatenation, and Selection Functions -- @@ -94,9 +109,24 @@ package Ada.Strings.Bounded with SPARK_Mode is => To_String (To_Bounded_String'Result) = Source (Source'First .. Source'First - 1 + Max_Length)); + -- If Source'Length <= Max_Length, then this function returns a + -- Bounded_String that represents Source. Otherwise, the effect + -- depends on the value of Drop: + -- + -- * If Drop=Left, then the result is a Bounded_String that represents + -- the string comprising the rightmost Max_Length characters of + -- Source. + -- + -- * If Drop=Right, then the result is a Bounded_String that represents + -- the string comprising the leftmost Max_Length characters of Source. + -- + -- * If Drop=Error, then Strings.Length_Error is propagated. function To_String (Source : Bounded_String) return String with Global => null; + -- To_String returns the String value with lower bound 1 + -- represented by Source. If B is a Bounded_String, then + -- B = To_Bounded_String(To_String(B)). procedure Set_Bounded_String (Target : out Bounded_String; @@ -119,6 +149,14 @@ package Ada.Strings.Bounded with SPARK_Mode is To_String (Target) = Source (Source'First .. Source'First - 1 + Max_Length)); pragma Ada_05 (Set_Bounded_String); + -- Equivalent to Target := To_Bounded_String (Source, Drop); + + -- Each of the Append functions returns a Bounded_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_Bounded_String to the + -- concatenation result string, with Drop as provided to the Append + -- function. function Append (Left : Bounded_String; @@ -324,6 +362,10 @@ package Ada.Strings.Bounded with SPARK_Mode is Slice (Right, 1, Max_Length - 1) and then Element (Append'Result, 1) = Left); + -- Each of the procedures Append(Source, New_Item, Drop) has the same + -- effect as the corresponding assignment + -- Source := Append(Source, New_Item, Drop). + procedure Append (Source : in out Bounded_String; New_Item : Bounded_String; @@ -455,6 +497,9 @@ package Ada.Strings.Bounded with SPARK_Mode is Slice (Source'Old, 2, Max_Length) and then Element (Source, Max_Length) = New_Item); + -- Each of the "&" functions has the same effect as the corresponding + -- Append function, with Error as the Drop parameter. + function "&" (Left : Bounded_String; Right : Bounded_String) return Bounded_String @@ -516,6 +561,8 @@ package Ada.Strings.Bounded with SPARK_Mode is 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 Bounded_String; @@ -528,6 +575,9 @@ package Ada.Strings.Bounded with SPARK_Mode is Element (Source, K) = (if K = Index then By else Element (Source'Old, K))), 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 : Bounded_String; @@ -536,6 +586,10 @@ package Ada.Strings.Bounded with SPARK_Mode is with Pre => Low - 1 <= Length (Source) and then High <= Length (Source), 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 Bounded_Slice (Source : Bounded_String; @@ -546,6 +600,9 @@ package Ada.Strings.Bounded with SPARK_Mode is Post => To_String (Bounded_Slice'Result) = Slice (Source, Low, High), Global => null; pragma Ada_05 (Bounded_Slice); + -- Returns the slice at positions Low through High in the string + -- represented by Source as a bounded string; propagates Index_Error + -- if Low > Length(Source)+1 or High > Length(Source). procedure Bounded_Slice (Source : Bounded_String; @@ -557,6 +614,11 @@ package Ada.Strings.Bounded with SPARK_Mode is Post => To_String (Target) = Slice (Source, Low, High), Global => null; pragma Ada_05 (Bounded_Slice); + -- Equivalent to Target := Bounded_Slice (Source, Low, High); + + -- Each of the functions "=", "<", ">", "<=", and ">=" returns the same + -- result as the corresponding String operation applied to the String + -- values given or represented by the two parameters. function "=" (Left : Bounded_String; @@ -667,6 +729,11 @@ package Ada.Strings.Bounded with SPARK_Mode is -- Search Functions -- ---------------------- + -- 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 Bounded_String + -- parameter. + function Index (Source : Bounded_String; Pattern : String; @@ -1230,6 +1297,16 @@ package Ada.Strings.Bounded with SPARK_Mode is -- String Translation Subprograms -- ------------------------------------ + -- Each of the Translate subprograms, when applied to a Bounded_String, + -- has an analogous effect to the corresponding subprogram in + -- Strings.Fixed. For the Translate function, the translation is applied + -- to the string represented by the Bounded_String parameter, and the + -- result is converted (via To_Bounded_String) to a Bounded_String. For + -- the Translate procedure, the string represented by the Bounded_String + -- parameter after the translation is given by the Translate function + -- for fixed-length strings applied to the string represented by the + -- original value of the parameter. + function Translate (Source : Bounded_String; Mapping : Maps.Character_Mapping) return Bounded_String @@ -1278,6 +1355,19 @@ package Ada.Strings.Bounded with SPARK_Mode is -- String Transformation Subprograms -- --------------------------------------- + -- Each of the transformation subprograms (Replace_Slice, Insert, + -- Overwrite, Delete), selector subprograms (Trim, Head, Tail), and + -- constructor functions ("*") has an effect based on its corresponding + -- subprogram in Strings.Fixed, and Replicate is based on Fixed."*". + -- In the case of a function, the corresponding fixed-length string + -- subprogram is applied to the string represented by the Bounded_String + -- parameter. To_Bounded_String is applied the result string, with Drop + -- (or Error in the case of Generic_Bounded_Length."*") determining + -- the effect when the string length exceeds Max_Length. In + -- the case of a procedure, the corresponding function in + -- Strings.Bounded.Generic_Bounded_Length is applied, with the + -- result assigned into the Source parameter. + function Replace_Slice (Source : Bounded_String; Low : Positive;