From 0b6694b4e41d394df12d159c319be4b1326745ca Mon Sep 17 00:00:00 2001 From: Joffrey Huguet Date: Wed, 10 Jul 2019 09:01:28 +0000 Subject: [PATCH] [Ada] Add contracts to Strings libraries This patch adds contracts to Ada.Strings libraries, in order to remove warnings when using these libraries in SPARK. 2019-07-10 Joffrey Huguet gcc/ada/ * libgnat/a-strbou.ads, libgnat/a-strfix.ads, libgnat/a-strunb.ads, libgnat/a-strunb__shared.ads: Add global contracts, contract cases, preconditions and postconditions to procedures and functions. From-SVN: r273334 --- gcc/ada/ChangeLog | 7 + gcc/ada/libgnat/a-strbou.ads | 521 +++++++++++++++++++++++---- gcc/ada/libgnat/a-strfix.ads | 246 +++++++++++-- gcc/ada/libgnat/a-strunb.ads | 403 +++++++++++++++++---- gcc/ada/libgnat/a-strunb__shared.ads | 405 +++++++++++++++++---- 5 files changed, 1328 insertions(+), 254 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 2c069ab125d..9d990336be7 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,10 @@ +2019-07-10 Joffrey Huguet + + * libgnat/a-strbou.ads, libgnat/a-strfix.ads, + libgnat/a-strunb.ads, libgnat/a-strunb__shared.ads: Add global + contracts, contract cases, preconditions and postconditions to + procedures and functions. + 2019-07-10 Doug Rupp * sysdep.c (__gnat_is_file_not_found_error): Reformulate to also diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads index f525ccf76a6..ae61b869e21 100644 --- a/gcc/ada/libgnat/a-strbou.ads +++ b/gcc/ada/libgnat/a-strbou.ads @@ -33,6 +33,12 @@ -- -- ------------------------------------------------------------------------------ +-- 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.Strings.Superbounded; @@ -43,7 +49,9 @@ package Ada.Strings.Bounded is Max : Positive; -- Maximum length of a Bounded_String - package Generic_Bounded_Length is + package Generic_Bounded_Length with + Initial_Condition => Length (Null_Bounded_String) = 0 + is Max_Length : constant Positive := Max; @@ -54,7 +62,8 @@ package Ada.Strings.Bounded is subtype Length_Range is Natural range 0 .. Max_Length; - function Length (Source : Bounded_String) return Length_Range; + function Length (Source : Bounded_String) return Length_Range with + Global => null; -------------------------------------------------------- -- Conversion, Concatenation, and Selection Functions -- @@ -62,162 +71,302 @@ package Ada.Strings.Bounded is function To_Bounded_String (Source : String; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => (if Source'Length > Max_Length then Drop /= Error), + Post => + Length (To_Bounded_String'Result) + = Natural'Min (Max_Length, Source'Length), + Global => null; - function To_String (Source : Bounded_String) return String; + function To_String (Source : Bounded_String) return String with + Post => To_String'Result'Length = Length (Source), + Global => null; procedure Set_Bounded_String (Target : out Bounded_String; Source : String; - Drop : Truncation := Error); + Drop : Truncation := Error) + with + Pre => (if Source'Length > Max_Length then Drop /= Error), + Post => Length (Target) = Natural'Min (Max_Length, Source'Length), + Global => null; pragma Ada_05 (Set_Bounded_String); function Append (Left : Bounded_String; Right : Bounded_String; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => + (if Length (Left) > Max_Length - Length (Right) + then Drop /= Error), + Post => + Length (Append'Result) + = Natural'Min (Max_Length, Length (Left) + Length (Right)), + Global => null; function Append (Left : Bounded_String; Right : String; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => + (if Right'Length > Max_Length - Length (Left) + then Drop /= Error), + Post => + Length (Append'Result) + = Natural'Min (Max_Length, Length (Left) + Right'Length), + Global => null; function Append (Left : String; Right : Bounded_String; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => + (if Left'Length > Max_Length - Length (Right) + then Drop /= Error), + Post => + Length (Append'Result) + = Natural'Min (Max_Length, Left'Length + Length (Right)), + Global => null; function Append (Left : Bounded_String; Right : Character; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => (if Length (Left) = Max_Length then Drop /= Error), + Post => + Length (Append'Result) + = Natural'Min (Max_Length, Length (Left) + 1), + Global => null; function Append (Left : Character; Right : Bounded_String; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => (if Length (Right) = Max_Length then Drop /= Error), + Post => + Length (Append'Result) + = Natural'Min (Max_Length, 1 + Length (Right)), + Global => null; procedure Append (Source : in out Bounded_String; New_Item : Bounded_String; - Drop : Truncation := Error); + Drop : Truncation := Error) + with + Pre => + (if Length (Source) > Max_Length - Length (New_Item) + then Drop /= Error), + Post => + Length (Source) + = Natural'Min (Max_Length, Length (Source)'Old + Length (New_Item)), + Global => null; procedure Append (Source : in out Bounded_String; New_Item : String; - Drop : Truncation := Error); + Drop : Truncation := Error) + with + Pre => + (if New_Item'Length > Max_Length - Length (Source) + then Drop /= Error), + Post => + Length (Source) + = Natural'Min (Max_Length, Length (Source)'Old + New_Item'Length), + Global => null; procedure Append (Source : in out Bounded_String; New_Item : Character; - Drop : Truncation := Error); + Drop : Truncation := Error) + with + Pre => (if Length (Source) = Max_Length then Drop /= Error), + Post => + Length (Source) + = Natural'Min (Max_Length, Length (Source)'Old + 1), + Global => null; function "&" (Left : Bounded_String; - Right : Bounded_String) return Bounded_String; + Right : Bounded_String) return Bounded_String + with + Pre => Length (Left) <= Max_Length - Length (Right), + Post => Length ("&"'Result) = Length (Left) + Length (Right), + Global => null; function "&" (Left : Bounded_String; - Right : String) return Bounded_String; + Right : String) return Bounded_String + with + Pre => Right'Length <= Max_Length - Length (Left), + Post => Length ("&"'Result) = Length (Left) + Right'Length, + Global => null; function "&" (Left : String; - Right : Bounded_String) return Bounded_String; + Right : Bounded_String) return Bounded_String + with + Pre => Left'Length <= Max_Length - Length (Right), + Post => Length ("&"'Result) = Left'Length + Length (Right), + Global => null; function "&" (Left : Bounded_String; - Right : Character) return Bounded_String; + Right : Character) return Bounded_String + with + Pre => Length (Left) < Max_Length, + Post => Length ("&"'Result) = Length (Left) + 1, + Global => null; function "&" (Left : Character; - Right : Bounded_String) return Bounded_String; + Right : Bounded_String) return Bounded_String + with + Pre => Length (Right) < Max_Length, + Post => Length ("&"'Result) = 1 + Length (Right), + Global => null; function Element (Source : Bounded_String; - Index : Positive) return Character; + Index : Positive) return Character + with + Pre => Index <= Length (Source), + Global => null; procedure Replace_Element (Source : in out Bounded_String; Index : Positive; - By : Character); + By : Character) + with + Pre => Index <= Length (Source), + Post => Length (Source) = Length (Source)'Old, + Global => null; function Slice (Source : Bounded_String; Low : Positive; - High : Natural) return String; + 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; function Bounded_Slice (Source : Bounded_String; Low : Positive; - High : Natural) return Bounded_String; + High : Natural) return Bounded_String + with + Pre => Low - 1 <= Length (Source) and then High <= Length (Source), + Post => + Length (Bounded_Slice'Result) = Natural'Max (0, High - Low + 1), + Global => null; pragma Ada_05 (Bounded_Slice); procedure Bounded_Slice (Source : Bounded_String; Target : out Bounded_String; Low : Positive; - High : Natural); + 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 (Bounded_Slice); function "=" (Left : Bounded_String; - Right : Bounded_String) return Boolean; + Right : Bounded_String) return Boolean + with + Global => null; function "=" (Left : Bounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function "=" (Left : String; - Right : Bounded_String) return Boolean; + Right : Bounded_String) return Boolean + with + Global => null; function "<" (Left : Bounded_String; - Right : Bounded_String) return Boolean; + Right : Bounded_String) return Boolean + with + Global => null; function "<" (Left : Bounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function "<" (Left : String; - Right : Bounded_String) return Boolean; + Right : Bounded_String) return Boolean + with + Global => null; function "<=" (Left : Bounded_String; - Right : Bounded_String) return Boolean; + Right : Bounded_String) return Boolean + with + Global => null; function "<=" (Left : Bounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function "<=" (Left : String; - Right : Bounded_String) return Boolean; + Right : Bounded_String) return Boolean + with + Global => null; function ">" (Left : Bounded_String; - Right : Bounded_String) return Boolean; + Right : Bounded_String) return Boolean + with + Global => null; function ">" (Left : Bounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function ">" (Left : String; - Right : Bounded_String) return Boolean; + Right : Bounded_String) return Boolean + with + Global => null; function ">=" (Left : Bounded_String; - Right : Bounded_String) return Boolean; + Right : Bounded_String) return Boolean + with + Global => null; function ">=" (Left : Bounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function ">=" (Left : String; - Right : Bounded_String) return Boolean; + Right : Bounded_String) return Boolean + with + Global => null; ---------------------- -- Search Functions -- @@ -227,26 +376,40 @@ package Ada.Strings.Bounded is (Source : Bounded_String; Pattern : String; Going : Direction := Forward; - Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; + Mapping : Maps.Character_Mapping := Maps.Identity) return Natural + with + Pre => Pattern'Length /= 0, + Global => null; function Index (Source : Bounded_String; Pattern : String; Going : Direction := Forward; - Mapping : Maps.Character_Mapping_Function) return Natural; + Mapping : Maps.Character_Mapping_Function) return Natural + with + Pre => Pattern'Length /= 0, + Global => null; function Index (Source : Bounded_String; Set : Maps.Character_Set; Test : Membership := Inside; - Going : Direction := Forward) return Natural; + Going : Direction := Forward) return Natural + with + Global => null; function Index (Source : Bounded_String; Pattern : String; From : Positive; Going : Direction := Forward; - Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; + 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 @@ -254,7 +417,13 @@ package Ada.Strings.Bounded is Pattern : String; From : Positive; Going : Direction := Forward; - Mapping : Maps.Character_Mapping_Function) return Natural; + 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 @@ -262,32 +431,48 @@ package Ada.Strings.Bounded is Set : Maps.Character_Set; From : Positive; Test : Membership := Inside; - Going : Direction := Forward) return Natural; + 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 : Bounded_String; - Going : Direction := Forward) return Natural; + Going : Direction := Forward) return Natural + with + Global => null; function Index_Non_Blank (Source : Bounded_String; From : Positive; - Going : Direction := Forward) return Natural; + 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 : Bounded_String; Pattern : String; - Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; + Mapping : Maps.Character_Mapping := Maps.Identity) return Natural + with + Pre => Pattern'Length /= 0, + Global => null; function Count (Source : Bounded_String; Pattern : String; - Mapping : Maps.Character_Mapping_Function) return Natural; + Mapping : Maps.Character_Mapping_Function) return Natural + with + Pre => Pattern'Length /= 0, + Global => null; function Count (Source : Bounded_String; - Set : Maps.Character_Set) return Natural; + Set : Maps.Character_Set) return Natural + with + Global => null; procedure Find_Token (Source : Bounded_String; @@ -295,7 +480,10 @@ package Ada.Strings.Bounded is From : Positive; Test : Membership; First : out Positive; - Last : out Natural); + Last : out Natural) + with + Pre => (if Length (Source) /= 0 then From <= Length (Source)), + Global => null; pragma Ada_2012 (Find_Token); procedure Find_Token @@ -303,7 +491,9 @@ package Ada.Strings.Bounded is Set : Maps.Character_Set; Test : Membership; First : out Positive; - Last : out Natural); + Last : out Natural) + with + Global => null; ------------------------------------ -- String Translation Subprograms -- @@ -311,19 +501,31 @@ package Ada.Strings.Bounded is function Translate (Source : Bounded_String; - Mapping : Maps.Character_Mapping) return Bounded_String; + Mapping : Maps.Character_Mapping) return Bounded_String + with + Post => Length (Translate'Result) = Length (Source), + Global => null; procedure Translate (Source : in out Bounded_String; - Mapping : Maps.Character_Mapping); + Mapping : Maps.Character_Mapping) + with + Post => Length (Source) = Length (Source)'Old, + Global => null; function Translate (Source : Bounded_String; - Mapping : Maps.Character_Mapping_Function) return Bounded_String; + Mapping : Maps.Character_Mapping_Function) return Bounded_String + with + Post => Length (Translate'Result) = Length (Source), + Global => null; procedure Translate (Source : in out Bounded_String; - Mapping : Maps.Character_Mapping_Function); + Mapping : Maps.Character_Mapping_Function) + with + Post => Length (Source) = Length (Source)'Old, + Global => null; --------------------------------------- -- String Transformation Subprograms -- @@ -334,48 +536,149 @@ package Ada.Strings.Bounded is Low : Positive; High : Natural; By : String; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => + Low - 1 <= Length (Source) + and then + (if Drop = Error + then (if High >= Low + then Low - 1 + <= Max_Length - By'Length + - Natural'Max (Length (Source) - High, 0) + else Length (Source) <= Max_Length - By'Length)), + Contract_Cases => + (High >= Low => + Length (Replace_Slice'Result) + = Natural'Min + (Max_Length, + Low - 1 + By'Length + Natural'Max (Length (Source) - High, + 0)), + others => + Length (Replace_Slice'Result) + = Natural'Min (Max_Length, Length (Source) + By'Length)), + Global => null; procedure Replace_Slice (Source : in out Bounded_String; Low : Positive; High : Natural; By : String; - Drop : Truncation := Error); + Drop : Truncation := Error) + with + Pre => + Low - 1 <= Length (Source) + and then + (if Drop = Error + then (if High >= Low + then Low - 1 + <= Max_Length - By'Length + - Natural'Max (Length (Source) - High, 0) + else Length (Source) <= Max_Length - By'Length)), + Contract_Cases => + (High >= Low => + Length (Source) + = Natural'Min + (Max_Length, + Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, + 0)), + others => + Length (Source) + = Natural'Min (Max_Length, Length (Source)'Old + By'Length)), + Global => null; function Insert (Source : Bounded_String; Before : Positive; New_Item : String; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => + Before - 1 <= Length (Source) + and then (if New_Item'Length > Max_Length - Length (Source) + then Drop /= Error), + Post => + Length (Insert'Result) + = Natural'Min (Max_Length, Length (Source) + New_Item'Length), + Global => null; procedure Insert (Source : in out Bounded_String; Before : Positive; New_Item : String; - Drop : Truncation := Error); + Drop : Truncation := Error) + with + Pre => + Before - 1 <= Length (Source) + and then (if New_Item'Length > Max_Length - Length (Source) + then Drop /= Error), + Post => + Length (Source) + = Natural'Min (Max_Length, Length (Source)'Old + New_Item'Length), + Global => null; function Overwrite (Source : Bounded_String; Position : Positive; New_Item : String; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => + Position - 1 <= Length (Source) + and then (if New_Item'Length > Max_Length - (Position - 1) + then Drop /= Error), + Post => + Length (Overwrite'Result) + = Natural'Max + (Length (Source), + Natural'Min (Max_Length, Position - 1 + New_Item'Length)), + Global => null; procedure Overwrite (Source : in out Bounded_String; Position : Positive; New_Item : String; - Drop : Truncation := Error); + Drop : Truncation := Error) + with + Pre => + Position - 1 <= Length (Source) + and then (if New_Item'Length > Max_Length - (Position - 1) + then Drop /= Error), + Post => + Length (Source) + = Natural'Max + (Length (Source)'Old, + Natural'Min (Max_Length, Position - 1 + New_Item'Length)), + Global => null; function Delete (Source : Bounded_String; From : Positive; - Through : Natural) return Bounded_String; + Through : Natural) return Bounded_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 Bounded_String; From : Positive; - Through : Natural); + 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; --------------------------------- -- String Selector Subprograms -- @@ -383,45 +686,73 @@ package Ada.Strings.Bounded is function Trim (Source : Bounded_String; - Side : Trim_End) return Bounded_String; + Side : Trim_End) return Bounded_String + with + Post => Length (Trim'Result) <= Length (Source), + Global => null; procedure Trim (Source : in out Bounded_String; - Side : Trim_End); + Side : Trim_End) + with + Post => Length (Source) <= Length (Source)'Old, + Global => null; function Trim (Source : Bounded_String; Left : Maps.Character_Set; - Right : Maps.Character_Set) return Bounded_String; + Right : Maps.Character_Set) return Bounded_String + with + Post => Length (Trim'Result) <= Length (Source), + Global => null; procedure Trim (Source : in out Bounded_String; Left : Maps.Character_Set; - Right : Maps.Character_Set); + Right : Maps.Character_Set) + with + Post => Length (Source) <= Length (Source)'Old, + Global => null; function Head (Source : Bounded_String; Count : Natural; Pad : Character := Space; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => (if Count > Max_Length then Drop /= Error), + Post => Length (Head'Result) = Natural'Min (Max_Length, Count), + Global => null; procedure Head (Source : in out Bounded_String; Count : Natural; Pad : Character := Space; - Drop : Truncation := Error); + Drop : Truncation := Error) + with + Pre => (if Count > Max_Length then Drop /= Error), + Post => Length (Source) = Natural'Min (Max_Length, Count), + Global => null; function Tail (Source : Bounded_String; Count : Natural; Pad : Character := Space; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => (if Count > Max_Length then Drop /= Error), + Post => Length (Tail'Result) = Natural'Min (Max_Length, Count), + Global => null; procedure Tail (Source : in out Bounded_String; Count : Natural; Pad : Character := Space; - Drop : Truncation := Error); + Drop : Truncation := Error) + with + Pre => (if Count > Max_Length then Drop /= Error), + Post => Length (Source) = Natural'Min (Max_Length, Count), + Global => null; ------------------------------------ -- String Constructor Subprograms -- @@ -429,30 +760,66 @@ package Ada.Strings.Bounded is function "*" (Left : Natural; - Right : Character) return Bounded_String; + Right : Character) return Bounded_String + with + Pre => Left <= Max_Length, + Post => Length ("*"'Result) = Left, + Global => null; function "*" (Left : Natural; - Right : String) return Bounded_String; + Right : String) return Bounded_String + with + Pre => (if Left /= 0 then Right'Length <= Max_Length / Left), + Post => Length ("*"'Result) = Left * Right'Length, + Global => null; function "*" (Left : Natural; - Right : Bounded_String) return Bounded_String; + Right : Bounded_String) return Bounded_String + with + Pre => (if Left /= 0 then Length (Right) <= Max_Length / Left), + Post => Length ("*"'Result) = Left * Length (Right), + Global => null; function Replicate (Count : Natural; Item : Character; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => (if Count > Max_Length then Drop /= Error), + Post => + Length (Replicate'Result) + = Natural'Min (Max_Length, Count), + Global => null; function Replicate (Count : Natural; Item : String; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => + (if Item'Length /= 0 + and then Count > Max_Length / Item'Length + then Drop /= Error), + Post => + Length (Replicate'Result) + = Natural'Min (Max_Length, Count * Item'Length), + Global => null; function Replicate (Count : Natural; Item : Bounded_String; - Drop : Truncation := Error) return Bounded_String; + Drop : Truncation := Error) return Bounded_String + with + Pre => + (if Length (Item) /= 0 + and then Count > Max_Length / Length (Item) + then Drop /= Error), + Post => + Length (Replicate'Result) + = Natural'Min (Max_Length, Count * Length (Item)), + Global => null; private -- Most of the implementation is in the separate non generic package diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads index 157186104d2..7d6e121c534 100644 --- a/gcc/ada/libgnat/a-strfix.ads +++ b/gcc/ada/libgnat/a-strfix.ads @@ -13,6 +13,12 @@ -- -- ------------------------------------------------------------------------------ +-- 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; -- The language-defined package Strings.Fixed provides string-handling @@ -34,7 +40,7 @@ with Ada.Strings.Maps; -- these effects. Similar control is provided by the string transformation -- procedures. -package Ada.Strings.Fixed is +package Ada.Strings.Fixed with SPARK_Mode is pragma Preelaborate; -------------------------------------------------------------- @@ -46,7 +52,12 @@ package Ada.Strings.Fixed is Target : out String; Drop : Truncation := Error; Justify : Alignment := Left; - Pad : Character := Space); + Pad : Character := Space) + with + + -- Incomplete contract + + Global => null; -- The Move procedure copies characters from Source to Target. If Source -- has the same length as Target, then the effect is to assign Source to -- Target. If Source is shorter than Target then: @@ -95,7 +106,12 @@ package Ada.Strings.Fixed is Pattern : String; From : Positive; Going : Direction := Forward; - Mapping : Maps.Character_Mapping_Function) return Natural; + Mapping : Maps.Character_Mapping_Function) return Natural + with + Pre => + Pattern'Length /= 0 + and then (if Source'Length /= 0 then From in Source'Range), + Global => null; pragma Ada_05 (Index); function Index @@ -103,7 +119,12 @@ package Ada.Strings.Fixed is Pattern : String; From : Positive; Going : Direction := Forward; - Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; + Mapping : Maps.Character_Mapping := Maps.Identity) return Natural + with + Pre => + Pattern'Length /= 0 + and then (if Source'Length /= 0 then From in Source'Range), + Global => null; pragma Ada_05 (Index); -- Each Index function searches, starting from From, for a slice of @@ -123,13 +144,19 @@ package Ada.Strings.Fixed is (Source : String; Pattern : String; Going : Direction := Forward; - Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; + Mapping : Maps.Character_Mapping := Maps.Identity) return Natural + with + Pre => Pattern'Length > 0, + Global => null; function Index (Source : String; Pattern : String; Going : Direction := Forward; - Mapping : Maps.Character_Mapping_Function) return Natural; + Mapping : Maps.Character_Mapping_Function) return Natural + with + Pre => Pattern'Length /= 0, + Global => null; -- If Going = Forward, returns: -- @@ -143,14 +170,19 @@ package Ada.Strings.Fixed is (Source : String; Set : Maps.Character_Set; Test : Membership := Inside; - Going : Direction := Forward) return Natural; + Going : Direction := Forward) return Natural + with + Global => null; function Index (Source : String; Set : Maps.Character_Set; From : Positive; Test : Membership := Inside; - Going : Direction := Forward) return Natural; + Going : Direction := Forward) return Natural + with + Pre => (if Source'Length /= 0 then From in Source'Range), + Global => null; pragma Ada_05 (Index); -- Index searches for the first or last occurrence of any of a set of -- characters (when Test=Inside), or any of the complement of a set of @@ -164,24 +196,35 @@ package Ada.Strings.Fixed is function Index_Non_Blank (Source : String; From : Positive; - Going : Direction := Forward) return Natural; + Going : Direction := Forward) return Natural + with + Pre => (if Source'Length /= 0 then From in Source'Range), + Global => null; pragma Ada_05 (Index_Non_Blank); -- Returns Index (Source, Maps.To_Set(Space), From, Outside, Going) function Index_Non_Blank (Source : String; - Going : Direction := Forward) return Natural; + Going : Direction := Forward) return Natural + with + Global => null; -- Returns Index (Source, Maps.To_Set(Space), Outside, Going) function Count (Source : String; Pattern : String; - Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; + Mapping : Maps.Character_Mapping := Maps.Identity) return Natural + with + Pre => Pattern'Length /= 0, + Global => null; function Count (Source : String; Pattern : String; - Mapping : Maps.Character_Mapping_Function) return Natural; + Mapping : Maps.Character_Mapping_Function) return Natural + with + Pre => Pattern'Length /= 0, + Global => null; -- Returns the maximum number of nonoverlapping slices of Source that match -- Pattern with respect to Mapping. If Pattern is the null string then @@ -189,7 +232,9 @@ package Ada.Strings.Fixed is function Count (Source : String; - Set : Maps.Character_Set) return Natural; + Set : Maps.Character_Set) return Natural + with + Global => null; -- Returns the number of occurrences in Source of characters that are in -- Set. @@ -199,7 +244,10 @@ package Ada.Strings.Fixed is From : Positive; Test : Membership; First : out Positive; - Last : out Natural); + Last : out Natural) + with + Pre => (if Source'Length /= 0 then From in Source'Range), + Global => null; pragma Ada_2012 (Find_Token); -- If Source is not the null string and From is not in Source'Range, then -- Index_Error is raised. Otherwise, First is set to the index of the first @@ -214,7 +262,9 @@ package Ada.Strings.Fixed is Set : Maps.Character_Set; Test : Membership; First : out Positive; - Last : out Natural); + Last : out Natural) + with + Global => null; -- Equivalent to Find_Token (Source, Set, Source'First, Test, First, Last) ------------------------------------ @@ -223,11 +273,17 @@ package Ada.Strings.Fixed is function Translate (Source : String; - Mapping : Maps.Character_Mapping_Function) return String; + Mapping : Maps.Character_Mapping_Function) return String + with + Post => Translate'Result'Length = Source'Length, + Global => null; function Translate (Source : String; - Mapping : Maps.Character_Mapping) return String; + Mapping : Maps.Character_Mapping) return String + with + Post => Translate'Result'Length = Source'Length, + Global => null; -- Returns the string S whose length is Source'Length and such that S (I) -- is the character to which Mapping maps the corresponding element of @@ -235,11 +291,15 @@ package Ada.Strings.Fixed is procedure Translate (Source : in out String; - Mapping : Maps.Character_Mapping_Function); + Mapping : Maps.Character_Mapping_Function) + with + Global => null; procedure Translate (Source : in out String; - Mapping : Maps.Character_Mapping); + Mapping : Maps.Character_Mapping) + with + Global => null; -- Equivalent to Source := Translate(Source, Mapping) @@ -254,7 +314,15 @@ package Ada.Strings.Fixed is By : String; Drop : Truncation := Error; Justify : Alignment := Left; - Pad : Character := Space); + Pad : Character := Space) + with + Pre => + + -- Incomplete contract + + Low - 1 <= Source'Last + and then High >= Source'First - 1, + Global => null; -- If Low > Source'Last+1, or High < Source'First - 1, then Index_Error is -- propagated. Otherwise: -- @@ -269,7 +337,25 @@ package Ada.Strings.Fixed is (Source : String; Low : Positive; High : Natural; - By : String) return String; + By : String) return String + with + Pre => + Low - 1 <= Source'Last + and then High >= Source'First - 1 + and then (if High >= Low + then Natural'Max (0, Low - Source'First) + <= Natural'Last - By'Length + - Natural'Max (Source'Last - High, 0) + else Source'Length <= Natural'Last - By'Length), + Contract_Cases => + (High >= Low => + Replace_Slice'Result'Length + = Natural'Max (0, Low - Source'First) + + By'Length + + Natural'Max (Source'Last - High, 0), + others => + Replace_Slice'Result'Length = Source'Length + By'Length), + Global => null; -- Equivalent to: -- -- Move (Replace_Slice (Source, Low, High, By), @@ -278,7 +364,13 @@ package Ada.Strings.Fixed is function Insert (Source : String; Before : Positive; - New_Item : String) return String; + New_Item : String) return String + with + Pre => + Before - 1 in Source'First - 1 .. Source'Last + and then Source'Length <= Natural'Last - New_Item'Length, + Post => Insert'Result'Length = Source'Length + New_Item'Length, + Global => null; -- Propagates Index_Error if Before is not in -- Source'First .. Source'Last+1; otherwise, returns -- Source (Source'First .. Before - 1) @@ -288,13 +380,30 @@ package Ada.Strings.Fixed is (Source : in out String; Before : Positive; New_Item : String; - Drop : Truncation := Error); + Drop : Truncation := Error) + with + Pre => Before - 1 in Source'First - 1 .. Source'Last, + + -- Incomplete contract + + Global => null; -- Equivalent to Move (Insert (Source, Before, New_Item), Source, Drop) function Overwrite (Source : String; Position : Positive; - New_Item : String) return String; + New_Item : String) return String + with + Pre => + Position - 1 in Source'First - 1 .. Source'Last + and then + (if Position - Source'First >= Source'Length - New_Item'Length + then Position - Source'First <= Natural'Last - New_Item'Length), + Post => + Overwrite'Result'Length + = Integer'Max (Source'Length, + Position - Source'First + New_Item'Length), + Global => null; -- Propagates Index_Error if Position is not in -- Source'First .. Source'Last + 1; otherwise, returns the string obtained -- from Source by consecutively replacing characters starting at Position @@ -306,13 +415,29 @@ package Ada.Strings.Fixed is (Source : in out String; Position : Positive; New_Item : String; - Drop : Truncation := Right); + Drop : Truncation := Right) + with + Pre => Position - 1 in Source'First - 1 .. Source'Last, + + -- Incomplete contract + + Global => null; -- Equivalent to Move(Overwrite(Source, Position, New_Item), Source, Drop) function Delete (Source : String; From : Positive; - Through : Natural) return String; + Through : Natural) return String + with + Pre => (if From <= Through + then (From in Source'Range + and then Through <= Source'Last)), + Post => + Delete'Result'Length + = Source'Length - (if From <= Through + then Through - From + 1 + else 0), + Global => null; -- If From <= Through, the returned string is -- Replace_Slice(Source, From, Through, ""); otherwise, it is Source with -- lower bound 1. @@ -322,7 +447,15 @@ package Ada.Strings.Fixed is From : Positive; Through : Natural; Justify : Alignment := Left; - Pad : Character := Space); + Pad : Character := Space) + with + Pre => (if From <= Through + then (From in Source'Range + and then Through <= Source'Last)), + + -- Incomplete contract + + Global => null; -- Equivalent to: -- -- Move (Delete (Source, From, Through), @@ -334,7 +467,10 @@ package Ada.Strings.Fixed is function Trim (Source : String; - Side : Trim_End) return String; + Side : Trim_End) return String + with + Post => Trim'Result'Length <= Source'Length, + Global => null; -- Returns the string obtained by removing from Source all leading Space -- characters (if Side = Left), all trailing Space characters (if -- Side = Right), or all leading and trailing Space characters (if @@ -344,7 +480,12 @@ package Ada.Strings.Fixed is (Source : in out String; Side : Trim_End; Justify : Alignment := Left; - Pad : Character := Space); + Pad : Character := Space) + with + + -- Incomplete contract + + Global => null; -- Equivalent to: -- -- Move (Trim (Source, Side), Source, Justify=>Justify, Pad=>Pad). @@ -352,7 +493,10 @@ package Ada.Strings.Fixed is function Trim (Source : String; Left : Maps.Character_Set; - Right : Maps.Character_Set) return String; + Right : Maps.Character_Set) return String + with + Post => Trim'Result'Length <= Source'Length, + Global => null; -- Returns the string obtained by removing from Source all leading -- characters in Left and all trailing characters in Right. @@ -361,7 +505,12 @@ package Ada.Strings.Fixed is Left : Maps.Character_Set; Right : Maps.Character_Set; Justify : Alignment := Strings.Left; - Pad : Character := Space); + Pad : Character := Space) + with + + -- Incomplete contract + + Global => null; -- Equivalent to: -- -- Move (Trim (Source, Left, Right), @@ -370,7 +519,10 @@ package Ada.Strings.Fixed is function Head (Source : String; Count : Natural; - Pad : Character := Space) return String; + Pad : Character := Space) return String + with + Post => Head'Result'Length = Count, + Global => null; -- Returns a string of length Count. If Count <= Source'Length, the string -- comprises the first Count characters of Source. Otherwise, its contents -- are Source concatenated with Count - Source'Length Pad characters. @@ -379,7 +531,12 @@ package Ada.Strings.Fixed is (Source : in out String; Count : Natural; Justify : Alignment := Left; - Pad : Character := Space); + Pad : Character := Space) + with + + -- Incomplete contract + + Global => null; -- Equivalent to: -- -- Move (Head (Source, Count, Pad), @@ -388,7 +545,10 @@ package Ada.Strings.Fixed is function Tail (Source : String; Count : Natural; - Pad : Character := Space) return String; + Pad : Character := Space) return String + with + Post => Tail'Result'Length = Count, + Global => null; -- Returns a string of length Count. If Count <= Source'Length, the string -- comprises the last Count characters of Source. Otherwise, its contents -- are Count-Source'Length Pad characters concatenated with Source. @@ -397,7 +557,12 @@ package Ada.Strings.Fixed is (Source : in out String; Count : Natural; Justify : Alignment := Left; - Pad : Character := Space); + Pad : Character := Space) + with + + -- Incomplete contract + + Global => null; -- Equivalent to: -- -- Move (Tail (Source, Count, Pad), @@ -409,11 +574,18 @@ package Ada.Strings.Fixed is function "*" (Left : Natural; - Right : Character) return String; + Right : Character) return String + with + Post => "*"'Result'Length = Left, + Global => null; function "*" (Left : Natural; - Right : String) return String; + Right : String) return String + with + Pre => (if Right'Length /= 0 then Left <= Natural'Last / Right'Length), + Post => "*"'Result'Length = Left * Right'Length, + Global => null; -- These functions replicate a character or string a specified number of -- times. The first function returns a string whose length is Left and each diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads index c0caf10bb72..e875b5b90c8 100644 --- a/gcc/ada/libgnat/a-strunb.ads +++ b/gcc/ada/libgnat/a-strunb.ads @@ -33,6 +33,12 @@ -- -- ------------------------------------------------------------------------------ +-- 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; @@ -45,7 +51,9 @@ with Ada.Finalization; -- length. Since the Unbounded_String type is private, relevant constructor -- and selector operations are provided. -package Ada.Strings.Unbounded is +package Ada.Strings.Unbounded with + Initial_Condition => Length (Null_Unbounded_String) = 0 +is pragma Preelaborate; type Unbounded_String is private; @@ -56,7 +64,8 @@ package Ada.Strings.Unbounded is -- otherwise initialized, it will be initialized to the same value as -- Null_Unbounded_String. - function Length (Source : Unbounded_String) return Natural; + 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; @@ -71,15 +80,25 @@ package Ada.Strings.Unbounded is -------------------------------------------------------- function To_Unbounded_String - (Source : String) return 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; + (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; + 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: @@ -91,21 +110,35 @@ package Ada.Strings.Unbounded is procedure Set_Unbounded_String (Target : out Unbounded_String; - Source : 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); + 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); + 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); + 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 @@ -113,23 +146,43 @@ package Ada.Strings.Unbounded is function "&" (Left : Unbounded_String; - Right : Unbounded_String) return 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; + 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; + 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; + 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; + 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 @@ -139,14 +192,21 @@ package Ada.Strings.Unbounded is function Element (Source : Unbounded_String; - Index : Positive) return Character; + 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); + 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). @@ -154,7 +214,11 @@ package Ada.Strings.Unbounded is function Slice (Source : Unbounded_String; Low : Positive; - High : Natural) return String; + 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 @@ -163,7 +227,12 @@ package Ada.Strings.Unbounded is function Unbounded_Slice (Source : Unbounded_String; Low : Positive; - High : Natural) return Unbounded_String; + 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 @@ -173,7 +242,11 @@ package Ada.Strings.Unbounded is (Source : Unbounded_String; Target : out Unbounded_String; Low : Positive; - High : Natural); + 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 @@ -181,63 +254,93 @@ package Ada.Strings.Unbounded is function "=" (Left : Unbounded_String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function "=" (Left : Unbounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function "=" (Left : String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function "<" (Left : Unbounded_String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function "<" (Left : Unbounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function "<" (Left : String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function "<=" (Left : Unbounded_String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function "<=" (Left : Unbounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function "<=" (Left : String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function ">" (Left : Unbounded_String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function ">" (Left : Unbounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function ">" (Left : String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function ">=" (Left : Unbounded_String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function ">=" (Left : Unbounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function ">=" (Left : String; - Right : Unbounded_String) return Boolean; + 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 @@ -251,26 +354,38 @@ package Ada.Strings.Unbounded is (Source : Unbounded_String; Pattern : String; Going : Direction := Forward; - Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; + 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; + 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; + 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; + 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 @@ -278,7 +393,11 @@ package Ada.Strings.Unbounded is Pattern : String; From : Positive; Going : Direction := Forward; - Mapping : Maps.Character_Mapping_Function) return Natural; + 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 @@ -286,32 +405,48 @@ package Ada.Strings.Unbounded is Set : Maps.Character_Set; From : Positive; Test : Membership := Inside; - Going : Direction := Forward) return Natural; + 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; + Going : Direction := Forward) return Natural + with + Global => null; function Index_Non_Blank (Source : Unbounded_String; From : Positive; - Going : Direction := Forward) return Natural; + 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; + 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; + 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; + Set : Maps.Character_Set) return Natural + with + Global => null; procedure Find_Token (Source : Unbounded_String; @@ -319,7 +454,10 @@ package Ada.Strings.Unbounded is From : Positive; Test : Membership; First : out Positive; - Last : out Natural); + Last : out Natural) + with + Pre => (if Length (Source) /= 0 then From <= Length (Source)), + Global => null; pragma Ada_2012 (Find_Token); procedure Find_Token @@ -327,7 +465,9 @@ package Ada.Strings.Unbounded is Set : Maps.Character_Set; Test : Membership; First : out Positive; - Last : out Natural); + 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 @@ -340,19 +480,31 @@ package Ada.Strings.Unbounded is function Translate (Source : Unbounded_String; - Mapping : Maps.Character_Mapping) return 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); + 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; + 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); + 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 @@ -367,93 +519,204 @@ package Ada.Strings.Unbounded is (Source : Unbounded_String; Low : Positive; High : Natural; - By : String) return Unbounded_String; + 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); + 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; + 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); + 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; + 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); + 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; + 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); + 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; + 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); + 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; + 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); + 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; + 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); + Pad : Character := Space) + with + Post => Length (Source) = Count, + Global => null; function Tail (Source : Unbounded_String; Count : Natural; - Pad : Character := Space) return Unbounded_String; + 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); + Pad : Character := Space) + with + Post => Length (Source) = Count, + Global => null; function "*" (Left : Natural; - Right : Character) return Unbounded_String; + Right : Character) return Unbounded_String + with + Pre => Left <= Natural'Last, + Post => Length ("*"'Result) = Left, + Global => null; function "*" (Left : Natural; - Right : String) return Unbounded_String; + 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; + 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 diff --git a/gcc/ada/libgnat/a-strunb__shared.ads b/gcc/ada/libgnat/a-strunb__shared.ads index 385a9e62040..17acd56e491 100644 --- a/gcc/ada/libgnat/a-strunb__shared.ads +++ b/gcc/ada/libgnat/a-strunb__shared.ads @@ -33,6 +33,12 @@ -- -- ------------------------------------------------------------------------------ +-- 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); + -- This package provides an implementation of Ada.Strings.Unbounded that uses -- reference counts to implement copy on modification (rather than copy on -- assignment). This is significantly more efficient on many targets. @@ -73,7 +79,9 @@ with Ada.Strings.Maps; private with Ada.Finalization; private with System.Atomic_Counters; -package Ada.Strings.Unbounded is +package Ada.Strings.Unbounded with + Initial_Condition => Length (Null_Unbounded_String) = 0 +is pragma Preelaborate; type Unbounded_String is private; @@ -81,7 +89,8 @@ package Ada.Strings.Unbounded is Null_Unbounded_String : constant Unbounded_String; - function Length (Source : Unbounded_String) return Natural; + function Length (Source : Unbounded_String) return Natural with + Global => null; type String_Access is access all String; @@ -92,136 +101,229 @@ package Ada.Strings.Unbounded is -------------------------------------------------------- function To_Unbounded_String - (Source : String) return Unbounded_String; + (Source : String) return Unbounded_String + with + Post => Length (To_Unbounded_String'Result) = Source'Length, + Global => null; function To_Unbounded_String - (Length : Natural) return Unbounded_String; + (Length : Natural) return Unbounded_String + with + Post => + Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length, + Global => null; - function To_String (Source : Unbounded_String) return String; + function To_String (Source : Unbounded_String) return String with + Post => To_String'Result'Length = Length (Source), + Global => null; procedure Set_Unbounded_String (Target : out Unbounded_String; - Source : String); + Source : String) + with + Global => null; pragma Ada_05 (Set_Unbounded_String); procedure Append (Source : in out Unbounded_String; - New_Item : 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); + 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); + New_Item : Character) + with + Pre => Length (Source) < Natural'Last, + Post => Length (Source) = Length (Source)'Old + 1, + Global => null; function "&" (Left : Unbounded_String; - Right : Unbounded_String) return 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; + 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; + 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; + 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; + Right : Unbounded_String) return Unbounded_String + with + Pre => Length (Right) < Natural'Last, + Post => Length ("&"'Result) = Length (Right) + 1, + Global => null; function Element (Source : Unbounded_String; - Index : Positive) return Character; + Index : Positive) return Character + with + Pre => Index <= Length (Source), + Global => null; procedure Replace_Element (Source : in out Unbounded_String; Index : Positive; - By : Character); + By : Character) + with + Pre => Index <= Length (Source), + Post => Length (Source) = Length (Source)'Old, + Global => null; function Slice (Source : Unbounded_String; Low : Positive; - High : Natural) return String; + 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; function Unbounded_Slice (Source : Unbounded_String; Low : Positive; - High : Natural) return Unbounded_String; + 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); procedure Unbounded_Slice (Source : Unbounded_String; Target : out Unbounded_String; Low : Positive; - High : Natural); + 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); function "=" (Left : Unbounded_String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function "=" (Left : Unbounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function "=" (Left : String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function "<" (Left : Unbounded_String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function "<" (Left : Unbounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function "<" (Left : String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function "<=" (Left : Unbounded_String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function "<=" (Left : Unbounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function "<=" (Left : String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function ">" (Left : Unbounded_String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function ">" (Left : Unbounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function ">" (Left : String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function ">=" (Left : Unbounded_String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; function ">=" (Left : Unbounded_String; - Right : String) return Boolean; + Right : String) return Boolean + with + Global => null; function ">=" (Left : String; - Right : Unbounded_String) return Boolean; + Right : Unbounded_String) return Boolean + with + Global => null; ------------------------ -- Search Subprograms -- @@ -231,26 +333,39 @@ package Ada.Strings.Unbounded is (Source : Unbounded_String; Pattern : String; Going : Direction := Forward; - Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; + 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; + 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; + 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; + 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 @@ -258,7 +373,13 @@ package Ada.Strings.Unbounded is Pattern : String; From : Positive; Going : Direction := Forward; - Mapping : Maps.Character_Mapping_Function) return Natural; + 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 @@ -266,32 +387,48 @@ package Ada.Strings.Unbounded is Set : Maps.Character_Set; From : Positive; Test : Membership := Inside; - Going : Direction := Forward) return Natural; + 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; + Going : Direction := Forward) return Natural + with + Global => null; function Index_Non_Blank (Source : Unbounded_String; From : Positive; - Going : Direction := Forward) return Natural; + 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; + 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; + 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; + Set : Maps.Character_Set) return Natural + with + Global => null; procedure Find_Token (Source : Unbounded_String; @@ -299,7 +436,10 @@ package Ada.Strings.Unbounded is From : Positive; Test : Membership; First : out Positive; - Last : out Natural); + Last : out Natural) + with + Pre => (if Length (Source) /= 0 then From <= Length (Source)), + Global => null; pragma Ada_2012 (Find_Token); procedure Find_Token @@ -307,7 +447,9 @@ package Ada.Strings.Unbounded is Set : Maps.Character_Set; Test : Membership; First : out Positive; - Last : out Natural); + Last : out Natural) + with + Global => null; ------------------------------------ -- String Translation Subprograms -- @@ -315,19 +457,31 @@ package Ada.Strings.Unbounded is function Translate (Source : Unbounded_String; - Mapping : Maps.Character_Mapping) return 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); + 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; + 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); + Mapping : Maps.Character_Mapping_Function) + with + Post => Length (Source) = Length (Source)'Old, + Global => null; --------------------------------------- -- String Transformation Subprograms -- @@ -337,93 +491,204 @@ package Ada.Strings.Unbounded is (Source : Unbounded_String; Low : Positive; High : Natural; - By : String) return Unbounded_String; + 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); + 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; + 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); + 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; + 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); + 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; + 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); + 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; + 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); + 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; + 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); + 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; + 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); + Pad : Character := Space) + with + Post => Length (Source) = Count, + Global => null; function Tail (Source : Unbounded_String; Count : Natural; - Pad : Character := Space) return Unbounded_String; + 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); + Pad : Character := Space) + with + Post => Length (Source) = Count, + Global => null; function "*" (Left : Natural; - Right : Character) return Unbounded_String; + Right : Character) return Unbounded_String + with + Pre => Left <= Natural'Last, + Post => Length ("*"'Result) = Left, + Global => null; function "*" (Left : Natural; - Right : String) return Unbounded_String; + 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; + 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; private pragma Inline (Length); -- 2.30.2