+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>
* sysdep.c (__gnat_is_file_not_found_error): Reformulate to also
-- --
------------------------------------------------------------------------------
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore.
+
+pragma Assertion_Policy (Pre => Ignore);
+
with Ada.Strings.Maps;
with Ada.Strings.Superbounded;
Max : Positive;
-- Maximum length of a Bounded_String
- package Generic_Bounded_Length is
+ package Generic_Bounded_Length with
+ Initial_Condition => Length (Null_Bounded_String) = 0
+ is
Max_Length : constant Positive := Max;
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 --
function To_Bounded_String
(Source : String;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre => (if Source'Length > Max_Length then Drop /= Error),
+ Post =>
+ Length (To_Bounded_String'Result)
+ = Natural'Min (Max_Length, Source'Length),
+ Global => null;
- function To_String (Source : Bounded_String) return String;
+ function To_String (Source : Bounded_String) return String with
+ Post => To_String'Result'Length = Length (Source),
+ Global => null;
procedure Set_Bounded_String
(Target : out Bounded_String;
Source : String;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre => (if Source'Length > Max_Length then Drop /= Error),
+ Post => Length (Target) = Natural'Min (Max_Length, Source'Length),
+ Global => null;
pragma Ada_05 (Set_Bounded_String);
function Append
(Left : Bounded_String;
Right : Bounded_String;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre =>
+ (if Length (Left) > Max_Length - Length (Right)
+ then Drop /= Error),
+ Post =>
+ Length (Append'Result)
+ = Natural'Min (Max_Length, Length (Left) + Length (Right)),
+ Global => null;
function Append
(Left : Bounded_String;
Right : String;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre =>
+ (if Right'Length > Max_Length - Length (Left)
+ then Drop /= Error),
+ Post =>
+ Length (Append'Result)
+ = Natural'Min (Max_Length, Length (Left) + Right'Length),
+ Global => null;
function Append
(Left : String;
Right : Bounded_String;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre =>
+ (if Left'Length > Max_Length - Length (Right)
+ then Drop /= Error),
+ Post =>
+ Length (Append'Result)
+ = Natural'Min (Max_Length, Left'Length + Length (Right)),
+ Global => null;
function Append
(Left : Bounded_String;
Right : Character;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre => (if Length (Left) = Max_Length then Drop /= Error),
+ Post =>
+ Length (Append'Result)
+ = Natural'Min (Max_Length, Length (Left) + 1),
+ Global => null;
function Append
(Left : Character;
Right : Bounded_String;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre => (if Length (Right) = Max_Length then Drop /= Error),
+ Post =>
+ Length (Append'Result)
+ = Natural'Min (Max_Length, 1 + Length (Right)),
+ Global => null;
procedure Append
(Source : in out Bounded_String;
New_Item : Bounded_String;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre =>
+ (if Length (Source) > Max_Length - Length (New_Item)
+ then Drop /= Error),
+ Post =>
+ Length (Source)
+ = Natural'Min (Max_Length, Length (Source)'Old + Length (New_Item)),
+ Global => null;
procedure Append
(Source : in out Bounded_String;
New_Item : String;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre =>
+ (if New_Item'Length > Max_Length - Length (Source)
+ then Drop /= Error),
+ Post =>
+ Length (Source)
+ = Natural'Min (Max_Length, Length (Source)'Old + New_Item'Length),
+ Global => null;
procedure Append
(Source : in out Bounded_String;
New_Item : Character;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre => (if Length (Source) = Max_Length then Drop /= Error),
+ Post =>
+ Length (Source)
+ = Natural'Min (Max_Length, Length (Source)'Old + 1),
+ Global => null;
function "&"
(Left : Bounded_String;
- Right : Bounded_String) return Bounded_String;
+ Right : Bounded_String) return Bounded_String
+ with
+ Pre => Length (Left) <= Max_Length - Length (Right),
+ Post => Length ("&"'Result) = Length (Left) + Length (Right),
+ Global => null;
function "&"
(Left : Bounded_String;
- Right : String) return Bounded_String;
+ Right : String) return Bounded_String
+ with
+ Pre => Right'Length <= Max_Length - Length (Left),
+ Post => Length ("&"'Result) = Length (Left) + Right'Length,
+ Global => null;
function "&"
(Left : String;
- Right : Bounded_String) return Bounded_String;
+ Right : Bounded_String) return Bounded_String
+ with
+ Pre => Left'Length <= Max_Length - Length (Right),
+ Post => Length ("&"'Result) = Left'Length + Length (Right),
+ Global => null;
function "&"
(Left : Bounded_String;
- Right : Character) return Bounded_String;
+ Right : Character) return Bounded_String
+ with
+ Pre => Length (Left) < Max_Length,
+ Post => Length ("&"'Result) = Length (Left) + 1,
+ Global => null;
function "&"
(Left : Character;
- Right : Bounded_String) return Bounded_String;
+ Right : Bounded_String) return Bounded_String
+ with
+ Pre => Length (Right) < Max_Length,
+ Post => Length ("&"'Result) = 1 + Length (Right),
+ Global => null;
function Element
(Source : Bounded_String;
- Index : Positive) return Character;
+ Index : Positive) return Character
+ with
+ Pre => Index <= Length (Source),
+ Global => null;
procedure Replace_Element
(Source : in out Bounded_String;
Index : Positive;
- By : Character);
+ By : Character)
+ with
+ Pre => Index <= Length (Source),
+ Post => Length (Source) = Length (Source)'Old,
+ Global => null;
function Slice
(Source : Bounded_String;
Low : Positive;
- High : Natural) return String;
+ High : Natural) return String
+ with
+ Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
+ Post => Slice'Result'Length = Natural'Max (0, High - Low + 1),
+ Global => null;
function Bounded_Slice
(Source : Bounded_String;
Low : Positive;
- High : Natural) return Bounded_String;
+ High : Natural) return Bounded_String
+ with
+ Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
+ Post =>
+ Length (Bounded_Slice'Result) = Natural'Max (0, High - Low + 1),
+ Global => null;
pragma Ada_05 (Bounded_Slice);
procedure Bounded_Slice
(Source : Bounded_String;
Target : out Bounded_String;
Low : Positive;
- High : Natural);
+ High : Natural)
+ with
+ Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
+ Post => Length (Target) = Natural'Max (0, High - Low + 1),
+ Global => null;
pragma Ada_05 (Bounded_Slice);
function "="
(Left : Bounded_String;
- Right : Bounded_String) return Boolean;
+ Right : Bounded_String) return Boolean
+ with
+ Global => null;
function "="
(Left : Bounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function "="
(Left : String;
- Right : Bounded_String) return Boolean;
+ Right : Bounded_String) return Boolean
+ with
+ Global => null;
function "<"
(Left : Bounded_String;
- Right : Bounded_String) return Boolean;
+ Right : Bounded_String) return Boolean
+ with
+ Global => null;
function "<"
(Left : Bounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function "<"
(Left : String;
- Right : Bounded_String) return Boolean;
+ Right : Bounded_String) return Boolean
+ with
+ Global => null;
function "<="
(Left : Bounded_String;
- Right : Bounded_String) return Boolean;
+ Right : Bounded_String) return Boolean
+ with
+ Global => null;
function "<="
(Left : Bounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function "<="
(Left : String;
- Right : Bounded_String) return Boolean;
+ Right : Bounded_String) return Boolean
+ with
+ Global => null;
function ">"
(Left : Bounded_String;
- Right : Bounded_String) return Boolean;
+ Right : Bounded_String) return Boolean
+ with
+ Global => null;
function ">"
(Left : Bounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function ">"
(Left : String;
- Right : Bounded_String) return Boolean;
+ Right : Bounded_String) return Boolean
+ with
+ Global => null;
function ">="
(Left : Bounded_String;
- Right : Bounded_String) return Boolean;
+ Right : Bounded_String) return Boolean
+ with
+ Global => null;
function ">="
(Left : Bounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function ">="
(Left : String;
- Right : Bounded_String) return Boolean;
+ Right : Bounded_String) return Boolean
+ with
+ Global => null;
----------------------
-- Search Functions --
(Source : Bounded_String;
Pattern : String;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Index
(Source : Bounded_String;
Pattern : String;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Index
(Source : Bounded_String;
Set : Maps.Character_Set;
Test : Membership := Inside;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Global => null;
function Index
(Source : Bounded_String;
Pattern : String;
From : Positive;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre =>
+ (if Length (Source) /= 0
+ then From <= Length (Source))
+ and then Pattern'Length /= 0,
+ Global => null;
pragma Ada_05 (Index);
function Index
Pattern : String;
From : Positive;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre =>
+ (if Length (Source) /= 0
+ then From <= Length (Source))
+ and then Pattern'Length /= 0,
+ Global => null;
pragma Ada_05 (Index);
function Index
Set : Maps.Character_Set;
From : Positive;
Test : Membership := Inside;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Pre => (if Length (Source) /= 0 then From <= Length (Source)),
+ Global => null;
pragma Ada_05 (Index);
function Index_Non_Blank
(Source : Bounded_String;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Global => null;
function Index_Non_Blank
(Source : Bounded_String;
From : Positive;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Pre => (if Length (Source) /= 0 then From <= Length (Source)),
+ Global => null;
pragma Ada_05 (Index_Non_Blank);
function Count
(Source : Bounded_String;
Pattern : String;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Count
(Source : Bounded_String;
Pattern : String;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Count
(Source : Bounded_String;
- Set : Maps.Character_Set) return Natural;
+ Set : Maps.Character_Set) return Natural
+ with
+ Global => null;
procedure Find_Token
(Source : Bounded_String;
From : Positive;
Test : Membership;
First : out Positive;
- Last : out Natural);
+ Last : out Natural)
+ with
+ Pre => (if Length (Source) /= 0 then From <= Length (Source)),
+ Global => null;
pragma Ada_2012 (Find_Token);
procedure Find_Token
Set : Maps.Character_Set;
Test : Membership;
First : out Positive;
- Last : out Natural);
+ Last : out Natural)
+ with
+ Global => null;
------------------------------------
-- String Translation Subprograms --
function Translate
(Source : Bounded_String;
- Mapping : Maps.Character_Mapping) return Bounded_String;
+ Mapping : Maps.Character_Mapping) return Bounded_String
+ with
+ Post => Length (Translate'Result) = Length (Source),
+ Global => null;
procedure Translate
(Source : in out Bounded_String;
- Mapping : Maps.Character_Mapping);
+ Mapping : Maps.Character_Mapping)
+ with
+ Post => Length (Source) = Length (Source)'Old,
+ Global => null;
function Translate
(Source : Bounded_String;
- Mapping : Maps.Character_Mapping_Function) return Bounded_String;
+ Mapping : Maps.Character_Mapping_Function) return Bounded_String
+ with
+ Post => Length (Translate'Result) = Length (Source),
+ Global => null;
procedure Translate
(Source : in out Bounded_String;
- Mapping : Maps.Character_Mapping_Function);
+ Mapping : Maps.Character_Mapping_Function)
+ with
+ Post => Length (Source) = Length (Source)'Old,
+ Global => null;
---------------------------------------
-- String Transformation Subprograms --
Low : Positive;
High : Natural;
By : String;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre =>
+ Low - 1 <= Length (Source)
+ and then
+ (if Drop = Error
+ then (if High >= Low
+ then Low - 1
+ <= Max_Length - By'Length
+ - Natural'Max (Length (Source) - High, 0)
+ else Length (Source) <= Max_Length - By'Length)),
+ Contract_Cases =>
+ (High >= Low =>
+ Length (Replace_Slice'Result)
+ = Natural'Min
+ (Max_Length,
+ Low - 1 + By'Length + Natural'Max (Length (Source) - High,
+ 0)),
+ others =>
+ Length (Replace_Slice'Result)
+ = Natural'Min (Max_Length, Length (Source) + By'Length)),
+ Global => null;
procedure Replace_Slice
(Source : in out Bounded_String;
Low : Positive;
High : Natural;
By : String;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre =>
+ Low - 1 <= Length (Source)
+ and then
+ (if Drop = Error
+ then (if High >= Low
+ then Low - 1
+ <= Max_Length - By'Length
+ - Natural'Max (Length (Source) - High, 0)
+ else Length (Source) <= Max_Length - By'Length)),
+ Contract_Cases =>
+ (High >= Low =>
+ Length (Source)
+ = Natural'Min
+ (Max_Length,
+ Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High,
+ 0)),
+ others =>
+ Length (Source)
+ = Natural'Min (Max_Length, Length (Source)'Old + By'Length)),
+ Global => null;
function Insert
(Source : Bounded_String;
Before : Positive;
New_Item : String;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre =>
+ Before - 1 <= Length (Source)
+ and then (if New_Item'Length > Max_Length - Length (Source)
+ then Drop /= Error),
+ Post =>
+ Length (Insert'Result)
+ = Natural'Min (Max_Length, Length (Source) + New_Item'Length),
+ Global => null;
procedure Insert
(Source : in out Bounded_String;
Before : Positive;
New_Item : String;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre =>
+ Before - 1 <= Length (Source)
+ and then (if New_Item'Length > Max_Length - Length (Source)
+ then Drop /= Error),
+ Post =>
+ Length (Source)
+ = Natural'Min (Max_Length, Length (Source)'Old + New_Item'Length),
+ Global => null;
function Overwrite
(Source : Bounded_String;
Position : Positive;
New_Item : String;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre =>
+ Position - 1 <= Length (Source)
+ and then (if New_Item'Length > Max_Length - (Position - 1)
+ then Drop /= Error),
+ Post =>
+ Length (Overwrite'Result)
+ = Natural'Max
+ (Length (Source),
+ Natural'Min (Max_Length, Position - 1 + New_Item'Length)),
+ Global => null;
procedure Overwrite
(Source : in out Bounded_String;
Position : Positive;
New_Item : String;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre =>
+ Position - 1 <= Length (Source)
+ and then (if New_Item'Length > Max_Length - (Position - 1)
+ then Drop /= Error),
+ Post =>
+ Length (Source)
+ = Natural'Max
+ (Length (Source)'Old,
+ Natural'Min (Max_Length, Position - 1 + New_Item'Length)),
+ Global => null;
function Delete
(Source : Bounded_String;
From : Positive;
- Through : Natural) return Bounded_String;
+ Through : Natural) return Bounded_String
+ with
+ Pre =>
+ (if Through <= From then From - 1 <= Length (Source)),
+ Contract_Cases =>
+ (Through >= From =>
+ Length (Delete'Result) = Length (Source) - (Through - From + 1),
+ others =>
+ Length (Delete'Result) = Length (Source)),
+
+ Global => null;
procedure Delete
(Source : in out Bounded_String;
From : Positive;
- Through : Natural);
+ Through : Natural)
+ with
+ Pre =>
+ (if Through <= From then From - 1 <= Length (Source)),
+ Contract_Cases =>
+ (Through >= From =>
+ Length (Source) = Length (Source)'Old - (Through - From + 1),
+ others =>
+ Length (Source) = Length (Source)'Old),
+ Global => null;
---------------------------------
-- String Selector Subprograms --
function Trim
(Source : Bounded_String;
- Side : Trim_End) return Bounded_String;
+ Side : Trim_End) return Bounded_String
+ with
+ Post => Length (Trim'Result) <= Length (Source),
+ Global => null;
procedure Trim
(Source : in out Bounded_String;
- Side : Trim_End);
+ Side : Trim_End)
+ with
+ Post => Length (Source) <= Length (Source)'Old,
+ Global => null;
function Trim
(Source : Bounded_String;
Left : Maps.Character_Set;
- Right : Maps.Character_Set) return Bounded_String;
+ Right : Maps.Character_Set) return Bounded_String
+ with
+ Post => Length (Trim'Result) <= Length (Source),
+ Global => null;
procedure Trim
(Source : in out Bounded_String;
Left : Maps.Character_Set;
- Right : Maps.Character_Set);
+ Right : Maps.Character_Set)
+ with
+ Post => Length (Source) <= Length (Source)'Old,
+ Global => null;
function Head
(Source : Bounded_String;
Count : Natural;
Pad : Character := Space;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre => (if Count > Max_Length then Drop /= Error),
+ Post => Length (Head'Result) = Natural'Min (Max_Length, Count),
+ Global => null;
procedure Head
(Source : in out Bounded_String;
Count : Natural;
Pad : Character := Space;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre => (if Count > Max_Length then Drop /= Error),
+ Post => Length (Source) = Natural'Min (Max_Length, Count),
+ Global => null;
function Tail
(Source : Bounded_String;
Count : Natural;
Pad : Character := Space;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre => (if Count > Max_Length then Drop /= Error),
+ Post => Length (Tail'Result) = Natural'Min (Max_Length, Count),
+ Global => null;
procedure Tail
(Source : in out Bounded_String;
Count : Natural;
Pad : Character := Space;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre => (if Count > Max_Length then Drop /= Error),
+ Post => Length (Source) = Natural'Min (Max_Length, Count),
+ Global => null;
------------------------------------
-- String Constructor Subprograms --
function "*"
(Left : Natural;
- Right : Character) return Bounded_String;
+ Right : Character) return Bounded_String
+ with
+ Pre => Left <= Max_Length,
+ Post => Length ("*"'Result) = Left,
+ Global => null;
function "*"
(Left : Natural;
- Right : String) return Bounded_String;
+ Right : String) return Bounded_String
+ with
+ Pre => (if Left /= 0 then Right'Length <= Max_Length / Left),
+ Post => Length ("*"'Result) = Left * Right'Length,
+ Global => null;
function "*"
(Left : Natural;
- Right : Bounded_String) return Bounded_String;
+ Right : Bounded_String) return Bounded_String
+ with
+ Pre => (if Left /= 0 then Length (Right) <= Max_Length / Left),
+ Post => Length ("*"'Result) = Left * Length (Right),
+ Global => null;
function Replicate
(Count : Natural;
Item : Character;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre => (if Count > Max_Length then Drop /= Error),
+ Post =>
+ Length (Replicate'Result)
+ = Natural'Min (Max_Length, Count),
+ Global => null;
function Replicate
(Count : Natural;
Item : String;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre =>
+ (if Item'Length /= 0
+ and then Count > Max_Length / Item'Length
+ then Drop /= Error),
+ Post =>
+ Length (Replicate'Result)
+ = Natural'Min (Max_Length, Count * Item'Length),
+ Global => null;
function Replicate
(Count : Natural;
Item : Bounded_String;
- Drop : Truncation := Error) return Bounded_String;
+ Drop : Truncation := Error) return Bounded_String
+ with
+ Pre =>
+ (if Length (Item) /= 0
+ and then Count > Max_Length / Length (Item)
+ then Drop /= Error),
+ Post =>
+ Length (Replicate'Result)
+ = Natural'Min (Max_Length, Count * Length (Item)),
+ Global => null;
private
-- Most of the implementation is in the separate non generic package
-- --
------------------------------------------------------------------------------
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore.
+
+pragma Assertion_Policy (Pre => Ignore);
+
with Ada.Strings.Maps;
-- The language-defined package Strings.Fixed provides string-handling
-- these effects. Similar control is provided by the string transformation
-- procedures.
-package Ada.Strings.Fixed is
+package Ada.Strings.Fixed with SPARK_Mode is
pragma Preelaborate;
--------------------------------------------------------------
Target : out String;
Drop : Truncation := Error;
Justify : Alignment := Left;
- Pad : Character := Space);
+ Pad : Character := Space)
+ with
+
+ -- Incomplete contract
+
+ Global => null;
-- The Move procedure copies characters from Source to Target. If Source
-- has the same length as Target, then the effect is to assign Source to
-- Target. If Source is shorter than Target then:
Pattern : String;
From : Positive;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre =>
+ Pattern'Length /= 0
+ and then (if Source'Length /= 0 then From in Source'Range),
+ Global => null;
pragma Ada_05 (Index);
function Index
Pattern : String;
From : Positive;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre =>
+ Pattern'Length /= 0
+ and then (if Source'Length /= 0 then From in Source'Range),
+ Global => null;
pragma Ada_05 (Index);
-- Each Index function searches, starting from From, for a slice of
(Source : String;
Pattern : String;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre => Pattern'Length > 0,
+ Global => null;
function Index
(Source : String;
Pattern : String;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
-- If Going = Forward, returns:
--
(Source : String;
Set : Maps.Character_Set;
Test : Membership := Inside;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Global => null;
function Index
(Source : String;
Set : Maps.Character_Set;
From : Positive;
Test : Membership := Inside;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Pre => (if Source'Length /= 0 then From in Source'Range),
+ Global => null;
pragma Ada_05 (Index);
-- Index searches for the first or last occurrence of any of a set of
-- characters (when Test=Inside), or any of the complement of a set of
function Index_Non_Blank
(Source : String;
From : Positive;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Pre => (if Source'Length /= 0 then From in Source'Range),
+ Global => null;
pragma Ada_05 (Index_Non_Blank);
-- Returns Index (Source, Maps.To_Set(Space), From, Outside, Going)
function Index_Non_Blank
(Source : String;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Global => null;
-- Returns Index (Source, Maps.To_Set(Space), Outside, Going)
function Count
(Source : String;
Pattern : String;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Count
(Source : String;
Pattern : String;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
-- Returns the maximum number of nonoverlapping slices of Source that match
-- Pattern with respect to Mapping. If Pattern is the null string then
function Count
(Source : String;
- Set : Maps.Character_Set) return Natural;
+ Set : Maps.Character_Set) return Natural
+ with
+ Global => null;
-- Returns the number of occurrences in Source of characters that are in
-- Set.
From : Positive;
Test : Membership;
First : out Positive;
- Last : out Natural);
+ Last : out Natural)
+ with
+ Pre => (if Source'Length /= 0 then From in Source'Range),
+ Global => null;
pragma Ada_2012 (Find_Token);
-- If Source is not the null string and From is not in Source'Range, then
-- Index_Error is raised. Otherwise, First is set to the index of the first
Set : Maps.Character_Set;
Test : Membership;
First : out Positive;
- Last : out Natural);
+ Last : out Natural)
+ with
+ Global => null;
-- Equivalent to Find_Token (Source, Set, Source'First, Test, First, Last)
------------------------------------
function Translate
(Source : String;
- Mapping : Maps.Character_Mapping_Function) return String;
+ Mapping : Maps.Character_Mapping_Function) return String
+ with
+ Post => Translate'Result'Length = Source'Length,
+ Global => null;
function Translate
(Source : String;
- Mapping : Maps.Character_Mapping) return String;
+ Mapping : Maps.Character_Mapping) return String
+ with
+ Post => Translate'Result'Length = Source'Length,
+ Global => null;
-- Returns the string S whose length is Source'Length and such that S (I)
-- is the character to which Mapping maps the corresponding element of
procedure Translate
(Source : in out String;
- Mapping : Maps.Character_Mapping_Function);
+ Mapping : Maps.Character_Mapping_Function)
+ with
+ Global => null;
procedure Translate
(Source : in out String;
- Mapping : Maps.Character_Mapping);
+ Mapping : Maps.Character_Mapping)
+ with
+ Global => null;
-- Equivalent to Source := Translate(Source, Mapping)
By : String;
Drop : Truncation := Error;
Justify : Alignment := Left;
- Pad : Character := Space);
+ Pad : Character := Space)
+ with
+ Pre =>
+
+ -- Incomplete contract
+
+ Low - 1 <= Source'Last
+ and then High >= Source'First - 1,
+ Global => null;
-- If Low > Source'Last+1, or High < Source'First - 1, then Index_Error is
-- propagated. Otherwise:
--
(Source : String;
Low : Positive;
High : Natural;
- By : String) return String;
+ By : String) return String
+ with
+ Pre =>
+ Low - 1 <= Source'Last
+ and then High >= Source'First - 1
+ and then (if High >= Low
+ then Natural'Max (0, Low - Source'First)
+ <= Natural'Last - By'Length
+ - Natural'Max (Source'Last - High, 0)
+ else Source'Length <= Natural'Last - By'Length),
+ Contract_Cases =>
+ (High >= Low =>
+ Replace_Slice'Result'Length
+ = Natural'Max (0, Low - Source'First)
+ + By'Length
+ + Natural'Max (Source'Last - High, 0),
+ others =>
+ Replace_Slice'Result'Length = Source'Length + By'Length),
+ Global => null;
-- Equivalent to:
--
-- Move (Replace_Slice (Source, Low, High, By),
function Insert
(Source : String;
Before : Positive;
- New_Item : String) return String;
+ New_Item : String) return String
+ with
+ Pre =>
+ Before - 1 in Source'First - 1 .. Source'Last
+ and then Source'Length <= Natural'Last - New_Item'Length,
+ Post => Insert'Result'Length = Source'Length + New_Item'Length,
+ Global => null;
-- Propagates Index_Error if Before is not in
-- Source'First .. Source'Last+1; otherwise, returns
-- Source (Source'First .. Before - 1)
(Source : in out String;
Before : Positive;
New_Item : String;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre => Before - 1 in Source'First - 1 .. Source'Last,
+
+ -- Incomplete contract
+
+ Global => null;
-- Equivalent to Move (Insert (Source, Before, New_Item), Source, Drop)
function Overwrite
(Source : String;
Position : Positive;
- New_Item : String) return String;
+ New_Item : String) return String
+ with
+ Pre =>
+ Position - 1 in Source'First - 1 .. Source'Last
+ and then
+ (if Position - Source'First >= Source'Length - New_Item'Length
+ then Position - Source'First <= Natural'Last - New_Item'Length),
+ Post =>
+ Overwrite'Result'Length
+ = Integer'Max (Source'Length,
+ Position - Source'First + New_Item'Length),
+ Global => null;
-- Propagates Index_Error if Position is not in
-- Source'First .. Source'Last + 1; otherwise, returns the string obtained
-- from Source by consecutively replacing characters starting at Position
(Source : in out String;
Position : Positive;
New_Item : String;
- Drop : Truncation := Right);
+ Drop : Truncation := Right)
+ with
+ Pre => Position - 1 in Source'First - 1 .. Source'Last,
+
+ -- Incomplete contract
+
+ Global => null;
-- Equivalent to Move(Overwrite(Source, Position, New_Item), Source, Drop)
function Delete
(Source : String;
From : Positive;
- Through : Natural) return String;
+ Through : Natural) return String
+ with
+ Pre => (if From <= Through
+ then (From in Source'Range
+ and then Through <= Source'Last)),
+ Post =>
+ Delete'Result'Length
+ = Source'Length - (if From <= Through
+ then Through - From + 1
+ else 0),
+ Global => null;
-- If From <= Through, the returned string is
-- Replace_Slice(Source, From, Through, ""); otherwise, it is Source with
-- lower bound 1.
From : Positive;
Through : Natural;
Justify : Alignment := Left;
- Pad : Character := Space);
+ Pad : Character := Space)
+ with
+ Pre => (if From <= Through
+ then (From in Source'Range
+ and then Through <= Source'Last)),
+
+ -- Incomplete contract
+
+ Global => null;
-- Equivalent to:
--
-- Move (Delete (Source, From, Through),
function Trim
(Source : String;
- Side : Trim_End) return String;
+ Side : Trim_End) return String
+ with
+ Post => Trim'Result'Length <= Source'Length,
+ Global => null;
-- Returns the string obtained by removing from Source all leading Space
-- characters (if Side = Left), all trailing Space characters (if
-- Side = Right), or all leading and trailing Space characters (if
(Source : in out String;
Side : Trim_End;
Justify : Alignment := Left;
- Pad : Character := Space);
+ Pad : Character := Space)
+ with
+
+ -- Incomplete contract
+
+ Global => null;
-- Equivalent to:
--
-- Move (Trim (Source, Side), Source, Justify=>Justify, Pad=>Pad).
function Trim
(Source : String;
Left : Maps.Character_Set;
- Right : Maps.Character_Set) return String;
+ Right : Maps.Character_Set) return String
+ with
+ Post => Trim'Result'Length <= Source'Length,
+ Global => null;
-- Returns the string obtained by removing from Source all leading
-- characters in Left and all trailing characters in Right.
Left : Maps.Character_Set;
Right : Maps.Character_Set;
Justify : Alignment := Strings.Left;
- Pad : Character := Space);
+ Pad : Character := Space)
+ with
+
+ -- Incomplete contract
+
+ Global => null;
-- Equivalent to:
--
-- Move (Trim (Source, Left, Right),
function Head
(Source : String;
Count : Natural;
- Pad : Character := Space) return String;
+ Pad : Character := Space) return String
+ with
+ Post => Head'Result'Length = Count,
+ Global => null;
-- Returns a string of length Count. If Count <= Source'Length, the string
-- comprises the first Count characters of Source. Otherwise, its contents
-- are Source concatenated with Count - Source'Length Pad characters.
(Source : in out String;
Count : Natural;
Justify : Alignment := Left;
- Pad : Character := Space);
+ Pad : Character := Space)
+ with
+
+ -- Incomplete contract
+
+ Global => null;
-- Equivalent to:
--
-- Move (Head (Source, Count, Pad),
function Tail
(Source : String;
Count : Natural;
- Pad : Character := Space) return String;
+ Pad : Character := Space) return String
+ with
+ Post => Tail'Result'Length = Count,
+ Global => null;
-- Returns a string of length Count. If Count <= Source'Length, the string
-- comprises the last Count characters of Source. Otherwise, its contents
-- are Count-Source'Length Pad characters concatenated with Source.
(Source : in out String;
Count : Natural;
Justify : Alignment := Left;
- Pad : Character := Space);
+ Pad : Character := Space)
+ with
+
+ -- Incomplete contract
+
+ Global => null;
-- Equivalent to:
--
-- Move (Tail (Source, Count, Pad),
function "*"
(Left : Natural;
- Right : Character) return String;
+ Right : Character) return String
+ with
+ Post => "*"'Result'Length = Left,
+ Global => null;
function "*"
(Left : Natural;
- Right : String) return String;
+ Right : String) return String
+ with
+ Pre => (if Right'Length /= 0 then Left <= Natural'Last / Right'Length),
+ Post => "*"'Result'Length = Left * Right'Length,
+ Global => null;
-- These functions replicate a character or string a specified number of
-- times. The first function returns a string whose length is Left and each
-- --
------------------------------------------------------------------------------
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore.
+
+pragma Assertion_Policy (Pre => Ignore);
+
with Ada.Strings.Maps;
with Ada.Finalization;
-- length. Since the Unbounded_String type is private, relevant constructor
-- and selector operations are provided.
-package Ada.Strings.Unbounded is
+package Ada.Strings.Unbounded with
+ Initial_Condition => Length (Null_Unbounded_String) = 0
+is
pragma Preelaborate;
type Unbounded_String is private;
-- otherwise initialized, it will be initialized to the same value as
-- Null_Unbounded_String.
- function Length (Source : Unbounded_String) return Natural;
+ function Length (Source : Unbounded_String) return Natural with
+ Global => null;
-- Returns the length of the String represented by Source
type String_Access is access all String;
--------------------------------------------------------
function To_Unbounded_String
- (Source : String) return Unbounded_String;
+ (Source : String) return Unbounded_String
+ with
+ Post => Length (To_Unbounded_String'Result) = Source'Length,
+ Global => null;
-- Returns an Unbounded_String that represents Source
function To_Unbounded_String
- (Length : Natural) return Unbounded_String;
+ (Length : Natural) return Unbounded_String
+ with
+ Post =>
+ Ada.Strings.Unbounded.Length (To_Unbounded_String'Result)
+ = Length,
+ Global => null;
-- Returns an Unbounded_String that represents an uninitialized String
-- whose length is Length.
- function To_String (Source : Unbounded_String) return String;
+ function To_String (Source : Unbounded_String) return String with
+ Post => To_String'Result'Length = Length (Source),
+ Global => null;
-- Returns the String with lower bound 1 represented by Source
-- To_String and To_Unbounded_String are related as follows:
procedure Set_Unbounded_String
(Target : out Unbounded_String;
- Source : String);
+ Source : String)
+ with
+ Global => null;
pragma Ada_05 (Set_Unbounded_String);
-- Sets Target to an Unbounded_String that represents Source
procedure Append
(Source : in out Unbounded_String;
- New_Item : Unbounded_String);
+ New_Item : Unbounded_String)
+ with
+ Pre => Length (New_Item) <= Natural'Last - Length (Source),
+ Post => Length (Source) = Length (Source)'Old + Length (New_Item),
+ Global => null;
procedure Append
(Source : in out Unbounded_String;
- New_Item : String);
+ New_Item : String)
+ with
+ Pre => New_Item'Length <= Natural'Last - Length (Source),
+ Post => Length (Source) = Length (Source)'Old + New_Item'Length,
+ Global => null;
procedure Append
(Source : in out Unbounded_String;
- New_Item : Character);
+ New_Item : Character)
+ with
+ Pre => Length (Source) < Natural'Last,
+ Post => Length (Source) = Length (Source)'Old + 1,
+ Global => null;
-- For each of the Append procedures, the resulting string represented by
-- the Source parameter is given by the concatenation of the original value
function "&"
(Left : Unbounded_String;
- Right : Unbounded_String) return Unbounded_String;
+ Right : Unbounded_String) return Unbounded_String
+ with
+ Pre => Length (Right) <= Natural'Last - Length (Left),
+ Post => Length ("&"'Result) = Length (Left) + Length (Right),
+ Global => null;
function "&"
(Left : Unbounded_String;
- Right : String) return Unbounded_String;
+ Right : String) return Unbounded_String
+ with
+ Pre => Right'Length <= Natural'Last - Length (Left),
+ Post => Length ("&"'Result) = Length (Left) + Right'Length,
+ Global => null;
function "&"
(Left : String;
- Right : Unbounded_String) return Unbounded_String;
+ Right : Unbounded_String) return Unbounded_String
+ with
+ Pre => Left'Length <= Natural'Last - Length (Right),
+ Post => Length ("&"'Result) = Left'Length + Length (Right),
+ Global => null;
function "&"
(Left : Unbounded_String;
- Right : Character) return Unbounded_String;
+ Right : Character) return Unbounded_String
+ with
+ Pre => Length (Left) < Natural'Last,
+ Post => Length ("&"'Result) = Length (Left) + 1,
+ Global => null;
function "&"
(Left : Character;
- Right : Unbounded_String) return Unbounded_String;
+ Right : Unbounded_String) return Unbounded_String
+ with
+ Pre => Length (Right) < Natural'Last,
+ Post => Length ("&"'Result) = Length (Right) + 1,
+ Global => null;
-- Each of the "&" functions returns an Unbounded_String obtained by
-- concatenating the string or character given or represented by one of the
function Element
(Source : Unbounded_String;
- Index : Positive) return Character;
+ Index : Positive) return Character
+ with
+ Pre => Index <= Length (Source),
+ Global => null;
-- Returns the character at position Index in the string represented by
-- Source; propagates Index_Error if Index > Length (Source).
procedure Replace_Element
(Source : in out Unbounded_String;
Index : Positive;
- By : Character);
+ By : Character)
+ with
+ Pre => Index <= Length (Source),
+ Post => Length (Source) = Length (Source)'Old,
+ Global => null;
-- Updates Source such that the character at position Index in the string
-- represented by Source is By; propagates Index_Error if
-- Index > Length (Source).
function Slice
(Source : Unbounded_String;
Low : Positive;
- High : Natural) return String;
+ High : Natural) return String
+ with
+ Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
+ Post => Slice'Result'Length = Natural'Max (0, High - Low + 1),
+ Global => null;
-- Returns the slice at positions Low through High in the string
-- represented by Source; propagates Index_Error if
-- Low > Length (Source) + 1 or High > Length (Source). The bounds of the
function Unbounded_Slice
(Source : Unbounded_String;
Low : Positive;
- High : Natural) return Unbounded_String;
+ High : Natural) return Unbounded_String
+ with
+ Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
+ Post =>
+ Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
+ Global => null;
pragma Ada_05 (Unbounded_Slice);
-- Returns the slice at positions Low through High in the string
-- represented by Source as an Unbounded_String. This propagates
(Source : Unbounded_String;
Target : out Unbounded_String;
Low : Positive;
- High : Natural);
+ High : Natural)
+ with
+ Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
+ Post => Length (Target) = Natural'Max (0, High - Low + 1),
+ Global => null;
pragma Ada_05 (Unbounded_Slice);
-- Sets Target to the Unbounded_String representing the slice at positions
-- Low through High in the string represented by Source. This propagates
function "="
(Left : Unbounded_String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function "="
(Left : Unbounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function "="
(Left : String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function "<"
(Left : Unbounded_String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function "<"
(Left : Unbounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function "<"
(Left : String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function "<="
(Left : Unbounded_String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function "<="
(Left : Unbounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function "<="
(Left : String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function ">"
(Left : Unbounded_String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function ">"
(Left : Unbounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function ">"
(Left : String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function ">="
(Left : Unbounded_String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function ">="
(Left : Unbounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function ">="
(Left : String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
-- Each of the functions "=", "<", ">", "<=", and ">=" returns the same
-- result as the corresponding String operation applied to the String
(Source : Unbounded_String;
Pattern : String;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Index
(Source : Unbounded_String;
Pattern : String;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Index
(Source : Unbounded_String;
Set : Maps.Character_Set;
Test : Membership := Inside;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Global => null;
function Index
(Source : Unbounded_String;
Pattern : String;
From : Positive;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre => (if Length (Source) /= 0 then From <= Length (Source))
+ and then Pattern'Length /= 0,
+ Global => null;
pragma Ada_05 (Index);
function Index
Pattern : String;
From : Positive;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre => (if Length (Source) /= 0 then From <= Length (Source))
+ and then Pattern'Length /= 0,
+ Global => null;
pragma Ada_05 (Index);
function Index
Set : Maps.Character_Set;
From : Positive;
Test : Membership := Inside;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Pre => (if Length (Source) /= 0 then From <= Length (Source)),
+ Global => null;
pragma Ada_05 (Index);
function Index_Non_Blank
(Source : Unbounded_String;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Global => null;
function Index_Non_Blank
(Source : Unbounded_String;
From : Positive;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Pre => (if Length (Source) /= 0 then From <= Length (Source)),
+ Global => null;
pragma Ada_05 (Index_Non_Blank);
function Count
(Source : Unbounded_String;
Pattern : String;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Count
(Source : Unbounded_String;
Pattern : String;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Count
(Source : Unbounded_String;
- Set : Maps.Character_Set) return Natural;
+ Set : Maps.Character_Set) return Natural
+ with
+ Global => null;
procedure Find_Token
(Source : Unbounded_String;
From : Positive;
Test : Membership;
First : out Positive;
- Last : out Natural);
+ Last : out Natural)
+ with
+ Pre => (if Length (Source) /= 0 then From <= Length (Source)),
+ Global => null;
pragma Ada_2012 (Find_Token);
procedure Find_Token
Set : Maps.Character_Set;
Test : Membership;
First : out Positive;
- Last : out Natural);
+ Last : out Natural)
+ with
+ Global => null;
-- Each of the search subprograms (Index, Index_Non_Blank, Count,
-- Find_Token) has the same effect as the corresponding subprogram in
function Translate
(Source : Unbounded_String;
- Mapping : Maps.Character_Mapping) return Unbounded_String;
+ Mapping : Maps.Character_Mapping) return Unbounded_String
+ with
+ Post => Length (Translate'Result) = Length (Source),
+ Global => null;
procedure Translate
(Source : in out Unbounded_String;
- Mapping : Maps.Character_Mapping);
+ Mapping : Maps.Character_Mapping)
+ with
+ Post => Length (Source) = Length (Source)'Old,
+ Global => null;
function Translate
(Source : Unbounded_String;
- Mapping : Maps.Character_Mapping_Function) return Unbounded_String;
+ Mapping : Maps.Character_Mapping_Function) return Unbounded_String
+ with
+ Post => Length (Translate'Result) = Length (Source),
+ Global => null;
procedure Translate
(Source : in out Unbounded_String;
- Mapping : Maps.Character_Mapping_Function);
+ Mapping : Maps.Character_Mapping_Function)
+ with
+ Post => Length (Source) = Length (Source)'Old,
+ Global => null;
-- The Translate function has an analogous effect to the corresponding
-- subprogram in Strings.Fixed. The translation is applied to the string
(Source : Unbounded_String;
Low : Positive;
High : Natural;
- By : String) return Unbounded_String;
+ By : String) return Unbounded_String
+ with
+ Pre =>
+ Low - 1 <= Length (Source)
+ and then (if High >= Low
+ then Low - 1
+ <= Natural'Last - By'Length
+ - Natural'Max (Length (Source) - High, 0)
+ else Length (Source) <= Natural'Last - By'Length),
+ Contract_Cases =>
+ (High >= Low =>
+ Length (Replace_Slice'Result)
+ = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+ others =>
+ Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
+ Global => null;
procedure Replace_Slice
(Source : in out Unbounded_String;
Low : Positive;
High : Natural;
- By : String);
+ By : String)
+ with
+ Pre =>
+ Low - 1 <= Length (Source)
+ and then (if High >= Low
+ then Low - 1
+ <= Natural'Last - By'Length
+ - Natural'Max (Length (Source) - High, 0)
+ else Length (Source) <= Natural'Last - By'Length),
+ Contract_Cases =>
+ (High >= Low =>
+ Length (Source)
+ = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+ others =>
+ Length (Source) = Length (Source)'Old + By'Length),
+ Global => null;
function Insert
(Source : Unbounded_String;
Before : Positive;
- New_Item : String) return Unbounded_String;
+ New_Item : String) return Unbounded_String
+ with
+ Pre => Before - 1 <= Length (Source)
+ and then New_Item'Length <= Natural'Last - Length (Source),
+ Post => Length (Insert'Result) = Length (Source) + New_Item'Length,
+ Global => null;
procedure Insert
(Source : in out Unbounded_String;
Before : Positive;
- New_Item : String);
+ New_Item : String)
+ with
+ Pre => Before - 1 <= Length (Source)
+ and then New_Item'Length <= Natural'Last - Length (Source),
+ Post => Length (Source) = Length (Source)'Old + New_Item'Length,
+ Global => null;
function Overwrite
(Source : Unbounded_String;
Position : Positive;
- New_Item : String) return Unbounded_String;
+ New_Item : String) return Unbounded_String
+ with
+ Pre => Position - 1 <= Length (Source)
+ and then (if New_Item'Length /= 0
+ then
+ New_Item'Length <= Natural'Last - (Position - 1)),
+ Post =>
+ Length (Overwrite'Result)
+ = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
+ Global => null;
procedure Overwrite
(Source : in out Unbounded_String;
Position : Positive;
- New_Item : String);
+ New_Item : String)
+ with
+ Pre => Position - 1 <= Length (Source)
+ and then (if New_Item'Length /= 0
+ then
+ New_Item'Length <= Natural'Last - (Position - 1)),
+ Post =>
+ Length (Source)
+ = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
+
+ Global => null;
function Delete
(Source : Unbounded_String;
From : Positive;
- Through : Natural) return Unbounded_String;
+ Through : Natural) return Unbounded_String
+ with
+ Pre => (if Through <= From then From - 1 <= Length (Source)),
+ Contract_Cases =>
+ (Through >= From =>
+ Length (Delete'Result) = Length (Source) - (Through - From + 1),
+ others =>
+ Length (Delete'Result) = Length (Source)),
+ Global => null;
procedure Delete
(Source : in out Unbounded_String;
From : Positive;
- Through : Natural);
+ Through : Natural)
+ with
+ Pre => (if Through <= From then From - 1 <= Length (Source)),
+ Contract_Cases =>
+ (Through >= From =>
+ Length (Source) = Length (Source)'Old - (Through - From + 1),
+ others =>
+ Length (Source) = Length (Source)'Old),
+ Global => null;
function Trim
(Source : Unbounded_String;
- Side : Trim_End) return Unbounded_String;
+ Side : Trim_End) return Unbounded_String
+ with
+ Post => Length (Trim'Result) <= Length (Source),
+ Global => null;
procedure Trim
(Source : in out Unbounded_String;
- Side : Trim_End);
+ Side : Trim_End)
+ with
+ Post => Length (Source) <= Length (Source)'Old,
+ Global => null;
function Trim
(Source : Unbounded_String;
Left : Maps.Character_Set;
- Right : Maps.Character_Set) return Unbounded_String;
+ Right : Maps.Character_Set) return Unbounded_String
+ with
+ Post => Length (Trim'Result) <= Length (Source),
+ Global => null;
procedure Trim
(Source : in out Unbounded_String;
Left : Maps.Character_Set;
- Right : Maps.Character_Set);
+ Right : Maps.Character_Set)
+ with
+ Post => Length (Source) <= Length (Source)'Old,
+ Global => null;
function Head
(Source : Unbounded_String;
Count : Natural;
- Pad : Character := Space) return Unbounded_String;
+ Pad : Character := Space) return Unbounded_String
+ with
+ Post => Length (Head'Result) = Count,
+ Global => null;
procedure Head
(Source : in out Unbounded_String;
Count : Natural;
- Pad : Character := Space);
+ Pad : Character := Space)
+ with
+ Post => Length (Source) = Count,
+ Global => null;
function Tail
(Source : Unbounded_String;
Count : Natural;
- Pad : Character := Space) return Unbounded_String;
+ Pad : Character := Space) return Unbounded_String
+ with
+ Post => Length (Tail'Result) = Count,
+ Global => null;
procedure Tail
(Source : in out Unbounded_String;
Count : Natural;
- Pad : Character := Space);
+ Pad : Character := Space)
+ with
+ Post => Length (Source) = Count,
+ Global => null;
function "*"
(Left : Natural;
- Right : Character) return Unbounded_String;
+ Right : Character) return Unbounded_String
+ with
+ Pre => Left <= Natural'Last,
+ Post => Length ("*"'Result) = Left,
+ Global => null;
function "*"
(Left : Natural;
- Right : String) return Unbounded_String;
+ Right : String) return Unbounded_String
+ with
+ Pre => (if Left /= 0 then Right'Length <= Natural'Last / Left),
+ Post => Length ("*"'Result) = Left * Right'Length,
+ Global => null;
function "*"
(Left : Natural;
- Right : Unbounded_String) return Unbounded_String;
+ Right : Unbounded_String) return Unbounded_String
+ with
+ Pre => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
+ Post => Length ("*"'Result) = Left * Length (Right),
+ Global => null;
-- Each of the transformation functions (Replace_Slice, Insert, Overwrite,
-- Delete), selector functions (Trim, Head, Tail), and constructor
-- --
------------------------------------------------------------------------------
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore.
+
+pragma Assertion_Policy (Pre => Ignore);
+
-- This package provides an implementation of Ada.Strings.Unbounded that uses
-- reference counts to implement copy on modification (rather than copy on
-- assignment). This is significantly more efficient on many targets.
private with Ada.Finalization;
private with System.Atomic_Counters;
-package Ada.Strings.Unbounded is
+package Ada.Strings.Unbounded with
+ Initial_Condition => Length (Null_Unbounded_String) = 0
+is
pragma Preelaborate;
type Unbounded_String is private;
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;
--------------------------------------------------------
function To_Unbounded_String
- (Source : String) return Unbounded_String;
+ (Source : String) return Unbounded_String
+ with
+ Post => Length (To_Unbounded_String'Result) = Source'Length,
+ Global => null;
function To_Unbounded_String
- (Length : Natural) return Unbounded_String;
+ (Length : Natural) return Unbounded_String
+ with
+ Post =>
+ Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length,
+ Global => null;
- function To_String (Source : Unbounded_String) return String;
+ function To_String (Source : Unbounded_String) return String with
+ Post => To_String'Result'Length = Length (Source),
+ Global => null;
procedure Set_Unbounded_String
(Target : out Unbounded_String;
- Source : String);
+ Source : String)
+ with
+ Global => null;
pragma Ada_05 (Set_Unbounded_String);
procedure Append
(Source : in out Unbounded_String;
- New_Item : Unbounded_String);
+ New_Item : Unbounded_String)
+ with
+ Pre => Length (New_Item) <= Natural'Last - Length (Source),
+ Post => Length (Source) = Length (Source)'Old + Length (New_Item),
+ Global => null;
procedure Append
(Source : in out Unbounded_String;
- New_Item : String);
+ New_Item : String)
+ with
+ Pre => New_Item'Length <= Natural'Last - Length (Source),
+ Post => Length (Source) = Length (Source)'Old + New_Item'Length,
+ Global => null;
procedure Append
(Source : in out Unbounded_String;
- New_Item : Character);
+ New_Item : Character)
+ with
+ Pre => Length (Source) < Natural'Last,
+ Post => Length (Source) = Length (Source)'Old + 1,
+ Global => null;
function "&"
(Left : Unbounded_String;
- Right : Unbounded_String) return Unbounded_String;
+ Right : Unbounded_String) return Unbounded_String
+ with
+ Pre => Length (Right) <= Natural'Last - Length (Left),
+ Post => Length ("&"'Result) = Length (Left) + Length (Right),
+ Global => null;
function "&"
(Left : Unbounded_String;
- Right : String) return Unbounded_String;
+ Right : String) return Unbounded_String
+ with
+ Pre => Right'Length <= Natural'Last - Length (Left),
+ Post => Length ("&"'Result) = Length (Left) + Right'Length,
+ Global => null;
function "&"
(Left : String;
- Right : Unbounded_String) return Unbounded_String;
+ Right : Unbounded_String) return Unbounded_String
+ with
+ Pre => Left'Length <= Natural'Last - Length (Right),
+ Post => Length ("&"'Result) = Left'Length + Length (Right),
+ Global => null;
function "&"
(Left : Unbounded_String;
- Right : Character) return Unbounded_String;
+ Right : Character) return Unbounded_String
+ with
+ Pre => Length (Left) < Natural'Last,
+ Post => Length ("&"'Result) = Length (Left) + 1,
+ Global => null;
function "&"
(Left : Character;
- Right : Unbounded_String) return Unbounded_String;
+ Right : Unbounded_String) return Unbounded_String
+ with
+ Pre => Length (Right) < Natural'Last,
+ Post => Length ("&"'Result) = Length (Right) + 1,
+ Global => null;
function Element
(Source : Unbounded_String;
- Index : Positive) return Character;
+ Index : Positive) return Character
+ with
+ Pre => Index <= Length (Source),
+ Global => null;
procedure Replace_Element
(Source : in out Unbounded_String;
Index : Positive;
- By : Character);
+ By : Character)
+ with
+ Pre => Index <= Length (Source),
+ Post => Length (Source) = Length (Source)'Old,
+ Global => null;
function Slice
(Source : Unbounded_String;
Low : Positive;
- High : Natural) return String;
+ High : Natural) return String
+ with
+ Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
+ Post => Slice'Result'Length = Natural'Max (0, High - Low + 1),
+ Global => null;
function Unbounded_Slice
(Source : Unbounded_String;
Low : Positive;
- High : Natural) return Unbounded_String;
+ High : Natural) return Unbounded_String
+ with
+ Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
+ Post =>
+ Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
+ Global => null;
pragma Ada_05 (Unbounded_Slice);
procedure Unbounded_Slice
(Source : Unbounded_String;
Target : out Unbounded_String;
Low : Positive;
- High : Natural);
+ High : Natural)
+ with
+ Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
+ Post => Length (Target) = Natural'Max (0, High - Low + 1),
+ Global => null;
pragma Ada_05 (Unbounded_Slice);
function "="
(Left : Unbounded_String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function "="
(Left : Unbounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function "="
(Left : String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function "<"
(Left : Unbounded_String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function "<"
(Left : Unbounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function "<"
(Left : String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function "<="
(Left : Unbounded_String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function "<="
(Left : Unbounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function "<="
(Left : String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function ">"
(Left : Unbounded_String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function ">"
(Left : Unbounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function ">"
(Left : String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function ">="
(Left : Unbounded_String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
function ">="
(Left : Unbounded_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Global => null;
function ">="
(Left : String;
- Right : Unbounded_String) return Boolean;
+ Right : Unbounded_String) return Boolean
+ with
+ Global => null;
------------------------
-- Search Subprograms --
(Source : Unbounded_String;
Pattern : String;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Index
(Source : Unbounded_String;
Pattern : String;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Index
(Source : Unbounded_String;
Set : Maps.Character_Set;
Test : Membership := Inside;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Global => null;
function Index
(Source : Unbounded_String;
Pattern : String;
From : Positive;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre => (if Length (Source) /= 0
+ then From <= Length (Source))
+ and then Pattern'Length /= 0,
+ Global => null;
pragma Ada_05 (Index);
function Index
Pattern : String;
From : Positive;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre => (if Length (Source) /= 0
+ then From <= Length (Source))
+ and then Pattern'Length /= 0,
+ Global => null;
+
pragma Ada_05 (Index);
function Index
Set : Maps.Character_Set;
From : Positive;
Test : Membership := Inside;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Pre => (if Length (Source) /= 0 then From <= Length (Source)),
+ Global => null;
pragma Ada_05 (Index);
function Index_Non_Blank
(Source : Unbounded_String;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Global => null;
function Index_Non_Blank
(Source : Unbounded_String;
From : Positive;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Pre => (if Length (Source) /= 0 then From <= Length (Source)),
+ Global => null;
pragma Ada_05 (Index_Non_Blank);
function Count
(Source : Unbounded_String;
Pattern : String;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Count
(Source : Unbounded_String;
Pattern : String;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Count
(Source : Unbounded_String;
- Set : Maps.Character_Set) return Natural;
+ Set : Maps.Character_Set) return Natural
+ with
+ Global => null;
procedure Find_Token
(Source : Unbounded_String;
From : Positive;
Test : Membership;
First : out Positive;
- Last : out Natural);
+ Last : out Natural)
+ with
+ Pre => (if Length (Source) /= 0 then From <= Length (Source)),
+ Global => null;
pragma Ada_2012 (Find_Token);
procedure Find_Token
Set : Maps.Character_Set;
Test : Membership;
First : out Positive;
- Last : out Natural);
+ Last : out Natural)
+ with
+ Global => null;
------------------------------------
-- String Translation Subprograms --
function Translate
(Source : Unbounded_String;
- Mapping : Maps.Character_Mapping) return Unbounded_String;
+ Mapping : Maps.Character_Mapping) return Unbounded_String
+ with
+ Post => Length (Translate'Result) = Length (Source),
+ Global => null;
procedure Translate
(Source : in out Unbounded_String;
- Mapping : Maps.Character_Mapping);
+ Mapping : Maps.Character_Mapping)
+ with
+ Post => Length (Source) = Length (Source)'Old,
+ Global => null;
function Translate
(Source : Unbounded_String;
- Mapping : Maps.Character_Mapping_Function) return Unbounded_String;
+ Mapping : Maps.Character_Mapping_Function) return Unbounded_String
+ with
+ Post => Length (Translate'Result) = Length (Source),
+ Global => null;
procedure Translate
(Source : in out Unbounded_String;
- Mapping : Maps.Character_Mapping_Function);
+ Mapping : Maps.Character_Mapping_Function)
+ with
+ Post => Length (Source) = Length (Source)'Old,
+ Global => null;
---------------------------------------
-- String Transformation Subprograms --
(Source : Unbounded_String;
Low : Positive;
High : Natural;
- By : String) return Unbounded_String;
+ By : String) return Unbounded_String
+ with
+ Pre =>
+ Low - 1 <= Length (Source)
+ and then (if High >= Low
+ then Low - 1
+ <= Natural'Last - By'Length
+ - Natural'Max (Length (Source) - High, 0)
+ else Length (Source) <= Natural'Last - By'Length),
+ Contract_Cases =>
+ (High >= Low =>
+ Length (Replace_Slice'Result)
+ = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+ others =>
+ Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
+ Global => null;
procedure Replace_Slice
(Source : in out Unbounded_String;
Low : Positive;
High : Natural;
- By : String);
+ By : String)
+ with
+ Pre =>
+ Low - 1 <= Length (Source)
+ and then (if High >= Low
+ then Low - 1
+ <= Natural'Last - By'Length
+ - Natural'Max (Length (Source) - High, 0)
+ else Length (Source) <= Natural'Last - By'Length),
+ Contract_Cases =>
+ (High >= Low =>
+ Length (Source)
+ = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+ others =>
+ Length (Source) = Length (Source)'Old + By'Length),
+ Global => null;
function Insert
(Source : Unbounded_String;
Before : Positive;
- New_Item : String) return Unbounded_String;
+ New_Item : String) return Unbounded_String
+ with
+ Pre => Before - 1 <= Length (Source)
+ and then New_Item'Length <= Natural'Last - Length (Source),
+ Post => Length (Insert'Result) = Length (Source) + New_Item'Length,
+ Global => null;
procedure Insert
(Source : in out Unbounded_String;
Before : Positive;
- New_Item : String);
+ New_Item : String)
+ with
+ Pre => Before - 1 <= Length (Source)
+ and then New_Item'Length <= Natural'Last - Length (Source),
+ Post => Length (Source) = Length (Source)'Old + New_Item'Length,
+ Global => null;
function Overwrite
(Source : Unbounded_String;
Position : Positive;
- New_Item : String) return Unbounded_String;
+ New_Item : String) return Unbounded_String
+ with
+ Pre => Position - 1 <= Length (Source)
+ and then (if New_Item'Length /= 0
+ then
+ New_Item'Length <= Natural'Last - (Position - 1)),
+ Post =>
+ Length (Overwrite'Result)
+ = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
+ Global => null;
procedure Overwrite
(Source : in out Unbounded_String;
Position : Positive;
- New_Item : String);
+ New_Item : String)
+ with
+ Pre => Position - 1 <= Length (Source)
+ and then (if New_Item'Length /= 0
+ then
+ New_Item'Length <= Natural'Last - (Position - 1)),
+ Post =>
+ Length (Source)
+ = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
+
+ Global => null;
function Delete
(Source : Unbounded_String;
From : Positive;
- Through : Natural) return Unbounded_String;
+ Through : Natural) return Unbounded_String
+ with
+ Pre => (if Through <= From then From - 1 <= Length (Source)),
+ Contract_Cases =>
+ (Through >= From =>
+ Length (Delete'Result) = Length (Source) - (Through - From + 1),
+ others =>
+ Length (Delete'Result) = Length (Source)),
+ Global => null;
procedure Delete
(Source : in out Unbounded_String;
From : Positive;
- Through : Natural);
+ Through : Natural)
+ with
+ Pre => (if Through <= From then From - 1 <= Length (Source)),
+ Contract_Cases =>
+ (Through >= From =>
+ Length (Source) = Length (Source)'Old - (Through - From + 1),
+ others =>
+ Length (Source) = Length (Source)'Old),
+ Global => null;
function Trim
(Source : Unbounded_String;
- Side : Trim_End) return Unbounded_String;
+ Side : Trim_End) return Unbounded_String
+ with
+ Post => Length (Trim'Result) <= Length (Source),
+ Global => null;
procedure Trim
(Source : in out Unbounded_String;
- Side : Trim_End);
+ Side : Trim_End)
+ with
+ Post => Length (Source) <= Length (Source)'Old,
+ Global => null;
function Trim
(Source : Unbounded_String;
Left : Maps.Character_Set;
- Right : Maps.Character_Set) return Unbounded_String;
+ Right : Maps.Character_Set) return Unbounded_String
+ with
+ Post => Length (Trim'Result) <= Length (Source),
+ Global => null;
procedure Trim
(Source : in out Unbounded_String;
Left : Maps.Character_Set;
- Right : Maps.Character_Set);
+ Right : Maps.Character_Set)
+ with
+ Post => Length (Source) <= Length (Source)'Old,
+ Global => null;
function Head
(Source : Unbounded_String;
Count : Natural;
- Pad : Character := Space) return Unbounded_String;
+ Pad : Character := Space) return Unbounded_String
+ with
+ Post => Length (Head'Result) = Count,
+ Global => null;
procedure Head
(Source : in out Unbounded_String;
Count : Natural;
- Pad : Character := Space);
+ Pad : Character := Space)
+ with
+ Post => Length (Source) = Count,
+ Global => null;
function Tail
(Source : Unbounded_String;
Count : Natural;
- Pad : Character := Space) return Unbounded_String;
+ Pad : Character := Space) return Unbounded_String
+ with
+ Post => Length (Tail'Result) = Count,
+ Global => null;
procedure Tail
(Source : in out Unbounded_String;
Count : Natural;
- Pad : Character := Space);
+ Pad : Character := Space)
+ with
+ Post => Length (Source) = Count,
+ Global => null;
function "*"
(Left : Natural;
- Right : Character) return Unbounded_String;
+ Right : Character) return Unbounded_String
+ with
+ Pre => Left <= Natural'Last,
+ Post => Length ("*"'Result) = Left,
+ Global => null;
function "*"
(Left : Natural;
- Right : String) return Unbounded_String;
+ Right : String) return Unbounded_String
+ with
+ Pre => (if Left /= 0 then Right'Length <= Natural'Last / Left),
+ Post => Length ("*"'Result) = Left * Right'Length,
+ Global => null;
function "*"
(Left : Natural;
- Right : Unbounded_String) return Unbounded_String;
+ Right : Unbounded_String) return Unbounded_String
+ with
+ Pre => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
+ Post => Length ("*"'Result) = Left * Length (Right),
+ Global => null;
private
pragma Inline (Length);
projects / gcc.git / commitdiff