From: Joffrey Huguet <huguet@adacore.com>
Date: Wed, 10 Jul 2019 09:01:28 +0000 (+0000)
Subject: [Ada] Add contracts to Strings libraries
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0b6694b4e41d394df12d159c319be4b1326745ca;p=gcc.git

[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
---

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