Skip to content

R
riscv-gcc-1
Commit 0b6694b4 by Joffrey Huguet Committed by Pierre-Marie de Rodat
Options

[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  <huguet@adacore.com>

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
parent ef8a3d9e
Showing with 1328 additions and 254 deletions
gcc/ada/ChangeLog
2019-07-10 Joffrey Huguet <huguet@adacore.com>
* 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 <rupp@adacore.com> 2019-07-10 Doug Rupp <rupp@adacore.com>
* sysdep.c (__gnat_is_file_not_found_error): Reformulate to also * sysdep.c (__gnat_is_file_not_found_error): Reformulate to also
......
gcc/ada/libgnat/a-strbou.ads
...@@ -33,6 +33,12 @@ ...@@ -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.Maps;
with Ada.Strings.Superbounded; with Ada.Strings.Superbounded;
...@@ -43,7 +49,9 @@ package Ada.Strings.Bounded is ...@@ -43,7 +49,9 @@ package Ada.Strings.Bounded is
Max : Positive; Max : Positive;
-- Maximum length of a Bounded_String -- 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; Max_Length : constant Positive := Max;
...@@ -54,7 +62,8 @@ package Ada.Strings.Bounded is ...@@ -54,7 +62,8 @@ package Ada.Strings.Bounded is
subtype Length_Range is Natural range 0 .. Max_Length; 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 -- -- Conversion, Concatenation, and Selection Functions --
...@@ -62,162 +71,302 @@ package Ada.Strings.Bounded is ...@@ -62,162 +71,302 @@ package Ada.Strings.Bounded is
function To_Bounded_String function To_Bounded_String
(Source : 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 procedure Set_Bounded_String
(Target : out Bounded_String; (Target : out Bounded_String;
Source : 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); pragma Ada_05 (Set_Bounded_String);
function Append function Append
(Left : Bounded_String; (Left : Bounded_String;
Right : 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 function Append
(Left : Bounded_String; (Left : Bounded_String;
Right : 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 function Append
(Left : String; (Left : String;
Right : Bounded_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 function Append
(Left : Bounded_String; (Left : Bounded_String;
Right : Character; 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 function Append
(Left : Character; (Left : Character;
Right : Bounded_String; 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 procedure Append
(Source : in out Bounded_String; (Source : in out Bounded_String;
New_Item : 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 procedure Append
(Source : in out Bounded_String; (Source : in out Bounded_String;
New_Item : 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 procedure Append
(Source : in out Bounded_String; (Source : in out Bounded_String;
New_Item : Character; 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 "&" function "&"
(Left : Bounded_String; (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 "&" function "&"
(Left : Bounded_String; (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 "&" function "&"
(Left : String; (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 "&" function "&"
(Left : Bounded_String; (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 "&" function "&"
(Left : Character; (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 function Element
(Source : Bounded_String; (Source : Bounded_String;
Index : Positive) return Character; Index : Positive) return Character
with
Pre => Index <= Length (Source),
Global => null;
procedure Replace_Element procedure Replace_Element
(Source : in out Bounded_String; (Source : in out Bounded_String;
Index : Positive; Index : Positive;
By : Character); By : Character)
with
Pre => Index <= Length (Source),
Post => Length (Source) = Length (Source)'Old,
Global => null;
function Slice function Slice
(Source : Bounded_String; (Source : Bounded_String;
Low : Positive; 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 function Bounded_Slice
(Source : Bounded_String; (Source : Bounded_String;
Low : Positive; 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); pragma Ada_05 (Bounded_Slice);
procedure Bounded_Slice procedure Bounded_Slice
(Source : Bounded_String; (Source : Bounded_String;
Target : out Bounded_String; Target : out Bounded_String;
Low : Positive; 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); pragma Ada_05 (Bounded_Slice);
function "=" function "="
(Left : Bounded_String; (Left : Bounded_String;
Right : Bounded_String) return Boolean; Right : Bounded_String) return Boolean
with
Global => null;
function "=" function "="
(Left : Bounded_String; (Left : Bounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function "=" function "="
(Left : String; (Left : String;
Right : Bounded_String) return Boolean; Right : Bounded_String) return Boolean
with
Global => null;
function "<" function "<"
(Left : Bounded_String; (Left : Bounded_String;
Right : Bounded_String) return Boolean; Right : Bounded_String) return Boolean
with
Global => null;
function "<" function "<"
(Left : Bounded_String; (Left : Bounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function "<" function "<"
(Left : String; (Left : String;
Right : Bounded_String) return Boolean; Right : Bounded_String) return Boolean
with
Global => null;
function "<=" function "<="
(Left : Bounded_String; (Left : Bounded_String;
Right : Bounded_String) return Boolean; Right : Bounded_String) return Boolean
with
Global => null;
function "<=" function "<="
(Left : Bounded_String; (Left : Bounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function "<=" function "<="
(Left : String; (Left : String;
Right : Bounded_String) return Boolean; Right : Bounded_String) return Boolean
with
Global => null;
function ">" function ">"
(Left : Bounded_String; (Left : Bounded_String;
Right : Bounded_String) return Boolean; Right : Bounded_String) return Boolean
with
Global => null;
function ">" function ">"
(Left : Bounded_String; (Left : Bounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function ">" function ">"
(Left : String; (Left : String;
Right : Bounded_String) return Boolean; Right : Bounded_String) return Boolean
with
Global => null;
function ">=" function ">="
(Left : Bounded_String; (Left : Bounded_String;
Right : Bounded_String) return Boolean; Right : Bounded_String) return Boolean
with
Global => null;
function ">=" function ">="
(Left : Bounded_String; (Left : Bounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function ">=" function ">="
(Left : String; (Left : String;
Right : Bounded_String) return Boolean; Right : Bounded_String) return Boolean
with
Global => null;
---------------------- ----------------------
-- Search Functions -- -- Search Functions --
...@@ -227,26 +376,40 @@ package Ada.Strings.Bounded is ...@@ -227,26 +376,40 @@ package Ada.Strings.Bounded is
(Source : Bounded_String; (Source : Bounded_String;
Pattern : String; Pattern : String;
Going : Direction := Forward; 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 function Index
(Source : Bounded_String; (Source : Bounded_String;
Pattern : String; Pattern : String;
Going : Direction := Forward; 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 function Index
(Source : Bounded_String; (Source : Bounded_String;
Set : Maps.Character_Set; Set : Maps.Character_Set;
Test : Membership := Inside; Test : Membership := Inside;
Going : Direction := Forward) return Natural; Going : Direction := Forward) return Natural
with
Global => null;
function Index function Index
(Source : Bounded_String; (Source : Bounded_String;
Pattern : String; Pattern : String;
From : Positive; From : Positive;
Going : Direction := Forward; 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); pragma Ada_05 (Index);
function Index function Index
...@@ -254,7 +417,13 @@ package Ada.Strings.Bounded is ...@@ -254,7 +417,13 @@ package Ada.Strings.Bounded is
Pattern : String; Pattern : String;
From : Positive; From : Positive;
Going : Direction := Forward; 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); pragma Ada_05 (Index);
function Index function Index
...@@ -262,32 +431,48 @@ package Ada.Strings.Bounded is ...@@ -262,32 +431,48 @@ package Ada.Strings.Bounded is
Set : Maps.Character_Set; Set : Maps.Character_Set;
From : Positive; From : Positive;
Test : Membership := Inside; 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); pragma Ada_05 (Index);
function Index_Non_Blank function Index_Non_Blank
(Source : Bounded_String; (Source : Bounded_String;
Going : Direction := Forward) return Natural; Going : Direction := Forward) return Natural
with
Global => null;
function Index_Non_Blank function Index_Non_Blank
(Source : Bounded_String; (Source : Bounded_String;
From : Positive; 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); pragma Ada_05 (Index_Non_Blank);
function Count function Count
(Source : Bounded_String; (Source : Bounded_String;
Pattern : 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 function Count
(Source : Bounded_String; (Source : Bounded_String;
Pattern : 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 function Count
(Source : Bounded_String; (Source : Bounded_String;
Set : Maps.Character_Set) return Natural; Set : Maps.Character_Set) return Natural
with
Global => null;
procedure Find_Token procedure Find_Token
(Source : Bounded_String; (Source : Bounded_String;
...@@ -295,7 +480,10 @@ package Ada.Strings.Bounded is ...@@ -295,7 +480,10 @@ package Ada.Strings.Bounded is
From : Positive; From : Positive;
Test : Membership; Test : Membership;
First : out Positive; 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); pragma Ada_2012 (Find_Token);
procedure Find_Token procedure Find_Token
...@@ -303,7 +491,9 @@ package Ada.Strings.Bounded is ...@@ -303,7 +491,9 @@ package Ada.Strings.Bounded is
Set : Maps.Character_Set; Set : Maps.Character_Set;
Test : Membership; Test : Membership;
First : out Positive; First : out Positive;
Last : out Natural); Last : out Natural)
with
Global => null;
------------------------------------ ------------------------------------
-- String Translation Subprograms -- -- String Translation Subprograms --
...@@ -311,19 +501,31 @@ package Ada.Strings.Bounded is ...@@ -311,19 +501,31 @@ package Ada.Strings.Bounded is
function Translate function Translate
(Source : Bounded_String; (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 procedure Translate
(Source : in out Bounded_String; (Source : in out Bounded_String;
Mapping : Maps.Character_Mapping); Mapping : Maps.Character_Mapping)
with
Post => Length (Source) = Length (Source)'Old,
Global => null;
function Translate function Translate
(Source : Bounded_String; (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 procedure Translate
(Source : in out Bounded_String; (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 -- -- String Transformation Subprograms --
...@@ -334,48 +536,149 @@ package Ada.Strings.Bounded is ...@@ -334,48 +536,149 @@ package Ada.Strings.Bounded is
Low : Positive; Low : Positive;
High : Natural; High : Natural;
By : String; 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 procedure Replace_Slice
(Source : in out Bounded_String; (Source : in out Bounded_String;
Low : Positive; Low : Positive;
High : Natural; High : Natural;
By : String; 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 function Insert
(Source : Bounded_String; (Source : Bounded_String;
Before : Positive; Before : Positive;
New_Item : String; 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 procedure Insert
(Source : in out Bounded_String; (Source : in out Bounded_String;
Before : Positive; Before : Positive;
New_Item : String; 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 function Overwrite
(Source : Bounded_String; (Source : Bounded_String;
Position : Positive; Position : Positive;
New_Item : String; 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 procedure Overwrite
(Source : in out Bounded_String; (Source : in out Bounded_String;
Position : Positive; Position : Positive;
New_Item : String; 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 function Delete
(Source : Bounded_String; (Source : Bounded_String;
From : Positive; 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 procedure Delete
(Source : in out Bounded_String; (Source : in out Bounded_String;
From : Positive; 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 -- -- String Selector Subprograms --
...@@ -383,45 +686,73 @@ package Ada.Strings.Bounded is ...@@ -383,45 +686,73 @@ package Ada.Strings.Bounded is
function Trim function Trim
(Source : Bounded_String; (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 procedure Trim
(Source : in out Bounded_String; (Source : in out Bounded_String;
Side : Trim_End); Side : Trim_End)
with
Post => Length (Source) <= Length (Source)'Old,
Global => null;
function Trim function Trim
(Source : Bounded_String; (Source : Bounded_String;
Left : Maps.Character_Set; 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 procedure Trim
(Source : in out Bounded_String; (Source : in out Bounded_String;
Left : Maps.Character_Set; Left : Maps.Character_Set;
Right : Maps.Character_Set); Right : Maps.Character_Set)
with
Post => Length (Source) <= Length (Source)'Old,
Global => null;
function Head function Head
(Source : Bounded_String; (Source : Bounded_String;
Count : Natural; Count : Natural;
Pad : Character := Space; 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 procedure Head
(Source : in out Bounded_String; (Source : in out Bounded_String;
Count : Natural; Count : Natural;
Pad : Character := Space; 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 function Tail
(Source : Bounded_String; (Source : Bounded_String;
Count : Natural; Count : Natural;
Pad : Character := Space; 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 procedure Tail
(Source : in out Bounded_String; (Source : in out Bounded_String;
Count : Natural; Count : Natural;
Pad : Character := Space; 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 -- -- String Constructor Subprograms --
...@@ -429,30 +760,66 @@ package Ada.Strings.Bounded is ...@@ -429,30 +760,66 @@ package Ada.Strings.Bounded is
function "*" function "*"
(Left : Natural; (Left : Natural;
Right : Character) return Bounded_String; Right : Character) return Bounded_String
with
Pre => Left <= Max_Length,
Post => Length ("*"'Result) = Left,
Global => null;
function "*" function "*"
(Left : Natural; (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 "*" function "*"
(Left : Natural; (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 function Replicate
(Count : Natural; (Count : Natural;
Item : Character; 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 function Replicate
(Count : Natural; (Count : Natural;
Item : String; 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 function Replicate
(Count : Natural; (Count : Natural;
Item : Bounded_String; 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 private
-- Most of the implementation is in the separate non generic package -- Most of the implementation is in the separate non generic package
......
gcc/ada/libgnat/a-strfix.ads
...@@ -13,6 +13,12 @@ ...@@ -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; with Ada.Strings.Maps;
-- The language-defined package Strings.Fixed provides string-handling -- The language-defined package Strings.Fixed provides string-handling
...@@ -34,7 +40,7 @@ with Ada.Strings.Maps; ...@@ -34,7 +40,7 @@ with Ada.Strings.Maps;
-- these effects. Similar control is provided by the string transformation -- these effects. Similar control is provided by the string transformation
-- procedures. -- procedures.
package Ada.Strings.Fixed is package Ada.Strings.Fixed with SPARK_Mode is
pragma Preelaborate; pragma Preelaborate;
-------------------------------------------------------------- --------------------------------------------------------------
...@@ -46,7 +52,12 @@ package Ada.Strings.Fixed is ...@@ -46,7 +52,12 @@ package Ada.Strings.Fixed is
Target : out String; Target : out String;
Drop : Truncation := Error; Drop : Truncation := Error;
Justify : Alignment := Left; 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 -- 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 -- has the same length as Target, then the effect is to assign Source to
-- Target. If Source is shorter than Target then: -- Target. If Source is shorter than Target then:
...@@ -95,7 +106,12 @@ package Ada.Strings.Fixed is ...@@ -95,7 +106,12 @@ package Ada.Strings.Fixed is
Pattern : String; Pattern : String;
From : Positive; From : Positive;
Going : Direction := Forward; 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); pragma Ada_05 (Index);
function Index function Index
...@@ -103,7 +119,12 @@ package Ada.Strings.Fixed is ...@@ -103,7 +119,12 @@ package Ada.Strings.Fixed is
Pattern : String; Pattern : String;
From : Positive; From : Positive;
Going : Direction := Forward; 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); pragma Ada_05 (Index);
-- Each Index function searches, starting from From, for a slice of -- Each Index function searches, starting from From, for a slice of
...@@ -123,13 +144,19 @@ package Ada.Strings.Fixed is ...@@ -123,13 +144,19 @@ package Ada.Strings.Fixed is
(Source : String; (Source : String;
Pattern : String; Pattern : String;
Going : Direction := Forward; 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 function Index
(Source : String; (Source : String;
Pattern : String; Pattern : String;
Going : Direction := Forward; 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: -- If Going = Forward, returns:
-- --
...@@ -143,14 +170,19 @@ package Ada.Strings.Fixed is ...@@ -143,14 +170,19 @@ package Ada.Strings.Fixed is
(Source : String; (Source : String;
Set : Maps.Character_Set; Set : Maps.Character_Set;
Test : Membership := Inside; Test : Membership := Inside;
Going : Direction := Forward) return Natural; Going : Direction := Forward) return Natural
with
Global => null;
function Index function Index
(Source : String; (Source : String;
Set : Maps.Character_Set; Set : Maps.Character_Set;
From : Positive; From : Positive;
Test : Membership := Inside; 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); pragma Ada_05 (Index);
-- Index searches for the first or last occurrence of any of a set of -- 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 -- characters (when Test=Inside), or any of the complement of a set of
...@@ -164,24 +196,35 @@ package Ada.Strings.Fixed is ...@@ -164,24 +196,35 @@ package Ada.Strings.Fixed is
function Index_Non_Blank function Index_Non_Blank
(Source : String; (Source : String;
From : Positive; 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); pragma Ada_05 (Index_Non_Blank);
-- Returns Index (Source, Maps.To_Set(Space), From, Outside, Going) -- Returns Index (Source, Maps.To_Set(Space), From, Outside, Going)
function Index_Non_Blank function Index_Non_Blank
(Source : String; (Source : String;
Going : Direction := Forward) return Natural; Going : Direction := Forward) return Natural
with
Global => null;
-- Returns Index (Source, Maps.To_Set(Space), Outside, Going) -- Returns Index (Source, Maps.To_Set(Space), Outside, Going)
function Count function Count
(Source : String; (Source : String;
Pattern : 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 function Count
(Source : String; (Source : String;
Pattern : 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 -- Returns the maximum number of nonoverlapping slices of Source that match
-- Pattern with respect to Mapping. If Pattern is the null string then -- Pattern with respect to Mapping. If Pattern is the null string then
...@@ -189,7 +232,9 @@ package Ada.Strings.Fixed is ...@@ -189,7 +232,9 @@ package Ada.Strings.Fixed is
function Count function Count
(Source : String; (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 -- Returns the number of occurrences in Source of characters that are in
-- Set. -- Set.
...@@ -199,7 +244,10 @@ package Ada.Strings.Fixed is ...@@ -199,7 +244,10 @@ package Ada.Strings.Fixed is
From : Positive; From : Positive;
Test : Membership; Test : Membership;
First : out Positive; 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); pragma Ada_2012 (Find_Token);
-- If Source is not the null string and From is not in Source'Range, then -- 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 -- Index_Error is raised. Otherwise, First is set to the index of the first
...@@ -214,7 +262,9 @@ package Ada.Strings.Fixed is ...@@ -214,7 +262,9 @@ package Ada.Strings.Fixed is
Set : Maps.Character_Set; Set : Maps.Character_Set;
Test : Membership; Test : Membership;
First : out Positive; First : out Positive;
Last : out Natural); Last : out Natural)
with
Global => null;
-- Equivalent to Find_Token (Source, Set, Source'First, Test, First, Last) -- Equivalent to Find_Token (Source, Set, Source'First, Test, First, Last)
------------------------------------ ------------------------------------
...@@ -223,11 +273,17 @@ package Ada.Strings.Fixed is ...@@ -223,11 +273,17 @@ package Ada.Strings.Fixed is
function Translate function Translate
(Source : String; (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 function Translate
(Source : String; (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) -- 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 -- is the character to which Mapping maps the corresponding element of
...@@ -235,11 +291,15 @@ package Ada.Strings.Fixed is ...@@ -235,11 +291,15 @@ package Ada.Strings.Fixed is
procedure Translate procedure Translate
(Source : in out String; (Source : in out String;
Mapping : Maps.Character_Mapping_Function); Mapping : Maps.Character_Mapping_Function)
with
Global => null;
procedure Translate procedure Translate
(Source : in out String; (Source : in out String;
Mapping : Maps.Character_Mapping); Mapping : Maps.Character_Mapping)
with
Global => null;
-- Equivalent to Source := Translate(Source, Mapping) -- Equivalent to Source := Translate(Source, Mapping)
...@@ -254,7 +314,15 @@ package Ada.Strings.Fixed is ...@@ -254,7 +314,15 @@ package Ada.Strings.Fixed is
By : String; By : String;
Drop : Truncation := Error; Drop : Truncation := Error;
Justify : Alignment := Left; 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 -- If Low > Source'Last+1, or High < Source'First - 1, then Index_Error is
-- propagated. Otherwise: -- propagated. Otherwise:
-- --
...@@ -269,7 +337,25 @@ package Ada.Strings.Fixed is ...@@ -269,7 +337,25 @@ package Ada.Strings.Fixed is
(Source : String; (Source : String;
Low : Positive; Low : Positive;
High : Natural; 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: -- Equivalent to:
-- --
-- Move (Replace_Slice (Source, Low, High, By), -- Move (Replace_Slice (Source, Low, High, By),
...@@ -278,7 +364,13 @@ package Ada.Strings.Fixed is ...@@ -278,7 +364,13 @@ package Ada.Strings.Fixed is
function Insert function Insert
(Source : String; (Source : String;
Before : Positive; 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 -- Propagates Index_Error if Before is not in
-- Source'First .. Source'Last+1; otherwise, returns -- Source'First .. Source'Last+1; otherwise, returns
-- Source (Source'First .. Before - 1) -- Source (Source'First .. Before - 1)
...@@ -288,13 +380,30 @@ package Ada.Strings.Fixed is ...@@ -288,13 +380,30 @@ package Ada.Strings.Fixed is
(Source : in out String; (Source : in out String;
Before : Positive; Before : Positive;
New_Item : String; 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) -- Equivalent to Move (Insert (Source, Before, New_Item), Source, Drop)
function Overwrite function Overwrite
(Source : String; (Source : String;
Position : Positive; 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 -- Propagates Index_Error if Position is not in
-- Source'First .. Source'Last + 1; otherwise, returns the string obtained -- Source'First .. Source'Last + 1; otherwise, returns the string obtained
-- from Source by consecutively replacing characters starting at Position -- from Source by consecutively replacing characters starting at Position
...@@ -306,13 +415,29 @@ package Ada.Strings.Fixed is ...@@ -306,13 +415,29 @@ package Ada.Strings.Fixed is
(Source : in out String; (Source : in out String;
Position : Positive; Position : Positive;
New_Item : String; 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) -- Equivalent to Move(Overwrite(Source, Position, New_Item), Source, Drop)
function Delete function Delete
(Source : String; (Source : String;
From : Positive; 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 -- If From <= Through, the returned string is
-- Replace_Slice(Source, From, Through, ""); otherwise, it is Source with -- Replace_Slice(Source, From, Through, ""); otherwise, it is Source with
-- lower bound 1. -- lower bound 1.
...@@ -322,7 +447,15 @@ package Ada.Strings.Fixed is ...@@ -322,7 +447,15 @@ package Ada.Strings.Fixed is
From : Positive; From : Positive;
Through : Natural; Through : Natural;
Justify : Alignment := Left; 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: -- Equivalent to:
-- --
-- Move (Delete (Source, From, Through), -- Move (Delete (Source, From, Through),
...@@ -334,7 +467,10 @@ package Ada.Strings.Fixed is ...@@ -334,7 +467,10 @@ package Ada.Strings.Fixed is
function Trim function Trim
(Source : String; (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 -- Returns the string obtained by removing from Source all leading Space
-- characters (if Side = Left), all trailing Space characters (if -- characters (if Side = Left), all trailing Space characters (if
-- Side = Right), or all leading and trailing Space characters (if -- Side = Right), or all leading and trailing Space characters (if
...@@ -344,7 +480,12 @@ package Ada.Strings.Fixed is ...@@ -344,7 +480,12 @@ package Ada.Strings.Fixed is
(Source : in out String; (Source : in out String;
Side : Trim_End; Side : Trim_End;
Justify : Alignment := Left; Justify : Alignment := Left;
Pad : Character := Space); Pad : Character := Space)
with
-- Incomplete contract
Global => null;
-- Equivalent to: -- Equivalent to:
-- --
-- Move (Trim (Source, Side), Source, Justify=>Justify, Pad=>Pad). -- Move (Trim (Source, Side), Source, Justify=>Justify, Pad=>Pad).
...@@ -352,7 +493,10 @@ package Ada.Strings.Fixed is ...@@ -352,7 +493,10 @@ package Ada.Strings.Fixed is
function Trim function Trim
(Source : String; (Source : String;
Left : Maps.Character_Set; 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 -- Returns the string obtained by removing from Source all leading
-- characters in Left and all trailing characters in Right. -- characters in Left and all trailing characters in Right.
...@@ -361,7 +505,12 @@ package Ada.Strings.Fixed is ...@@ -361,7 +505,12 @@ package Ada.Strings.Fixed is
Left : Maps.Character_Set; Left : Maps.Character_Set;
Right : Maps.Character_Set; Right : Maps.Character_Set;
Justify : Alignment := Strings.Left; Justify : Alignment := Strings.Left;
Pad : Character := Space); Pad : Character := Space)
with
-- Incomplete contract
Global => null;
-- Equivalent to: -- Equivalent to:
-- --
-- Move (Trim (Source, Left, Right), -- Move (Trim (Source, Left, Right),
...@@ -370,7 +519,10 @@ package Ada.Strings.Fixed is ...@@ -370,7 +519,10 @@ package Ada.Strings.Fixed is
function Head function Head
(Source : String; (Source : String;
Count : Natural; 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 -- Returns a string of length Count. If Count <= Source'Length, the string
-- comprises the first Count characters of Source. Otherwise, its contents -- comprises the first Count characters of Source. Otherwise, its contents
-- are Source concatenated with Count - Source'Length Pad characters. -- are Source concatenated with Count - Source'Length Pad characters.
...@@ -379,7 +531,12 @@ package Ada.Strings.Fixed is ...@@ -379,7 +531,12 @@ package Ada.Strings.Fixed is
(Source : in out String; (Source : in out String;
Count : Natural; Count : Natural;
Justify : Alignment := Left; Justify : Alignment := Left;
Pad : Character := Space); Pad : Character := Space)
with
-- Incomplete contract
Global => null;
-- Equivalent to: -- Equivalent to:
-- --
-- Move (Head (Source, Count, Pad), -- Move (Head (Source, Count, Pad),
...@@ -388,7 +545,10 @@ package Ada.Strings.Fixed is ...@@ -388,7 +545,10 @@ package Ada.Strings.Fixed is
function Tail function Tail
(Source : String; (Source : String;
Count : Natural; 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 -- Returns a string of length Count. If Count <= Source'Length, the string
-- comprises the last Count characters of Source. Otherwise, its contents -- comprises the last Count characters of Source. Otherwise, its contents
-- are Count-Source'Length Pad characters concatenated with Source. -- are Count-Source'Length Pad characters concatenated with Source.
...@@ -397,7 +557,12 @@ package Ada.Strings.Fixed is ...@@ -397,7 +557,12 @@ package Ada.Strings.Fixed is
(Source : in out String; (Source : in out String;
Count : Natural; Count : Natural;
Justify : Alignment := Left; Justify : Alignment := Left;
Pad : Character := Space); Pad : Character := Space)
with
-- Incomplete contract
Global => null;
-- Equivalent to: -- Equivalent to:
-- --
-- Move (Tail (Source, Count, Pad), -- Move (Tail (Source, Count, Pad),
...@@ -409,11 +574,18 @@ package Ada.Strings.Fixed is ...@@ -409,11 +574,18 @@ package Ada.Strings.Fixed is
function "*" function "*"
(Left : Natural; (Left : Natural;
Right : Character) return String; Right : Character) return String
with
Post => "*"'Result'Length = Left,
Global => null;
function "*" function "*"
(Left : Natural; (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 -- These functions replicate a character or string a specified number of
-- times. The first function returns a string whose length is Left and each -- times. The first function returns a string whose length is Left and each
......
gcc/ada/libgnat/a-strunb.ads
...@@ -33,6 +33,12 @@ ...@@ -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.Maps;
with Ada.Finalization; with Ada.Finalization;
...@@ -45,7 +51,9 @@ with Ada.Finalization; ...@@ -45,7 +51,9 @@ with Ada.Finalization;
-- length. Since the Unbounded_String type is private, relevant constructor -- length. Since the Unbounded_String type is private, relevant constructor
-- and selector operations are provided. -- 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; pragma Preelaborate;
type Unbounded_String is private; type Unbounded_String is private;
...@@ -56,7 +64,8 @@ package Ada.Strings.Unbounded is ...@@ -56,7 +64,8 @@ package Ada.Strings.Unbounded is
-- otherwise initialized, it will be initialized to the same value as -- otherwise initialized, it will be initialized to the same value as
-- Null_Unbounded_String. -- 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 -- Returns the length of the String represented by Source
type String_Access is access all String; type String_Access is access all String;
...@@ -71,15 +80,25 @@ package Ada.Strings.Unbounded is ...@@ -71,15 +80,25 @@ package Ada.Strings.Unbounded is
-------------------------------------------------------- --------------------------------------------------------
function To_Unbounded_String 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 -- Returns an Unbounded_String that represents Source
function To_Unbounded_String 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 -- Returns an Unbounded_String that represents an uninitialized String
-- whose length is Length. -- 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 -- Returns the String with lower bound 1 represented by Source
-- To_String and To_Unbounded_String are related as follows: -- To_String and To_Unbounded_String are related as follows:
...@@ -91,21 +110,35 @@ package Ada.Strings.Unbounded is ...@@ -91,21 +110,35 @@ package Ada.Strings.Unbounded is
procedure Set_Unbounded_String procedure Set_Unbounded_String
(Target : out Unbounded_String; (Target : out Unbounded_String;
Source : String); Source : String)
with
Global => null;
pragma Ada_05 (Set_Unbounded_String); pragma Ada_05 (Set_Unbounded_String);
-- Sets Target to an Unbounded_String that represents Source -- Sets Target to an Unbounded_String that represents Source
procedure Append procedure Append
(Source : in out Unbounded_String; (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 procedure Append
(Source : in out Unbounded_String; (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 procedure Append
(Source : in out Unbounded_String; (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 -- For each of the Append procedures, the resulting string represented by
-- the Source parameter is given by the concatenation of the original value -- the Source parameter is given by the concatenation of the original value
...@@ -113,23 +146,43 @@ package Ada.Strings.Unbounded is ...@@ -113,23 +146,43 @@ package Ada.Strings.Unbounded is
function "&" function "&"
(Left : Unbounded_String; (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 "&" function "&"
(Left : Unbounded_String; (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 "&" function "&"
(Left : String; (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 "&" function "&"
(Left : Unbounded_String; (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 "&" function "&"
(Left : Character; (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 -- Each of the "&" functions returns an Unbounded_String obtained by
-- concatenating the string or character given or represented by one of the -- concatenating the string or character given or represented by one of the
...@@ -139,14 +192,21 @@ package Ada.Strings.Unbounded is ...@@ -139,14 +192,21 @@ package Ada.Strings.Unbounded is
function Element function Element
(Source : Unbounded_String; (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 -- Returns the character at position Index in the string represented by
-- Source; propagates Index_Error if Index > Length (Source). -- Source; propagates Index_Error if Index > Length (Source).
procedure Replace_Element procedure Replace_Element
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Index : Positive; 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 -- Updates Source such that the character at position Index in the string
-- represented by Source is By; propagates Index_Error if -- represented by Source is By; propagates Index_Error if
-- Index > Length (Source). -- Index > Length (Source).
...@@ -154,7 +214,11 @@ package Ada.Strings.Unbounded is ...@@ -154,7 +214,11 @@ package Ada.Strings.Unbounded is
function Slice function Slice
(Source : Unbounded_String; (Source : Unbounded_String;
Low : Positive; 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 -- Returns the slice at positions Low through High in the string
-- represented by Source; propagates Index_Error if -- represented by Source; propagates Index_Error if
-- Low > Length (Source) + 1 or High > Length (Source). The bounds of the -- Low > Length (Source) + 1 or High > Length (Source). The bounds of the
...@@ -163,7 +227,12 @@ package Ada.Strings.Unbounded is ...@@ -163,7 +227,12 @@ package Ada.Strings.Unbounded is
function Unbounded_Slice function Unbounded_Slice
(Source : Unbounded_String; (Source : Unbounded_String;
Low : Positive; 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); pragma Ada_05 (Unbounded_Slice);
-- Returns the slice at positions Low through High in the string -- Returns the slice at positions Low through High in the string
-- represented by Source as an Unbounded_String. This propagates -- represented by Source as an Unbounded_String. This propagates
...@@ -173,7 +242,11 @@ package Ada.Strings.Unbounded is ...@@ -173,7 +242,11 @@ package Ada.Strings.Unbounded is
(Source : Unbounded_String; (Source : Unbounded_String;
Target : out Unbounded_String; Target : out Unbounded_String;
Low : Positive; 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); pragma Ada_05 (Unbounded_Slice);
-- Sets Target to the Unbounded_String representing the slice at positions -- Sets Target to the Unbounded_String representing the slice at positions
-- Low through High in the string represented by Source. This propagates -- Low through High in the string represented by Source. This propagates
...@@ -181,63 +254,93 @@ package Ada.Strings.Unbounded is ...@@ -181,63 +254,93 @@ package Ada.Strings.Unbounded is
function "=" function "="
(Left : Unbounded_String; (Left : Unbounded_String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function "=" function "="
(Left : Unbounded_String; (Left : Unbounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function "=" function "="
(Left : String; (Left : String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function "<" function "<"
(Left : Unbounded_String; (Left : Unbounded_String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function "<" function "<"
(Left : Unbounded_String; (Left : Unbounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function "<" function "<"
(Left : String; (Left : String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function "<=" function "<="
(Left : Unbounded_String; (Left : Unbounded_String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function "<=" function "<="
(Left : Unbounded_String; (Left : Unbounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function "<=" function "<="
(Left : String; (Left : String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function ">" function ">"
(Left : Unbounded_String; (Left : Unbounded_String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function ">" function ">"
(Left : Unbounded_String; (Left : Unbounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function ">" function ">"
(Left : String; (Left : String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function ">=" function ">="
(Left : Unbounded_String; (Left : Unbounded_String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function ">=" function ">="
(Left : Unbounded_String; (Left : Unbounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function ">=" function ">="
(Left : String; (Left : String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
-- Each of the functions "=", "<", ">", "<=", and ">=" returns the same -- Each of the functions "=", "<", ">", "<=", and ">=" returns the same
-- result as the corresponding String operation applied to the String -- result as the corresponding String operation applied to the String
...@@ -251,26 +354,38 @@ package Ada.Strings.Unbounded is ...@@ -251,26 +354,38 @@ package Ada.Strings.Unbounded is
(Source : Unbounded_String; (Source : Unbounded_String;
Pattern : String; Pattern : String;
Going : Direction := Forward; 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 function Index
(Source : Unbounded_String; (Source : Unbounded_String;
Pattern : String; Pattern : String;
Going : Direction := Forward; 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 function Index
(Source : Unbounded_String; (Source : Unbounded_String;
Set : Maps.Character_Set; Set : Maps.Character_Set;
Test : Membership := Inside; Test : Membership := Inside;
Going : Direction := Forward) return Natural; Going : Direction := Forward) return Natural
with
Global => null;
function Index function Index
(Source : Unbounded_String; (Source : Unbounded_String;
Pattern : String; Pattern : String;
From : Positive; From : Positive;
Going : Direction := Forward; 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); pragma Ada_05 (Index);
function Index function Index
...@@ -278,7 +393,11 @@ package Ada.Strings.Unbounded is ...@@ -278,7 +393,11 @@ package Ada.Strings.Unbounded is
Pattern : String; Pattern : String;
From : Positive; From : Positive;
Going : Direction := Forward; 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); pragma Ada_05 (Index);
function Index function Index
...@@ -286,32 +405,48 @@ package Ada.Strings.Unbounded is ...@@ -286,32 +405,48 @@ package Ada.Strings.Unbounded is
Set : Maps.Character_Set; Set : Maps.Character_Set;
From : Positive; From : Positive;
Test : Membership := Inside; 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); pragma Ada_05 (Index);
function Index_Non_Blank function Index_Non_Blank
(Source : Unbounded_String; (Source : Unbounded_String;
Going : Direction := Forward) return Natural; Going : Direction := Forward) return Natural
with
Global => null;
function Index_Non_Blank function Index_Non_Blank
(Source : Unbounded_String; (Source : Unbounded_String;
From : Positive; 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); pragma Ada_05 (Index_Non_Blank);
function Count function Count
(Source : Unbounded_String; (Source : Unbounded_String;
Pattern : 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 function Count
(Source : Unbounded_String; (Source : Unbounded_String;
Pattern : 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 function Count
(Source : Unbounded_String; (Source : Unbounded_String;
Set : Maps.Character_Set) return Natural; Set : Maps.Character_Set) return Natural
with
Global => null;
procedure Find_Token procedure Find_Token
(Source : Unbounded_String; (Source : Unbounded_String;
...@@ -319,7 +454,10 @@ package Ada.Strings.Unbounded is ...@@ -319,7 +454,10 @@ package Ada.Strings.Unbounded is
From : Positive; From : Positive;
Test : Membership; Test : Membership;
First : out Positive; 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); pragma Ada_2012 (Find_Token);
procedure Find_Token procedure Find_Token
...@@ -327,7 +465,9 @@ package Ada.Strings.Unbounded is ...@@ -327,7 +465,9 @@ package Ada.Strings.Unbounded is
Set : Maps.Character_Set; Set : Maps.Character_Set;
Test : Membership; Test : Membership;
First : out Positive; First : out Positive;
Last : out Natural); Last : out Natural)
with
Global => null;
-- Each of the search subprograms (Index, Index_Non_Blank, Count, -- Each of the search subprograms (Index, Index_Non_Blank, Count,
-- Find_Token) has the same effect as the corresponding subprogram in -- Find_Token) has the same effect as the corresponding subprogram in
...@@ -340,19 +480,31 @@ package Ada.Strings.Unbounded is ...@@ -340,19 +480,31 @@ package Ada.Strings.Unbounded is
function Translate function Translate
(Source : Unbounded_String; (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 procedure Translate
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Mapping : Maps.Character_Mapping); Mapping : Maps.Character_Mapping)
with
Post => Length (Source) = Length (Source)'Old,
Global => null;
function Translate function Translate
(Source : Unbounded_String; (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 procedure Translate
(Source : in out Unbounded_String; (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 -- The Translate function has an analogous effect to the corresponding
-- subprogram in Strings.Fixed. The translation is applied to the string -- subprogram in Strings.Fixed. The translation is applied to the string
...@@ -367,93 +519,204 @@ package Ada.Strings.Unbounded is ...@@ -367,93 +519,204 @@ package Ada.Strings.Unbounded is
(Source : Unbounded_String; (Source : Unbounded_String;
Low : Positive; Low : Positive;
High : Natural; 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 procedure Replace_Slice
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Low : Positive; Low : Positive;
High : Natural; 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 function Insert
(Source : Unbounded_String; (Source : Unbounded_String;
Before : Positive; 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 procedure Insert
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Before : Positive; 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 function Overwrite
(Source : Unbounded_String; (Source : Unbounded_String;
Position : Positive; 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 procedure Overwrite
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Position : Positive; 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 function Delete
(Source : Unbounded_String; (Source : Unbounded_String;
From : Positive; 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 procedure Delete
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
From : Positive; 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 function Trim
(Source : Unbounded_String; (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 procedure Trim
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Side : Trim_End); Side : Trim_End)
with
Post => Length (Source) <= Length (Source)'Old,
Global => null;
function Trim function Trim
(Source : Unbounded_String; (Source : Unbounded_String;
Left : Maps.Character_Set; 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 procedure Trim
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Left : Maps.Character_Set; Left : Maps.Character_Set;
Right : Maps.Character_Set); Right : Maps.Character_Set)
with
Post => Length (Source) <= Length (Source)'Old,
Global => null;
function Head function Head
(Source : Unbounded_String; (Source : Unbounded_String;
Count : Natural; Count : Natural;
Pad : Character := Space) return Unbounded_String; Pad : Character := Space) return Unbounded_String
with
Post => Length (Head'Result) = Count,
Global => null;
procedure Head procedure Head
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Count : Natural; Count : Natural;
Pad : Character := Space); Pad : Character := Space)
with
Post => Length (Source) = Count,
Global => null;
function Tail function Tail
(Source : Unbounded_String; (Source : Unbounded_String;
Count : Natural; Count : Natural;
Pad : Character := Space) return Unbounded_String; Pad : Character := Space) return Unbounded_String
with
Post => Length (Tail'Result) = Count,
Global => null;
procedure Tail procedure Tail
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Count : Natural; Count : Natural;
Pad : Character := Space); Pad : Character := Space)
with
Post => Length (Source) = Count,
Global => null;
function "*" function "*"
(Left : Natural; (Left : Natural;
Right : Character) return Unbounded_String; Right : Character) return Unbounded_String
with
Pre => Left <= Natural'Last,
Post => Length ("*"'Result) = Left,
Global => null;
function "*" function "*"
(Left : Natural; (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 "*" function "*"
(Left : Natural; (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, -- Each of the transformation functions (Replace_Slice, Insert, Overwrite,
-- Delete), selector functions (Trim, Head, Tail), and constructor -- Delete), selector functions (Trim, Head, Tail), and constructor
......
gcc/ada/libgnat/a-strunb__shared.ads
...@@ -33,6 +33,12 @@ ...@@ -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 -- This package provides an implementation of Ada.Strings.Unbounded that uses
-- reference counts to implement copy on modification (rather than copy on -- reference counts to implement copy on modification (rather than copy on
-- assignment). This is significantly more efficient on many targets. -- assignment). This is significantly more efficient on many targets.
...@@ -73,7 +79,9 @@ with Ada.Strings.Maps; ...@@ -73,7 +79,9 @@ with Ada.Strings.Maps;
private with Ada.Finalization; private with Ada.Finalization;
private with System.Atomic_Counters; 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; pragma Preelaborate;
type Unbounded_String is private; type Unbounded_String is private;
...@@ -81,7 +89,8 @@ package Ada.Strings.Unbounded is ...@@ -81,7 +89,8 @@ package Ada.Strings.Unbounded is
Null_Unbounded_String : constant Unbounded_String; 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; type String_Access is access all String;
...@@ -92,136 +101,229 @@ package Ada.Strings.Unbounded is ...@@ -92,136 +101,229 @@ package Ada.Strings.Unbounded is
-------------------------------------------------------- --------------------------------------------------------
function To_Unbounded_String 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 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 procedure Set_Unbounded_String
(Target : out Unbounded_String; (Target : out Unbounded_String;
Source : String); Source : String)
with
Global => null;
pragma Ada_05 (Set_Unbounded_String); pragma Ada_05 (Set_Unbounded_String);
procedure Append procedure Append
(Source : in out Unbounded_String; (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 procedure Append
(Source : in out Unbounded_String; (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 procedure Append
(Source : in out Unbounded_String; (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 "&" function "&"
(Left : Unbounded_String; (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 "&" function "&"
(Left : Unbounded_String; (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 "&" function "&"
(Left : String; (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 "&" function "&"
(Left : Unbounded_String; (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 "&" function "&"
(Left : Character; (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 function Element
(Source : Unbounded_String; (Source : Unbounded_String;
Index : Positive) return Character; Index : Positive) return Character
with
Pre => Index <= Length (Source),
Global => null;
procedure Replace_Element procedure Replace_Element
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Index : Positive; Index : Positive;
By : Character); By : Character)
with
Pre => Index <= Length (Source),
Post => Length (Source) = Length (Source)'Old,
Global => null;
function Slice function Slice
(Source : Unbounded_String; (Source : Unbounded_String;
Low : Positive; 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 function Unbounded_Slice
(Source : Unbounded_String; (Source : Unbounded_String;
Low : Positive; 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); pragma Ada_05 (Unbounded_Slice);
procedure Unbounded_Slice procedure Unbounded_Slice
(Source : Unbounded_String; (Source : Unbounded_String;
Target : out Unbounded_String; Target : out Unbounded_String;
Low : Positive; 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); pragma Ada_05 (Unbounded_Slice);
function "=" function "="
(Left : Unbounded_String; (Left : Unbounded_String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function "=" function "="
(Left : Unbounded_String; (Left : Unbounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function "=" function "="
(Left : String; (Left : String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function "<" function "<"
(Left : Unbounded_String; (Left : Unbounded_String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function "<" function "<"
(Left : Unbounded_String; (Left : Unbounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function "<" function "<"
(Left : String; (Left : String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function "<=" function "<="
(Left : Unbounded_String; (Left : Unbounded_String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function "<=" function "<="
(Left : Unbounded_String; (Left : Unbounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function "<=" function "<="
(Left : String; (Left : String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function ">" function ">"
(Left : Unbounded_String; (Left : Unbounded_String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function ">" function ">"
(Left : Unbounded_String; (Left : Unbounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function ">" function ">"
(Left : String; (Left : String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function ">=" function ">="
(Left : Unbounded_String; (Left : Unbounded_String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
function ">=" function ">="
(Left : Unbounded_String; (Left : Unbounded_String;
Right : String) return Boolean; Right : String) return Boolean
with
Global => null;
function ">=" function ">="
(Left : String; (Left : String;
Right : Unbounded_String) return Boolean; Right : Unbounded_String) return Boolean
with
Global => null;
------------------------ ------------------------
-- Search Subprograms -- -- Search Subprograms --
...@@ -231,26 +333,39 @@ package Ada.Strings.Unbounded is ...@@ -231,26 +333,39 @@ package Ada.Strings.Unbounded is
(Source : Unbounded_String; (Source : Unbounded_String;
Pattern : String; Pattern : String;
Going : Direction := Forward; 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 function Index
(Source : Unbounded_String; (Source : Unbounded_String;
Pattern : String; Pattern : String;
Going : Direction := Forward; 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 function Index
(Source : Unbounded_String; (Source : Unbounded_String;
Set : Maps.Character_Set; Set : Maps.Character_Set;
Test : Membership := Inside; Test : Membership := Inside;
Going : Direction := Forward) return Natural; Going : Direction := Forward) return Natural
with
Global => null;
function Index function Index
(Source : Unbounded_String; (Source : Unbounded_String;
Pattern : String; Pattern : String;
From : Positive; From : Positive;
Going : Direction := Forward; 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); pragma Ada_05 (Index);
function Index function Index
...@@ -258,7 +373,13 @@ package Ada.Strings.Unbounded is ...@@ -258,7 +373,13 @@ package Ada.Strings.Unbounded is
Pattern : String; Pattern : String;
From : Positive; From : Positive;
Going : Direction := Forward; 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); pragma Ada_05 (Index);
function Index function Index
...@@ -266,32 +387,48 @@ package Ada.Strings.Unbounded is ...@@ -266,32 +387,48 @@ package Ada.Strings.Unbounded is
Set : Maps.Character_Set; Set : Maps.Character_Set;
From : Positive; From : Positive;
Test : Membership := Inside; 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); pragma Ada_05 (Index);
function Index_Non_Blank function Index_Non_Blank
(Source : Unbounded_String; (Source : Unbounded_String;
Going : Direction := Forward) return Natural; Going : Direction := Forward) return Natural
with
Global => null;
function Index_Non_Blank function Index_Non_Blank
(Source : Unbounded_String; (Source : Unbounded_String;
From : Positive; 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); pragma Ada_05 (Index_Non_Blank);
function Count function Count
(Source : Unbounded_String; (Source : Unbounded_String;
Pattern : 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 function Count
(Source : Unbounded_String; (Source : Unbounded_String;
Pattern : 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 function Count
(Source : Unbounded_String; (Source : Unbounded_String;
Set : Maps.Character_Set) return Natural; Set : Maps.Character_Set) return Natural
with
Global => null;
procedure Find_Token procedure Find_Token
(Source : Unbounded_String; (Source : Unbounded_String;
...@@ -299,7 +436,10 @@ package Ada.Strings.Unbounded is ...@@ -299,7 +436,10 @@ package Ada.Strings.Unbounded is
From : Positive; From : Positive;
Test : Membership; Test : Membership;
First : out Positive; 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); pragma Ada_2012 (Find_Token);
procedure Find_Token procedure Find_Token
...@@ -307,7 +447,9 @@ package Ada.Strings.Unbounded is ...@@ -307,7 +447,9 @@ package Ada.Strings.Unbounded is
Set : Maps.Character_Set; Set : Maps.Character_Set;
Test : Membership; Test : Membership;
First : out Positive; First : out Positive;
Last : out Natural); Last : out Natural)
with
Global => null;
------------------------------------ ------------------------------------
-- String Translation Subprograms -- -- String Translation Subprograms --
...@@ -315,19 +457,31 @@ package Ada.Strings.Unbounded is ...@@ -315,19 +457,31 @@ package Ada.Strings.Unbounded is
function Translate function Translate
(Source : Unbounded_String; (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 procedure Translate
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Mapping : Maps.Character_Mapping); Mapping : Maps.Character_Mapping)
with
Post => Length (Source) = Length (Source)'Old,
Global => null;
function Translate function Translate
(Source : Unbounded_String; (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 procedure Translate
(Source : in out Unbounded_String; (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 -- -- String Transformation Subprograms --
...@@ -337,93 +491,204 @@ package Ada.Strings.Unbounded is ...@@ -337,93 +491,204 @@ package Ada.Strings.Unbounded is
(Source : Unbounded_String; (Source : Unbounded_String;
Low : Positive; Low : Positive;
High : Natural; 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 procedure Replace_Slice
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Low : Positive; Low : Positive;
High : Natural; 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 function Insert
(Source : Unbounded_String; (Source : Unbounded_String;
Before : Positive; 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 procedure Insert
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Before : Positive; 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 function Overwrite
(Source : Unbounded_String; (Source : Unbounded_String;
Position : Positive; 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 procedure Overwrite
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Position : Positive; 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 function Delete
(Source : Unbounded_String; (Source : Unbounded_String;
From : Positive; 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 procedure Delete
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
From : Positive; 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 function Trim
(Source : Unbounded_String; (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 procedure Trim
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Side : Trim_End); Side : Trim_End)
with
Post => Length (Source) <= Length (Source)'Old,
Global => null;
function Trim function Trim
(Source : Unbounded_String; (Source : Unbounded_String;
Left : Maps.Character_Set; 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 procedure Trim
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Left : Maps.Character_Set; Left : Maps.Character_Set;
Right : Maps.Character_Set); Right : Maps.Character_Set)
with
Post => Length (Source) <= Length (Source)'Old,
Global => null;
function Head function Head
(Source : Unbounded_String; (Source : Unbounded_String;
Count : Natural; Count : Natural;
Pad : Character := Space) return Unbounded_String; Pad : Character := Space) return Unbounded_String
with
Post => Length (Head'Result) = Count,
Global => null;
procedure Head procedure Head
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Count : Natural; Count : Natural;
Pad : Character := Space); Pad : Character := Space)
with
Post => Length (Source) = Count,
Global => null;
function Tail function Tail
(Source : Unbounded_String; (Source : Unbounded_String;
Count : Natural; Count : Natural;
Pad : Character := Space) return Unbounded_String; Pad : Character := Space) return Unbounded_String
with
Post => Length (Tail'Result) = Count,
Global => null;
procedure Tail procedure Tail
(Source : in out Unbounded_String; (Source : in out Unbounded_String;
Count : Natural; Count : Natural;
Pad : Character := Space); Pad : Character := Space)
with
Post => Length (Source) = Count,
Global => null;
function "*" function "*"
(Left : Natural; (Left : Natural;
Right : Character) return Unbounded_String; Right : Character) return Unbounded_String
with
Pre => Left <= Natural'Last,
Post => Length ("*"'Result) = Left,
Global => null;
function "*" function "*"
(Left : Natural; (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 "*" function "*"
(Left : Natural; (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 private
pragma Inline (Length); pragma Inline (Length);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment