[Ada] SPARK proof of the Ada.Strings.Fixed library

gcc/ada/

	* libgnat/a-strfix.adb ("*"): Added loop invariants and lemmas
	for proof.
	(Delete): Added assertions for proof, and conditions to avoid
	overflow.
	(Head): Added loop invariant.
	(Insert): Same as Delete.
	(Move): Declared with SPARK_Mode Off.
	(Overwrite): Added assertions for proof, and conditions to avoid
	overflow.
	(Replace_Slice): Added assertions for proof, and conditions to
	avoid overflow.
	(Tail): Added loop invariant and avoided overflows.
	(Translate): Added loop invariants.
	(Trim): Ensured empty strings returned start at 1.
	* libgnat/a-strfix.ads (Index): Rewrote contract cases for
	easier proof.
	(Index_Non_Blank): Separated the null string case.
	(Count): Specified Mapping shouldn't be null.
	(Find_Token): Specified Source'First should be Positive when no
	From is given.
	(Translate): Specified Mapping shouldn't be null.
	("*"): Rewrote postcondition for easier proof.
	* libgnat/a-strsea.adb (Belongs): Added postcondition.
	(Count): Rewrote loops and added loop invariants to avoid
	overflows.
	(Find_Token): Added loop invariants.
	(Index): Rewrote loops to avoid overflows and added loop
	invariants for proof.
	(Index_Non_Blank): Added loop invariants.
	(Is_Identity): New function isolated without SPARK_Mode.
	* libgnat/a-strsea.ads: Fix starting comment as package is no
	longer private.
	(Match): Declared ghost expression function Match.
	(Is_Identity): Described identity in the postcondition.
	(Index, Index_Non_Blank, Count, Find_Token): Added contract from
	a-strfix.ads.

4 files changed, 1166 insertions, 349 deletions

diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb
index ee72b6b..00967c4 100644
--- a/gcc/ada/libgnat/a-strfix.adb
+++ b/gcc/ada/libgnat/a-strfix.adb
@@ -38,10 +38,17 @@
 --  bounds of function return results were also fixed, and use of & removed for
 --  efficiency reasons.
 
+--  Ghost code, loop invariants and assertions in this unit are meant for
+--  analysis only, not for run-time checking, as it would be too costly
+--  otherwise. This is enforced by setting the assertion policy to Ignore.
+
+pragma Assertion_Policy (Ghost          => Ignore,
+                         Loop_Invariant => Ignore,
+                         Assert         => Ignore);
+
 with Ada.Strings.Maps; use Ada.Strings.Maps;
-with Ada.Strings.Search;
 
-package body Ada.Strings.Fixed is
+package body Ada.Strings.Fixed with SPARK_Mode is
 
    ------------------------
    -- Search Subprograms --
@@ -146,9 +153,12 @@ package body Ada.Strings.Fixed is
       Right : Character) return String
    is
    begin
-      return Result : String (1 .. Left) do
+      return Result : String (1 .. Left) with Relaxed_Initialization do
          for J in Result'Range loop
             Result (J) := Right;
+            pragma Loop_Invariant
+              (for all K in 1 .. J =>
+                 Result (K)'Initialized and then Result (K) = Right);
          end loop;
       end return;
    end "*";
@@ -157,12 +167,82 @@ package body Ada.Strings.Fixed is
      (Left  : Natural;
       Right : String) return String
    is
-      Ptr    : Integer := 1;
+      Ptr : Integer := 0;
+
+      --  Parts of the proof involving manipulations with the modulo operator
+      --  are complicated for the prover and can't be done automatically in
+      --  the global subprogram. That's why we isolate them in these two ghost
+      --  lemmas.
+
+      procedure Lemma_Mod (K : Integer) with
+        Ghost,
+        Pre =>
+          Right'Length /= 0
+          and then Ptr mod Right'Length = 0
+          and then Ptr in 0 .. Natural'Last - Right'Length
+          and then K in Ptr .. Ptr + Right'Length - 1,
+        Post => K mod Right'Length = K - Ptr;
+      --  Lemma_Mod is applied to an index considered in Lemma_Split to prove
+      --  that it has the right value modulo Right'Length.
+
+      procedure Lemma_Split (Result : String) with
+        Ghost,
+        Relaxed_Initialization => Result,
+        Pre                    =>
+          Right'Length /= 0
+            and then Result'First = 1
+            and then Result'Last >= 0
+            and then Ptr mod Right'Length = 0
+            and then Ptr in 0 .. Result'Last - Right'Length
+            and then Result (Result'First .. Ptr + Right'Length)'Initialized
+            and then Result (Ptr + 1 .. Ptr + Right'Length) = Right,
+        Post                   =>
+          (for all K in Ptr + 1 .. Ptr + Right'Length =>
+            Result (K) = Right (Right'First + (K - 1) mod Right'Length));
+      --  Lemma_Split is used after Result (Ptr + 1 .. Ptr + Right'Length) is
+      --  updated to Right and concludes that the characters match for each
+      --  index when taken modulo Right'Length, as the considered slice starts
+      --  at index 1 modulo Right'Length.
+
+      ---------------
+      -- Lemma_Mod --
+      ---------------
+
+      procedure Lemma_Mod (K : Integer) is null;
+
+      -----------------
+      -- Lemma_Split --
+      -----------------
+
+      procedure Lemma_Split (Result : String) is
+      begin
+         for K in Ptr + 1 .. Ptr + Right'Length loop
+            Lemma_Mod (K - 1);
+            pragma Loop_Invariant
+              (for all J in Ptr + 1 .. K =>
+                 Result (J) = Right (Right'First + (J - 1) mod Right'Length));
+         end loop;
+      end Lemma_Split;
+
+   --  Start of processing for "*"
+
    begin
-      return Result : String (1 .. Left * Right'Length) do
+      if Right'Length = 0 then
+         return "";
+      end if;
+
+      return Result : String (1 .. Left * Right'Length)
+        with Relaxed_Initialization
+      do
          for J in 1 .. Left loop
-            Result (Ptr .. Ptr + Right'Length - 1) := Right;
+            Result (Ptr + 1 .. Ptr + Right'Length) := Right;
+            Lemma_Split (Result);
             Ptr := Ptr + Right'Length;
+            pragma Loop_Invariant (Ptr = J * Right'Length);
+            pragma Loop_Invariant (Result (1 .. Ptr)'Initialized);
+            pragma Loop_Invariant
+              (for all K in 1 .. Ptr =>
+                 Result (K) = Right (Right'First + (K - 1) mod Right'Length));
          end loop;
       end return;
    end "*";
@@ -176,7 +256,6 @@ package body Ada.Strings.Fixed is
       From    : Positive;
       Through : Natural) return String
    is
-      Front : Integer;
    begin
       if From > Through then
          declare
@@ -204,13 +283,22 @@ package body Ada.Strings.Fixed is
          end if;
 
       else
-         Front := From - Source'First;
-         return Result : String (1 .. Source'Length - (Through - From + 1)) do
-            Result (1 .. Front) :=
-              Source (Source'First .. From - 1);
-            Result (Front + 1 .. Result'Last) :=
-              Source (Through + 1 .. Source'Last);
-         end return;
+         declare
+            Front : constant Integer := From - Source'First;
+
+         begin
+            return Result : String (1 .. Source'Length - (Through - From + 1))
+              with Relaxed_Initialization
+            do
+               Result (1 .. Front) :=
+                 Source (Source'First .. From - 1);
+
+               if Through < Source'Last then
+                  Result (Front + 1 .. Result'Last) :=
+                    Source (Through + 1 .. Source'Last);
+               end if;
+            end return;
+         end;
       end if;
    end Delete;
 
@@ -219,8 +307,7 @@ package body Ada.Strings.Fixed is
       From    : Positive;
       Through : Natural;
       Justify : Alignment := Left;
-      Pad     : Character := Space)
-   is
+      Pad     : Character := Space) with SPARK_Mode => Off is
    begin
       Move (Source  => Delete (Source, From, Through),
             Target  => Source,
@@ -240,16 +327,19 @@ package body Ada.Strings.Fixed is
       subtype Result_Type is String (1 .. Count);
 
    begin
-      if Count < Source'Length then
+      if Count <= Source'Length then
          return
-           Result_Type (Source (Source'First .. Source'First + Count - 1));
+           Result_Type (Source (Source'First .. Source'First + (Count - 1)));
 
       else
-         return Result : Result_Type do
+         return Result : Result_Type with Relaxed_Initialization do
             Result (1 .. Source'Length) := Source;
 
             for J in Source'Length + 1 .. Count loop
                Result (J) := Pad;
+               pragma Loop_Invariant
+                 (for all K in Source'Length + 1 .. J =>
+                    Result (K)'Initialized and then Result (K) = Pad);
             end loop;
          end return;
       end if;
@@ -281,17 +371,31 @@ package body Ada.Strings.Fixed is
       Front  : constant Integer := Before - Source'First;
 
    begin
-      if Before not in Source'First .. Source'Last + 1 then
+      if Before - 1 not in Source'First - 1 .. Source'Last then
          raise Index_Error;
       end if;
 
-      return Result : String (1 .. Source'Length + New_Item'Length) do
+      return Result : String (1 .. Source'Length + New_Item'Length)
+        with Relaxed_Initialization
+      do
          Result (1 .. Front) :=
            Source (Source'First .. Before - 1);
          Result (Front + 1 .. Front + New_Item'Length) :=
            New_Item;
-         Result (Front + New_Item'Length + 1 .. Result'Last) :=
-           Source (Before .. Source'Last);
+         pragma Assert
+           (Result
+              (Before - Source'First + 1
+               .. Before - Source'First + New_Item'Length)
+            = New_Item);
+
+         if Before <= Source'Last then
+            Result (Front + New_Item'Length + 1 .. Result'Last) :=
+              Source (Before .. Source'Last);
+         end if;
+
+         pragma Assert
+           (Result (1 .. Before - Source'First)
+            = Source (Source'First .. Before - 1));
       end return;
    end Insert;
 
@@ -299,8 +403,7 @@ package body Ada.Strings.Fixed is
      (Source   : in out String;
       Before   : Positive;
       New_Item : String;
-      Drop     : Truncation := Error)
-   is
+      Drop     : Truncation := Error) with SPARK_Mode => Off is
    begin
       Move (Source => Insert (Source, Before, New_Item),
             Target => Source,
@@ -316,7 +419,7 @@ package body Ada.Strings.Fixed is
       Target  : out String;
       Drop    : Truncation := Error;
       Justify : Alignment  := Left;
-      Pad     : Character  := Space)
+      Pad     : Character  := Space) with SPARK_Mode => Off
    is
       Sfirst  : constant Integer := Source'First;
       Slast   : constant Integer := Source'Last;
@@ -423,7 +526,7 @@ package body Ada.Strings.Fixed is
       Position : Positive;
       New_Item : String) return String is
    begin
-      if Position not in Source'First .. Source'Last + 1 then
+      if Position - 1 not in Source'First - 1 .. Source'Last then
          raise Index_Error;
       end if;
 
@@ -434,11 +537,32 @@ package body Ada.Strings.Fixed is
          Front         : constant Integer := Position - Source'First;
 
       begin
-         return Result : String (1 .. Result_Length) do
+         return Result : String (1 .. Result_Length)
+           with Relaxed_Initialization
+         do
             Result (1 .. Front) := Source (Source'First .. Position - 1);
+            pragma Assert
+              (Result (1 .. Position - Source'First)
+               = Source (Source'First .. Position - 1));
             Result (Front + 1 .. Front + New_Item'Length) := New_Item;
-            Result (Front + New_Item'Length + 1 .. Result'Length) :=
-              Source (Position + New_Item'Length .. Source'Last);
+            pragma Assert
+              (Result
+                 (Position - Source'First + 1
+                  .. Position - Source'First + New_Item'Length)
+               = New_Item);
+
+            if Position <= Source'Last - New_Item'Length then
+               Result (Front + New_Item'Length + 1 .. Result'Last) :=
+                 Source (Position + New_Item'Length .. Source'Last);
+            end if;
+
+            pragma Assert
+              (if Position <= Source'Last - New_Item'Length
+               then
+                  Result
+                 (Position - Source'First + New_Item'Length + 1
+                  .. Result'Last)
+               = Source (Position + New_Item'Length .. Source'Last));
          end return;
       end;
    end Overwrite;
@@ -447,8 +571,7 @@ package body Ada.Strings.Fixed is
      (Source   : in out String;
       Position : Positive;
       New_Item : String;
-      Drop     : Truncation := Right)
-   is
+      Drop     : Truncation := Right) with SPARK_Mode => Off is
    begin
       Move (Source => Overwrite (Source, Position, New_Item),
             Target => Source,
@@ -463,10 +586,9 @@ package body Ada.Strings.Fixed is
      (Source : String;
       Low    : Positive;
       High   : Natural;
-      By     : String) return String
-   is
+      By     : String) return String is
    begin
-      if Low > Source'Last + 1 or else High < Source'First - 1 then
+      if Low - 1 > Source'Last or else High < Source'First - 1 then
          raise Index_Error;
       end if;
 
@@ -484,11 +606,34 @@ package body Ada.Strings.Fixed is
             --  Length of result
 
          begin
-            return Result : String (1 .. Result_Length) do
+            return Result : String (1 .. Result_Length)
+              with Relaxed_Initialization do
                Result (1 .. Front_Len) := Source (Source'First .. Low - 1);
+               pragma Assert
+                 (Result (1 .. Integer'Max (0, Low - Source'First))
+                  = Source (Source'First .. Low - 1));
                Result (Front_Len + 1 .. Front_Len + By'Length) := By;
-               Result (Front_Len + By'Length + 1 .. Result'Length) :=
-                 Source (High + 1 .. Source'Last);
+
+               if High < Source'Last then
+                  Result (Front_Len + By'Length + 1 .. Result'Last) :=
+                    Source (High + 1 .. Source'Last);
+               end if;
+
+               pragma Assert
+                 (Result (1 .. Integer'Max (0, Low - Source'First))
+                  = Source (Source'First .. Low - 1));
+               pragma Assert
+                 (Result
+                    (Integer'Max (0, Low - Source'First) + 1
+                     .. Integer'Max (0, Low - Source'First) + By'Length)
+                  = By);
+               pragma Assert
+                 (if High < Source'Last
+                  then
+                     Result
+                    (Integer'Max (0, Low - Source'First) + By'Length + 1
+                     .. Result'Last)
+                  = Source (High + 1 .. Source'Last));
             end return;
          end;
       else
@@ -503,8 +648,7 @@ package body Ada.Strings.Fixed is
       By       : String;
       Drop     : Truncation := Error;
       Justify  : Alignment  := Left;
-      Pad      : Character  := Space)
-   is
+      Pad      : Character  := Space) with SPARK_Mode => Off is
    begin
       Move (Replace_Slice (Source, Low, High, By), Source, Drop, Justify, Pad);
    end Replace_Slice;
@@ -521,18 +665,26 @@ package body Ada.Strings.Fixed is
       subtype Result_Type is String (1 .. Count);
 
    begin
-      if Count < Source'Length then
+      if Count = 0 then
+         return "";
+
+      elsif Count < Source'Length then
          return Result_Type (Source (Source'Last - Count + 1 .. Source'Last));
 
       --  Pad on left
 
       else
-         return Result : Result_Type do
+         return Result : Result_Type with Relaxed_Initialization do
             for J in 1 .. Count - Source'Length loop
                Result (J) := Pad;
+               pragma Loop_Invariant
+                 (for all K in 1 .. J =>
+                    Result (K)'Initialized and then Result (K) = Pad);
             end loop;
 
-            Result (Count - Source'Length + 1 .. Count) := Source;
+            if Source'Length /= 0 then
+               Result (Count - Source'Length + 1 .. Count) := Source;
+            end if;
          end return;
       end if;
    end Tail;
@@ -560,9 +712,18 @@ package body Ada.Strings.Fixed is
       Mapping : Maps.Character_Mapping) return String
    is
    begin
-      return Result : String (1 .. Source'Length) do
+      return Result : String (1 .. Source'Length)
+        with Relaxed_Initialization
+      do
          for J in Source'Range loop
             Result (J - (Source'First - 1)) := Value (Mapping, Source (J));
+            pragma Loop_Invariant
+              (for all K in Source'First .. J =>
+                 Result (K - (Source'First - 1))'Initialized);
+            pragma Loop_Invariant
+              (for all K in Source'First .. J =>
+                 Result (K - (Source'First - 1)) =
+                   Value (Mapping, Source (K)));
          end loop;
       end return;
    end Translate;
@@ -574,6 +735,9 @@ package body Ada.Strings.Fixed is
    begin
       for J in Source'Range loop
          Source (J) := Value (Mapping, Source (J));
+         pragma Loop_Invariant
+           (for all K in Source'First .. J =>
+              Source (K) = Value (Mapping, Source'Loop_Entry (K)));
       end loop;
    end Translate;
 
@@ -583,9 +747,17 @@ package body Ada.Strings.Fixed is
    is
       pragma Unsuppress (Access_Check);
    begin
-      return Result : String (1 .. Source'Length) do
+      return Result : String (1 .. Source'Length)
+        with Relaxed_Initialization
+      do
          for J in Source'Range loop
             Result (J - (Source'First - 1)) := Mapping.all (Source (J));
+            pragma Loop_Invariant
+              (for all K in Source'First .. J =>
+                 Result (K - (Source'First - 1))'Initialized);
+            pragma Loop_Invariant
+              (for all K in Source'First .. J =>
+                 Result (K - (Source'First - 1)) = Mapping (Source (K)));
          end loop;
       end return;
    end Translate;
@@ -598,6 +770,9 @@ package body Ada.Strings.Fixed is
    begin
       for J in Source'Range loop
          Source (J) := Mapping.all (Source (J));
+         pragma Loop_Invariant
+           (for all K in Source'First .. J =>
+              Source (K) = Mapping (Source'Loop_Entry (K)));
       end loop;
    end Translate;
 
@@ -609,6 +784,9 @@ package body Ada.Strings.Fixed is
      (Source : String;
       Side   : Trim_End) return String
    is
+      Empty_String : constant String (1 .. 0) := "";
+      --  Without declaring the empty string as a separate string starting
+      --  at 1, SPARK provers have trouble proving the postcondition.
    begin
       case Side is
          when Strings.Left =>
@@ -618,7 +796,7 @@ package body Ada.Strings.Fixed is
                --  All blanks case
 
                if Low = 0 then
-                  return "";
+                  return Empty_String;
                end if;
 
                declare
@@ -635,7 +813,7 @@ package body Ada.Strings.Fixed is
                --  All blanks case
 
                if High = 0 then
-                  return "";
+                  return Empty_String;
                end if;
 
                declare
@@ -652,7 +830,7 @@ package body Ada.Strings.Fixed is
                --  All blanks case
 
                if Low = 0 then
-                  return "";
+                  return Empty_String;
                end if;
 
                declare
@@ -695,8 +873,7 @@ package body Ada.Strings.Fixed is
          return "";
       end if;
 
-      High :=
-        Index (Source, Set => Right, Test  => Outside, Going => Backward);
+      High := Index (Source, Set => Right, Test => Outside, Going => Backward);
 
       --  Case where source comprises only characters in Right
 
@@ -705,7 +882,8 @@ package body Ada.Strings.Fixed is
       end if;
 
       declare
-         subtype Result_Type is String (1 .. High - Low + 1);
+         Result_Length : constant Integer := High - Low + 1;
+         subtype Result_Type is String (1 .. Result_Length);
 
       begin
          return Result_Type (Source (Low .. High));
diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads
index 4214157..1a5ee94 100644
--- a/gcc/ada/libgnat/a-strfix.ads
+++ b/gcc/ada/libgnat/a-strfix.ads
@@ -13,14 +13,6 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
---  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
 --  subprograms for fixed-length strings; that is, for values of type
 --  Standard.String. Several of these subprograms are procedures that modify
@@ -40,6 +32,20 @@ with Ada.Strings.Maps;
 --  these effects. Similar control is provided by the string transformation
 --  procedures.
 
+--  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. Postconditions and
+--  contract cases should not be executed at runtime as well, in order not to
+--  slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Contract_Cases => Ignore,
+                         Ghost          => Ignore);
+
+with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
+with Ada.Strings.Search;
+
 package Ada.Strings.Fixed with SPARK_Mode is
    pragma Preelaborate;
 
@@ -108,56 +114,60 @@ package Ada.Strings.Fixed with SPARK_Mode is
       Going   : Direction := Forward;
       Mapping : Maps.Character_Mapping_Function) return Natural
    with
-     Pre            =>
-       Pattern'Length /= 0
-         and then (if Source'Length /= 0 then From in Source'Range),
+     Pre            => Pattern'Length > 0
+       and then Mapping /= null
+       and then (if Source'Length > 0 then From in Source'Range),
 
      Post           => Index'Result in 0 | Source'Range,
      Contract_Cases =>
 
-        --  If no slice in the considered range of Source matches Pattern,
-        --  then 0 is returned.
+       --  If Source is the empty string, then 0 is returned
 
-       ((for all J in Source'Range =>
-           (if (if Going = Forward
-                then J in From .. Source'Last - Pattern'Length + 1
-                else J <= From - Pattern'Length + 1)
-            then Translate (Source (J .. J - 1 + Pattern'Length), Mapping)
-                 /= Pattern))
+       (Source'Length = 0
         =>
           Index'Result = 0,
 
-        --  Otherwise, a valid index is returned
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
 
-        others
+        Source'Length > 0
+          and then
+            (for some J in
+              (if Going = Forward then From else Source'First)
+               .. (if Going = Forward then Source'Last else From)
+                - (Pattern'Length - 1) =>
+              Ada.Strings.Search.Match (Source, Pattern, Mapping, J))
         =>
-
           --  The result is in the considered range of Source
 
-          (if Going = Forward
-           then Index'Result in From .. Source'Last - Pattern'Length + 1
-           else Index'Result in Source'First .. From - Pattern'Length + 1)
+          Index'Result in
+            (if Going = Forward then From else Source'First)
+            .. (if Going = Forward then Source'Last else From)
+             - (Pattern'Length - 1)
 
             --  The slice beginning at the returned index matches Pattern
 
             and then
-              Translate (Source (Index'Result
-                                 .. Index'Result - 1 + Pattern'Length),
-                         Mapping)
-              = Pattern
+              Ada.Strings.Search.Match (Source, Pattern, Mapping, Index'Result)
 
-            --  The result is the smallest or largest index which satisfies the
-            --  matching, respectively when Going = Forward and
-            --  Going = Backwards.
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
 
             and then
               (for all J in Source'Range =>
                  (if (if Going = Forward
                       then J in From .. Index'Result - 1
-                      else J - 1 in Index'Result .. From - Pattern'Length)
-                  then Translate (Source (J .. J - 1 + Pattern'Length),
-                                  Mapping)
-                       /= Pattern))),
+                      else J - 1 in Index'Result
+                                    .. From - Pattern'Length)
+                  then not (Ada.Strings.Search.Match
+                              (Source, Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Index'Result = 0),
      Global         => null;
    pragma Ada_05 (Index);
 
@@ -168,56 +178,59 @@ package Ada.Strings.Fixed with SPARK_Mode is
       Going   : Direction := Forward;
       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
    with
-     Pre            =>
-       Pattern'Length /= 0
-         and then (if Source'Length /= 0 then From in Source'Range),
+     Pre            => Pattern'Length > 0
+       and then (if Source'Length > 0 then From in Source'Range),
 
      Post           => Index'Result in 0 | Source'Range,
      Contract_Cases =>
 
-        --  If no slice in the considered range of Source matches Pattern,
-        --  then 0 is returned.
+       --  If Source is the empty string, then 0 is returned
 
-       ((for all J in Source'Range =>
-           (if (if Going = Forward
-                then J in From .. Source'Last - Pattern'Length + 1
-                else J <= From - Pattern'Length + 1)
-            then Translate (Source (J .. J - 1 + Pattern'Length), Mapping)
-                 /= Pattern))
+       (Source'Length = 0
         =>
           Index'Result = 0,
 
-        --  Otherwise, a valid index is returned
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
 
-        others
+        Source'Length > 0
+          and then
+            (for some J in
+              (if Going = Forward then From else Source'First)
+              .. (if Going = Forward then Source'Last else From)
+               - (Pattern'Length - 1) =>
+              Ada.Strings.Search.Match (Source, Pattern, Mapping, J))
         =>
-
           --  The result is in the considered range of Source
 
-          (if Going = Forward
-           then Index'Result in From .. Source'Last - Pattern'Length + 1
-           else Index'Result in Source'First .. From - Pattern'Length + 1)
+          Index'Result in
+            (if Going = Forward then From else Source'First)
+            .. (if Going = Forward then Source'Last else From)
+             - (Pattern'Length - 1)
 
-            --  The slice beginning at the returned index matches Pattern
+          --  The slice beginning at the returned index matches Pattern
 
-            and then
-              Translate (Source (Index'Result
-                                 .. Index'Result - 1 + Pattern'Length),
-                         Mapping)
-              = Pattern
+          and then
+            Ada.Strings.Search.Match (Source, Pattern, Mapping, Index'Result)
 
             --  The result is the smallest or largest index which satisfies the
             --  matching, respectively when Going = Forward and
-            --  Going = Backwards.
+            --  Going = Backward.
 
             and then
               (for all J in Source'Range =>
                  (if (if Going = Forward
                       then J in From .. Index'Result - 1
-                      else J - 1 in Index'Result .. From - Pattern'Length)
-                  then Translate (Source (J .. J - 1 + Pattern'Length),
-                                  Mapping)
-                       /= Pattern))),
+                      else J - 1 in Index'Result
+                                    .. From - Pattern'Length)
+                  then not (Ada.Strings.Search.Match
+                              (Source, Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Index'Result = 0),
      Global         => null;
    pragma Ada_05 (Index);
 
@@ -245,37 +258,33 @@ package Ada.Strings.Fixed with SPARK_Mode is
      Post           => Index'Result in 0 | Source'Range,
      Contract_Cases =>
 
-        --  If Source is empty, or if no slice of Source matches Pattern, then
-        --  0 is returned.
+       --  If Source is the empty string, then 0 is returned
 
        (Source'Length = 0
-          or else
-            (for all J in Source'First .. Source'Last - Pattern'Length + 1 =>
-               Translate (Source (J .. J - 1 + Pattern'Length), Mapping)
-               /= Pattern)
         =>
           Index'Result = 0,
 
-        --  Otherwise, a valid index is returned
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
 
-        others
+        Source'Length > 0
+          and then
+            (for some J in
+              Source'First .. Source'Last - (Pattern'Length - 1) =>
+                Ada.Strings.Search.Match (Source, Pattern, Mapping, J))
         =>
-
           --  The result is in the considered range of Source
 
-          Index'Result in Source'First .. Source'Last - Pattern'Length + 1
+          Index'Result in Source'First .. Source'Last - (Pattern'Length - 1)
 
             --  The slice beginning at the returned index matches Pattern
 
             and then
-              Translate (Source (Index'Result
-                                 .. Index'Result - 1 + Pattern'Length),
-                         Mapping)
-              = Pattern
+              Ada.Strings.Search.Match (Source, Pattern, Mapping, Index'Result)
 
-            --  The result is the smallest or largest index which satisfies the
-            --  matching, respectively when Going = Forward and
-            --  Going = Backwards.
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
 
             and then
               (for all J in Source'Range =>
@@ -283,9 +292,14 @@ package Ada.Strings.Fixed with SPARK_Mode is
                       then J <= Index'Result - 1
                       else J - 1 in Index'Result
                                     .. Source'Last - Pattern'Length)
-                  then Translate (Source (J .. J - 1 + Pattern'Length),
-                                  Mapping)
-                       /= Pattern))),
+                  then not (Ada.Strings.Search.Match
+                              (Source, Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Index'Result = 0),
      Global         => null;
 
    function Index
@@ -294,42 +308,38 @@ package Ada.Strings.Fixed with SPARK_Mode is
       Going   : Direction := Forward;
       Mapping : Maps.Character_Mapping_Function) return Natural
    with
-     Pre            => Pattern'Length > 0,
+     Pre            => Pattern'Length > 0 and then Mapping /= null,
 
      Post           => Index'Result in 0 | Source'Range,
      Contract_Cases =>
 
-        --  If Source is empty, or if no slice of Source matches Pattern, then
-        --  0 is returned.
+       --  If Source is the empty string, then 0 is returned
 
        (Source'Length = 0
-          or else
-            (for all J in Source'First .. Source'Last - Pattern'Length + 1 =>
-               Translate (Source (J .. J - 1 + Pattern'Length), Mapping)
-               /= Pattern)
         =>
           Index'Result = 0,
 
-        --  Otherwise, a valid index is returned
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
 
-        others
+        Source'Length > 0
+          and then
+            (for some J in
+              Source'First .. Source'Last - (Pattern'Length - 1) =>
+                Ada.Strings.Search.Match (Source, Pattern, Mapping, J))
         =>
-
           --  The result is in the considered range of Source
 
-          Index'Result in Source'First .. Source'Last - Pattern'Length + 1
+          Index'Result in Source'First .. Source'Last - (Pattern'Length - 1)
 
-            --  The slice beginning at the returned index matches Pattern
+          --  The slice beginning at the returned index matches Pattern
 
-            and then
-              Translate (Source (Index'Result
-                                 .. Index'Result - 1 + Pattern'Length),
-                         Mapping)
-              = Pattern
+          and then
+            Ada.Strings.Search.Match (Source, Pattern, Mapping, Index'Result)
 
-            --  The result is the smallest or largest index which satisfies the
-            --  matching, respectively when Going = Forward and
-            --  Going = Backwards.
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
 
             and then
               (for all J in Source'Range =>
@@ -337,9 +347,14 @@ package Ada.Strings.Fixed with SPARK_Mode is
                       then J <= Index'Result - 1
                       else J - 1 in Index'Result
                                     .. Source'Last - Pattern'Length)
-                  then Translate (Source (J .. J - 1 + Pattern'Length),
-                                  Mapping)
-                       /= Pattern))),
+                  then not (Ada.Strings.Search.Match
+                              (Source, Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others
+        =>
+          Index'Result = 0),
      Global         => null;
 
    --  If Going = Forward, returns:
@@ -383,9 +398,9 @@ package Ada.Strings.Fixed with SPARK_Mode is
               (Test = Inside)
               = Ada.Strings.Maps.Is_In (Source (Index'Result), Set)
 
-            --  The result is the smallest or largest index which satisfies the
-            --  property, respectively when Going = Forward and
-            --  Going = Backwards.
+            --  The result is the smallest or largest index which satisfies
+            --  the property, respectively when Going = Forward and Going =
+            --  Backward.
 
             and then
               (for all J in Source'Range =>
@@ -402,22 +417,23 @@ package Ada.Strings.Fixed with SPARK_Mode is
       Test    : Membership := Inside;
       Going   : Direction := Forward) return Natural
    with
-     Pre            => (if Source'Length /= 0 then From in Source'Range),
-
+     Pre            => (if Source'Length > 0 then From in Source'Range),
      Post           => Index'Result in 0 | Source'Range,
      Contract_Cases =>
 
-        --  If no character in the considered slice of Source satisfies the
-        --  property Test on Set, then 0 is returned.
+        --  If Source is the empty string, or no character of the considered
+        --  slice of Source satisfies the property Test on Set, then 0 is
+        --  returned.
 
-       ((for all I in Source'Range =>
-           (if I = From
-                 or else (I > From) = (Going = Forward)
-            then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (I), Set)))
+        (Source'Length = 0
+          or else
+            (for all J in Source'Range =>
+               (if J = From or else (J > From) = (Going = Forward) then
+                  (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (J), Set)))
         =>
           Index'Result = 0,
 
-        --  Otherwise, an index in the range of Source is returned
+        --  Otherwise, a index in the considered range of Source is returned
 
         others
         =>
@@ -426,7 +442,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
 
           Index'Result in Source'Range
             and then (Index'Result = From
-                        or else (Index'Result > From) = (Going = Forward))
+                       or else
+                         (Index'Result > From) = (Going = Forward))
 
             --  The character at the returned index satisfies the property
             --  Test on Set.
@@ -435,19 +452,18 @@ package Ada.Strings.Fixed with SPARK_Mode is
               (Test = Inside)
               = Ada.Strings.Maps.Is_In (Source (Index'Result), Set)
 
-            --  The result is the smallest or largest index which satisfies the
-            --  property, respectively when Going = Forward and
-            --  Going = Backwards.
+            --  The result is the smallest or largest index which satisfies
+            --  the property, respectively when Going = Forward and Going =
+            --  Backward.
 
             and then
               (for all J in Source'Range =>
                  (if J /= Index'Result
-                       and then (J < Index'Result) = (Going = Forward)
-                       and then (J = From
-                                   or else (J > From) = (Going = Forward))
-                  then
-                    (Test = Inside)
-                    /= Ada.Strings.Maps.Is_In (Source (J), Set)))),
+                    and then (J < Index'Result) = (Going = Forward)
+                    and then (J = From
+                                or else (J > From) = (Going = Forward))
+                  then (Test = Inside)
+                       /= Ada.Strings.Maps.Is_In (Source (J), Set)))),
      Global         => null;
    pragma Ada_05 (Index);
    --  Index searches for the first or last occurrence of any of a set of
@@ -469,12 +485,14 @@ package Ada.Strings.Fixed with SPARK_Mode is
      Post           => Index_Non_Blank'Result in 0 | Source'Range,
      Contract_Cases =>
 
-        --  If all characters in the considered slice of Source are Space
-        --  characters, then 0 is returned.
+        --  If Source is the empty string, or all characters in the considered
+        --  slice of Source are Space characters, then 0 is returned.
 
-       ((for all J in Source'Range =>
-           (if J = From or else (J > From) = (Going = Forward)
-            then Source (J) = ' '))
+        (Source'Length = 0
+          or else
+            (for all J in Source'Range =>
+               (if J = From or else (J > From) = (Going = Forward) then
+                  Source (J) = ' '))
         =>
           Index_Non_Blank'Result = 0,
 
@@ -496,7 +514,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
 
             --  The result is the smallest or largest index which is not a
             --  Space character, respectively when Going = Forward and
-            --  Going = Backwards.
+            --  Going = Backward.
 
             and then
               (for all J in Source'Range =>
@@ -535,8 +553,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
             and then Source (Index_Non_Blank'Result) /= ' '
 
             --  The result is the smallest or largest index which is not a
-            --  Space character, respectively when Going = Forward and
-            --  Going = Backwards.
+            --  Space character, respectively when Going = Forward and Going
+            --  = Backward.
 
             and then
               (for all J in Source'Range =>
@@ -560,7 +578,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
       Pattern : String;
       Mapping : Maps.Character_Mapping_Function) return Natural
    with
-     Pre    => Pattern'Length /= 0,
+     Pre    => Pattern'Length /= 0 and then Mapping /= null,
      Global => null;
 
    --  Returns the maximum number of nonoverlapping slices of Source that match
@@ -646,6 +664,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
       First  : out Positive;
       Last   : out Natural)
    with
+     Pre            => Source'First > 0,
      Contract_Cases =>
 
         --  If Source is the empty string, or if no character of Source
@@ -701,6 +720,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
      (Source  : String;
       Mapping : Maps.Character_Mapping_Function) return String
    with
+     Pre    => Mapping /= null,
      Post   =>
 
        --  Lower bound of the returned string is 1
@@ -751,10 +771,11 @@ package Ada.Strings.Fixed with SPARK_Mode is
      (Source  : in out String;
       Mapping : Maps.Character_Mapping_Function)
    with
+     Pre    => Mapping /= null,
      Post   =>
 
-       --  Each character in Source after the call is the translation of
-       --  the character at the same position before the call, through Mapping.
+       --  Each character in Source after the call is the translation of the
+       --  character at the same position before the call, through Mapping.
 
        (for all J in Source'Range => Source (J) = Mapping (Source'Old (J))),
      Global => null;
@@ -765,8 +786,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
    with
      Post   =>
 
-       --  Each character in Source after the call is the translation of
-       --  the character at the same position before the call, through Mapping.
+       --  Each character in Source after the call is the translation of the
+       --  character at the same position before the call, through Mapping.
 
        (for all J in Source'Range =>
           Source (J) = Ada.Strings.Maps.Value (Mapping, Source'Old (J))),
@@ -778,32 +799,6 @@ package Ada.Strings.Fixed with SPARK_Mode is
    -- String Transformation Subprograms --
    ---------------------------------------
 
-   procedure Replace_Slice
-     (Source  : in out String;
-      Low     : Positive;
-      High    : Natural;
-      By      : String;
-      Drop    : Truncation := Error;
-      Justify : Alignment  := Left;
-      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:
-   --
-   --  * If High >= Low, then the returned string comprises
-   --    Source (Source'First .. Low - 1)
-   --    & By & Source(High + 1 .. Source'Last), but with lower bound 1.
-   --
-   --  * If High < Low, then the returned string is
-   --    Insert (Source, Before => Low, New_Item => By).
-
    function Replace_Slice
      (Source : String;
       Low    : Positive;
@@ -834,19 +829,19 @@ package Ada.Strings.Fixed with SPARK_Mode is
           --  Length of the returned string
 
           Replace_Slice'Result'Length
-          = Natural'Max (0, Low - Source'First)
+          = Integer'Max (0, Low - Source'First)
             + By'Length
-            + Natural'Max (Source'Last - High, 0)
+            + Integer'Max (Source'Last - High, 0)
 
             --  Elements starting at Low are replaced by elements of By
 
             and then
-              Replace_Slice'Result (1 .. Natural'Max (0, Low - Source'First))
+              Replace_Slice'Result (1 .. Integer'Max (0, Low - Source'First))
               = Source (Source'First .. Low - 1)
             and then
               Replace_Slice'Result
-                (Natural'Max (0, Low - Source'First) + 1
-                 .. Natural'Max (0, Low - Source'First) + By'Length)
+                (Integer'Max (0, Low - Source'First) + 1
+                 .. Integer'Max (0, Low - Source'First) + By'Length)
               = By
 
             --  When there are remaining characters after the replaced slice,
@@ -856,7 +851,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
               (if High < Source'Last
                then
                  Replace_Slice'Result
-                   (Natural'Max (0, Low - Source'First) + By'Length + 1
+                   (Integer'Max (0, Low - Source'First) + By'Length + 1
                     .. Replace_Slice'Result'Last)
                  = Source (High + 1 .. Source'Last)),
 
@@ -890,6 +885,30 @@ package Ada.Strings.Fixed with SPARK_Mode is
                    .. Replace_Slice'Result'Last)
                 = Source (Low .. Source'Last))),
      Global         => null;
+   --  If Low > Source'Last + 1, or High < Source'First - 1, then Index_Error
+   --  is propagated. Otherwise:
+   --
+   --  * If High >= Low, then the returned string comprises
+   --    Source (Source'First .. Low - 1)
+   --    & By & Source(High + 1 .. Source'Last), but with lower bound 1.
+   --
+   --  * If High < Low, then the returned string is
+   --    Insert (Source, Before => Low, New_Item => By).
+
+   procedure Replace_Slice
+     (Source  : in out String;
+      Low     : Positive;
+      High    : Natural;
+      By      : String;
+      Drop    : Truncation := Error;
+      Justify : Alignment  := Left;
+      Pad     : Character  := Space)
+   with
+     Pre    => Low - 1 <= Source'Last,
+
+   --  Incomplete contract
+
+     Global => null;
    --  Equivalent to:
    --
    --    Move (Replace_Slice (Source, Low, High, By),
@@ -929,7 +948,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
          --  are appended to the returned string.
 
          and then
-           (if Before - 1 < Source'Last
+           (if Before <= Source'Last
             then
               Insert'Result
                 (Before - Source'First + New_Item'Length + 1
@@ -937,7 +956,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
               = Source (Before .. Source'Last)),
      Global => null;
    --  Propagates Index_Error if Before is not in
-   --  Source'First .. Source'Last+1; otherwise, returns
+   --  Source'First .. Source'Last + 1; otherwise, returns
    --  Source (Source'First .. Before - 1)
    --  & New_Item & Source(Before..Source'Last), but with lower bound 1.
 
@@ -1384,9 +1403,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
          --  Content of the string is Right concatenated with itself Left times
 
          and then
-           (for all J in 0 .. Left - 1 =>
-              "*"'Result (J * Right'Length + 1 .. (J + 1) * Right'Length)
-              = Right),
+           (for all K in "*"'Result'Range =>
+              "*"'Result (K) = Right (Right'First + (K - 1) mod Right'Length)),
      Global => null;
 
    --  These functions replicate a character or string a specified number of
diff --git a/gcc/ada/libgnat/a-strsea.adb b/gcc/ada/libgnat/a-strsea.adb
index d96a4c7..243c92c 100644
--- a/gcc/ada/libgnat/a-strsea.adb
+++ b/gcc/ada/libgnat/a-strsea.adb
@@ -35,10 +35,18 @@
 --  case of identity mappings for Count and Index, and also Index_Non_Blank
 --  is specialized (rather than using the general Index routine).
 
+--  Ghost code, loop invariants and assertions in this unit are meant for
+--  analysis only, not for run-time checking, as it would be too costly
+--  otherwise. This is enforced by setting the assertion policy to Ignore.
+
+pragma Assertion_Policy (Ghost          => Ignore,
+                         Loop_Invariant => Ignore,
+                         Assert         => Ignore);
+
 with Ada.Strings.Maps; use Ada.Strings.Maps;
 with System;           use System;
 
-package body Ada.Strings.Search is
+package body Ada.Strings.Search with SPARK_Mode is
 
    -----------------------
    -- Local Subprograms --
@@ -61,13 +69,9 @@ package body Ada.Strings.Search is
       Set     : Maps.Character_Set;
       Test    : Membership) return Boolean
    is
-   begin
-      if Test = Inside then
-         return Is_In (Element, Set);
-      else
-         return not Is_In (Element, Set);
-      end if;
-   end Belongs;
+      (if Test = Inside then
+          Is_In (Element, Set)
+      else not (Is_In (Element, Set)));
 
    -----------
    -- Count --
@@ -81,47 +85,63 @@ package body Ada.Strings.Search is
       PL1 : constant Integer := Pattern'Length - 1;
       Num : Natural;
       Ind : Natural;
-      Cur : Natural;
 
    begin
       if Pattern = "" then
          raise Pattern_Error;
       end if;
 
+      --  Isolating the null string case to ensure Source'First, Source'Last in
+      --  Positive.
+
+      if Source = "" then
+         return 0;
+      end if;
+
       Num := 0;
-      Ind := Source'First;
+      Ind := Source'First - 1;
 
       --  Unmapped case
 
-      if Mapping'Address = Maps.Identity'Address then
-         while Ind <= Source'Last - PL1 loop
+      if Is_Identity (Mapping) then
+         while Ind < Source'Last - PL1 loop
+            Ind := Ind + 1;
             if Pattern = Source (Ind .. Ind + PL1) then
                Num := Num + 1;
-               Ind := Ind + Pattern'Length;
-            else
-               Ind := Ind + 1;
+               Ind := Ind + PL1;
             end if;
+
+            pragma Loop_Invariant (Num <= Ind - (Source'First - 1));
+            pragma Loop_Invariant (Ind >= Source'First);
          end loop;
 
       --  Mapped case
 
       else
-         while Ind <= Source'Last - PL1 loop
-            Cur := Ind;
+         while Ind < Source'Last - PL1 loop
+            Ind := Ind + 1;
             for K in Pattern'Range loop
-               if Pattern (K) /= Value (Mapping, Source (Cur)) then
-                  Ind := Ind + 1;
+               if Pattern (K) /= Value (Mapping,
+                 Source (Ind + (K - Pattern'First)))
+               then
+                  pragma Assert (not (Match (Source, Pattern, Mapping, Ind)));
                   goto Cont;
-               else
-                  Cur := Cur + 1;
                end if;
+
+               pragma Loop_Invariant
+                 (for all J in Pattern'First .. K =>
+                    Pattern (J) = Value (Mapping,
+                      Source (Ind + (J - Pattern'First))));
             end loop;
 
+            pragma Assert (Match (Source, Pattern, Mapping, Ind));
             Num := Num + 1;
-            Ind := Ind + Pattern'Length;
+            Ind := Ind + PL1;
 
-         <<Cont>>
+            <<Cont>>
             null;
+            pragma Loop_Invariant (Num <= Ind - (Source'First - 1));
+            pragma Loop_Invariant (Ind >= Source'First);
          end loop;
       end if;
 
@@ -138,13 +158,19 @@ package body Ada.Strings.Search is
       PL1 : constant Integer := Pattern'Length - 1;
       Num : Natural;
       Ind : Natural;
-      Cur : Natural;
 
    begin
       if Pattern = "" then
          raise Pattern_Error;
       end if;
 
+      --  Isolating the null string case to ensure Source'First, Source'Last in
+      --  Positive.
+
+      if Source = "" then
+         return 0;
+      end if;
+
       --  Check for null pointer in case checks are off
 
       if Mapping = null then
@@ -152,23 +178,28 @@ package body Ada.Strings.Search is
       end if;
 
       Num := 0;
-      Ind := Source'First;
-      while Ind <= Source'Last - PL1 loop
-         Cur := Ind;
+      Ind := Source'First - 1;
+      while Ind < Source'Last - PL1 loop
+         Ind := Ind + 1;
          for K in Pattern'Range loop
-            if Pattern (K) /= Mapping (Source (Cur)) then
-               Ind := Ind + 1;
+            if Pattern (K) /= Mapping (Source (Ind + (K - Pattern'First))) then
+               pragma Assert (not (Match (Source, Pattern, Mapping, Ind)));
                goto Cont;
-            else
-               Cur := Cur + 1;
             end if;
+
+            pragma Loop_Invariant
+              (for all J in Pattern'First .. K =>
+                 Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
          end loop;
 
+         pragma Assert (Match (Source, Pattern, Mapping, Ind));
          Num := Num + 1;
-         Ind := Ind + Pattern'Length;
+         Ind := Ind + PL1;
 
       <<Cont>>
          null;
+         pragma Loop_Invariant (Num <= Ind - (Source'First - 1));
+         pragma Loop_Invariant (Ind >= Source'First);
       end loop;
 
       return Num;
@@ -182,6 +213,7 @@ package body Ada.Strings.Search is
 
    begin
       for J in Source'Range loop
+         pragma Loop_Invariant (N <= J - Source'First);
          if Is_In (Source (J), Set) then
             N := N + 1;
          end if;
@@ -217,12 +249,18 @@ package body Ada.Strings.Search is
          if Belongs (Source (J), Set, Test) then
             First := J;
 
-            for K in J + 1 .. Source'Last loop
-               if not Belongs (Source (K), Set, Test) then
-                  Last := K - 1;
-                  return;
-               end if;
-            end loop;
+            if J < Source'Last then
+               for K in J + 1 .. Source'Last loop
+                  if not Belongs (Source (K), Set, Test) then
+                     Last := K - 1;
+                     return;
+                  end if;
+
+                  pragma Loop_Invariant
+                    (for all L in J .. K =>
+                       Belongs (Source (L), Set, Test));
+               end loop;
+            end if;
 
             --  Here if J indexes first char of token, and all chars after J
             --  are in the token.
@@ -230,6 +268,10 @@ package body Ada.Strings.Search is
             Last := Source'Last;
             return;
          end if;
+
+         pragma Loop_Invariant
+           (for all K in Integer'Max (From, Source'First) .. J =>
+                not (Belongs (Source (K), Set, Test)));
       end loop;
 
       --  Here if no token found
@@ -250,12 +292,18 @@ package body Ada.Strings.Search is
          if Belongs (Source (J), Set, Test) then
             First := J;
 
-            for K in J + 1 .. Source'Last loop
-               if not Belongs (Source (K), Set, Test) then
-                  Last := K - 1;
-                  return;
-               end if;
-            end loop;
+            if J < Source'Last then
+               for K in J + 1 .. Source'Last loop
+                  if not Belongs (Source (K), Set, Test) then
+                     Last := K - 1;
+                     return;
+                  end if;
+
+                  pragma Loop_Invariant
+                    (for all L in J .. K =>
+                       Belongs (Source (L), Set, Test));
+               end loop;
+            end if;
 
             --  Here if J indexes first char of token, and all chars after J
             --  are in the token.
@@ -263,6 +311,10 @@ package body Ada.Strings.Search is
             Last := Source'Last;
             return;
          end if;
+
+         pragma Loop_Invariant
+           (for all K in Source'First .. J =>
+              not (Belongs (Source (K), Set, Test)));
       end loop;
 
       --  Here if no token found
@@ -292,53 +344,61 @@ package body Ada.Strings.Search is
       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
    is
       PL1 : constant Integer := Pattern'Length - 1;
-      Cur : Natural;
-
-      Ind : Integer;
-      --  Index for start of match check. This can be negative if the pattern
-      --  length is greater than the string length, which is why this variable
-      --  is Integer instead of Natural. In this case, the search loops do not
-      --  execute at all, so this Ind value is never used.
 
    begin
       if Pattern = "" then
          raise Pattern_Error;
       end if;
 
+      --  If Pattern is longer than Source, it can't be found
+
+      if Pattern'Length > Source'Length then
+         return 0;
+      end if;
+
       --  Forwards case
 
       if Going = Forward then
-         Ind := Source'First;
 
          --  Unmapped forward case
 
-         if Mapping'Address = Maps.Identity'Address then
-            for J in 1 .. Source'Length - PL1 loop
+         if Is_Identity (Mapping) then
+            for Ind in Source'First .. Source'Last - PL1 loop
                if Pattern = Source (Ind .. Ind + PL1) then
+                  pragma Assert (Match (Source, Pattern, Mapping, Ind));
                   return Ind;
-               else
-                  Ind := Ind + 1;
                end if;
+
+               pragma Loop_Invariant
+                 (for all J in Source'First .. Ind =>
+                    not (Match (Source, Pattern, Mapping, J)));
             end loop;
 
          --  Mapped forward case
 
          else
-            for J in 1 .. Source'Length - PL1 loop
-               Cur := Ind;
-
+            for Ind in Source'First .. Source'Last - PL1 loop
                for K in Pattern'Range loop
-                  if Pattern (K) /= Value (Mapping, Source (Cur)) then
+                  if Pattern (K) /= Value (Mapping,
+                    Source (Ind + (K - Pattern'First)))
+                  then
                      goto Cont1;
-                  else
-                     Cur := Cur + 1;
                   end if;
+
+                  pragma Loop_Invariant
+                    (for all J in Pattern'First .. K =>
+                       Pattern (J) = Value (Mapping,
+                         Source (Ind + (J - Pattern'First))));
                end loop;
 
+               pragma Assert (Match (Source, Pattern, Mapping, Ind));
                return Ind;
 
-            <<Cont1>>
-               Ind := Ind + 1;
+               <<Cont1>>
+               pragma Loop_Invariant
+                 (for all J in Source'First .. Ind =>
+                    not (Match (Source, Pattern, Mapping, J)));
+               null;
             end loop;
          end if;
 
@@ -347,35 +407,43 @@ package body Ada.Strings.Search is
       else
          --  Unmapped backward case
 
-         Ind := Source'Last - PL1;
-
-         if Mapping'Address = Maps.Identity'Address then
-            for J in reverse 1 .. Source'Length - PL1 loop
+         if Is_Identity (Mapping) then
+            for Ind in reverse Source'First .. Source'Last - PL1 loop
                if Pattern = Source (Ind .. Ind + PL1) then
+                  pragma Assert (Match (Source, Pattern, Mapping, Ind));
                   return Ind;
-               else
-                  Ind := Ind - 1;
                end if;
+
+               pragma Loop_Invariant
+                 (for all J in Ind .. Source'Last - PL1 =>
+                    not (Match (Source, Pattern, Mapping, J)));
             end loop;
 
          --  Mapped backward case
 
          else
-            for J in reverse 1 .. Source'Length - PL1 loop
-               Cur := Ind;
-
+            for Ind in reverse Source'First .. Source'Last - PL1 loop
                for K in Pattern'Range loop
-                  if Pattern (K) /= Value (Mapping, Source (Cur)) then
+                  if Pattern (K) /= Value (Mapping,
+                    Source (Ind + (K - Pattern'First)))
+                  then
                      goto Cont2;
-                  else
-                     Cur := Cur + 1;
                   end if;
+
+                  pragma Loop_Invariant
+                    (for all J in Pattern'First .. K =>
+                       Pattern (J) = Value (Mapping,
+                         Source (Ind + (J - Pattern'First))));
                end loop;
 
+               pragma Assert (Match (Source, Pattern, Mapping, Ind));
                return Ind;
 
-            <<Cont2>>
-               Ind := Ind - 1;
+               <<Cont2>>
+               pragma Loop_Invariant
+                 (for all J in Ind .. Source'Last - PL1 =>
+                    not (Match (Source, Pattern, Mapping, J)));
+               null;
             end loop;
          end if;
       end if;
@@ -393,9 +461,6 @@ package body Ada.Strings.Search is
       Mapping : Maps.Character_Mapping_Function) return Natural
    is
       PL1 : constant Integer := Pattern'Length - 1;
-      Ind : Natural;
-      Cur : Natural;
-
    begin
       if Pattern = "" then
          raise Pattern_Error;
@@ -416,43 +481,52 @@ package body Ada.Strings.Search is
       --  Forwards case
 
       if Going = Forward then
-         Ind := Source'First;
-         for J in 1 .. Source'Length - PL1 loop
-            Cur := Ind;
-
+         for Ind in Source'First .. Source'Last - PL1 loop
             for K in Pattern'Range loop
-               if Pattern (K) /= Mapping.all (Source (Cur)) then
+               if Pattern (K) /= Mapping.all
+                 (Source (Ind + (K - Pattern'First)))
+               then
                   goto Cont1;
-               else
-                  Cur := Cur + 1;
                end if;
+
+               pragma Loop_Invariant
+                 (for all J in Pattern'First .. K =>
+                   Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
             end loop;
 
+            pragma Assert (Match (Source, Pattern, Mapping, Ind));
             return Ind;
 
-         <<Cont1>>
-            Ind := Ind + 1;
+            <<Cont1>>
+            pragma Loop_Invariant
+              (for all J in Source'First .. Ind =>
+                 not (Match (Source, Pattern, Mapping, J)));
+            null;
          end loop;
 
       --  Backwards case
 
       else
-         Ind := Source'Last - PL1;
-         for J in reverse 1 .. Source'Length - PL1 loop
-            Cur := Ind;
-
+         for Ind in reverse Source'First .. Source'Last - PL1 loop
             for K in Pattern'Range loop
-               if Pattern (K) /= Mapping.all (Source (Cur)) then
+               if Pattern (K) /= Mapping.all
+                 (Source (Ind + (K - Pattern'First)))
+               then
                   goto Cont2;
-               else
-                  Cur := Cur + 1;
                end if;
+
+               pragma Loop_Invariant
+                 (for all J in Pattern'First .. K =>
+                   Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
             end loop;
 
             return Ind;
 
-         <<Cont2>>
-            Ind := Ind - 1;
+            <<Cont2>>
+            pragma Loop_Invariant
+              (for all J in Ind .. (Source'Last - PL1) =>
+                not (Match (Source, Pattern, Mapping, J)));
+            null;
          end loop;
       end if;
 
@@ -476,6 +550,10 @@ package body Ada.Strings.Search is
             if Belongs (Source (J), Set, Test) then
                return J;
             end if;
+
+            pragma Loop_Invariant
+              (for all C of Source (Source'First .. J) =>
+                   not (Belongs (C, Set, Test)));
          end loop;
 
       --  Backwards case
@@ -485,6 +563,10 @@ package body Ada.Strings.Search is
             if Belongs (Source (J), Set, Test) then
                return J;
             end if;
+
+            pragma Loop_Invariant
+              (for all C of Source (J .. Source'Last) =>
+                   not (Belongs (C, Set, Test)));
          end loop;
       end if;
 
@@ -500,6 +582,8 @@ package body Ada.Strings.Search is
       Going   : Direction := Forward;
       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
    is
+      Result : Natural;
+      PL1    : constant Integer := Pattern'Length - 1;
    begin
 
       --  AI05-056: If source is empty result is always zero
@@ -512,17 +596,29 @@ package body Ada.Strings.Search is
             raise Index_Error;
          end if;
 
-         return
+         Result :=
            Index (Source (From .. Source'Last), Pattern, Forward, Mapping);
+         pragma Assert
+           (if (for some J in From .. Source'Last - PL1 =>
+                 Match (Source, Pattern, Mapping, J))
+            then Result in From .. Source'Last - PL1
+            else Result = 0);
 
       else
          if From > Source'Last then
             raise Index_Error;
          end if;
 
-         return
+         Result :=
            Index (Source (Source'First .. From), Pattern, Backward, Mapping);
+         pragma Assert
+           (if (for some J in Source'First .. From - PL1 =>
+                  Match (Source, Pattern, Mapping, J))
+            then Result in Source'First .. From - PL1
+            else Result = 0);
       end if;
+
+      return Result;
    end Index;
 
    function Index
@@ -603,6 +699,9 @@ package body Ada.Strings.Search is
             if Source (J) /= ' ' then
                return J;
             end if;
+
+            pragma Loop_Invariant
+              (for all C of Source (Source'First .. J) => C = ' ');
          end loop;
 
       else -- Going = Backward
@@ -610,6 +709,9 @@ package body Ada.Strings.Search is
             if Source (J) /= ' ' then
                return J;
             end if;
+
+            pragma Loop_Invariant
+              (for all C of Source (J .. Source'Last) => C = ' ');
          end loop;
       end if;
 
@@ -624,6 +726,13 @@ package body Ada.Strings.Search is
       Going  : Direction := Forward) return Natural
    is
    begin
+
+      --  For equivalence with Index, if Source is empty the result is 0
+
+      if Source'Length = 0 then
+         return 0;
+      end if;
+
       if Going = Forward then
          if From < Source'First then
             raise Index_Error;
@@ -642,4 +751,12 @@ package body Ada.Strings.Search is
       end if;
    end Index_Non_Blank;
 
+   function Is_Identity
+     (Mapping : Maps.Character_Mapping) return Boolean
+   with SPARK_Mode => Off
+   is
+   begin
+      return Mapping'Address = Maps.Identity'Address;
+   end Is_Identity;
+
 end Ada.Strings.Search;
diff --git a/gcc/ada/libgnat/a-strsea.ads b/gcc/ada/libgnat/a-strsea.ads
index 623c0f4..4396747 100644
--- a/gcc/ada/libgnat/a-strsea.ads
+++ b/gcc/ada/libgnat/a-strsea.ads
@@ -32,76 +32,489 @@
 --  This package contains the search functions from Ada.Strings.Fixed. They
 --  are separated out because they are shared by Ada.Strings.Bounded and
 --  Ada.Strings.Unbounded, and we don't want to drag in other irrelevant stuff
---  from Ada.Strings.Fixed when using the other two packages. We make this a
---  private package, since user programs should access these subprograms via
---  one of the standard string packages.
+--  from Ada.Strings.Fixed when using the other two packages. Although user
+--  programs should access these subprograms via one of the standard string
+--  packages, we do not make this a private package, since ghost function
+--  Match is used in the contracts of the standard string packages.
 
-with Ada.Strings.Maps;
+--  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. Postconditions,
+--  contract cases and ghost code should not be executed at runtime as well,
+--  in order not to slow down the execution of these functions.
 
-private package Ada.Strings.Search is
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Contract_Cases => Ignore,
+                         Ghost          => Ignore);
+
+with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
+
+package Ada.Strings.Search with SPARK_Mode is
    pragma Preelaborate;
 
+   --  The ghost function Match tells whether the slice of Source starting at
+   --  From and of length Pattern'Length matches with Pattern with respect to
+   --  Mapping. Pattern should be non-empty and the considered slice should be
+   --  fully included in Source'Range.
+
+   function Match
+     (Source  : String;
+      Pattern : String;
+      Mapping : Maps.Character_Mapping_Function;
+      From    : Integer) return Boolean
+   is
+      (for all K in Pattern'Range =>
+         Pattern (K) = Mapping (Source (From + (K - Pattern'First))))
+   with
+     Ghost,
+     Pre    => Mapping /= null
+       and then Pattern'Length > 0
+       and then Source'Length > 0
+       and then From in Source'First .. Source'Last - (Pattern'Length - 1),
+     Global => null;
+
+   function Match
+     (Source  : String;
+      Pattern : String;
+      Mapping : Maps.Character_Mapping;
+      From    : Integer) return Boolean
+   is
+      (for all K in Pattern'Range =>
+         Pattern (K) =
+           Ada.Strings.Maps.Value
+             (Mapping, Source (From + (K - Pattern'First))))
+   with
+     Ghost,
+     Pre    => Pattern'Length > 0
+       and then Source'Length > 0
+       and then From in Source'First .. Source'Last - (Pattern'Length - 1),
+     Global => null;
+
+   function Is_Identity
+     (Mapping : Maps.Character_Mapping) return Boolean
+   with
+     Post   => (if Is_Identity'Result then
+                (for all K in Character =>
+                   Ada.Strings.Maps.Value (Mapping, K) = K)),
+     Global => null;
+
    function Index
      (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,
+
+     Post           => Index'Result in 0 | Source'Range,
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Source'Length = 0 => Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Source'Length > 0
+          and then
+            (for some J in
+               Source'First .. Source'Last - (Pattern'Length - 1) =>
+                 Match (Source, Pattern, Mapping, J))
+        =>
+
+          --  The result is in the considered range of Source
+
+          Index'Result in Source'First .. Source'Last - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Match (Source, Pattern, Mapping, Index'Result)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in Source'Range =>
+                 (if (if Going = Forward
+                      then J <= Index'Result - 1
+                      else J - 1 in Index'Result
+                                    .. Source'Last - Pattern'Length)
+                  then not (Match (Source, Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others => Index'Result = 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 and then Mapping /= null,
+     Post           => Index'Result in 0 | Source'Range,
+     Contract_Cases =>
+
+       --  If Source is the null string, then 0 is returned
+
+       (Source'Length = 0 => Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Source'Length > 0 and then
+        (for some J in Source'First .. Source'Last - (Pattern'Length - 1) =>
+             Match (Source, Pattern, Mapping, J))
+        =>
+
+          --  The result is in the considered range of Source
+
+          Index'Result in Source'First .. Source'Last - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Match (Source, Pattern, Mapping, Index'Result)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in Source'Range =>
+                 (if (if Going = Forward
+                      then J <= Index'Result - 1
+                      else J - 1 in Index'Result
+                                    .. Source'Last - Pattern'Length)
+                  then not (Match (Source, Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others => Index'Result = 0),
+     Global         => null;
 
    function Index
      (Source : String;
       Set    : Maps.Character_Set;
       Test   : Membership := Inside;
-      Going  : Direction  := Forward) return Natural;
+      Going  : Direction  := Forward) return Natural
+   with
+     Post           => Index'Result in 0 | Source'Range,
+     Contract_Cases =>
+
+        --  If no character of Source satisfies the property Test on Set, then
+        --  0 is returned.
+
+       ((for all C of Source =>
+           (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set))
+        =>
+          Index'Result = 0,
+
+        --  Otherwise, a index in the range of Source is returned
+
+        others =>
+
+          --  The result is in the range of Source
+
+          Index'Result in Source'Range
+
+            --  The character at the returned index satisfies the property
+            --  Test on Set
+
+            and then (Test = Inside)
+              = Ada.Strings.Maps.Is_In (Source (Index'Result), Set)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the property, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in Source'Range =>
+                 (if J /= Index'Result
+                       and then (J < Index'Result) = (Going = Forward)
+                  then (Test = Inside)
+                       /= Ada.Strings.Maps.Is_In (Source (J), Set)))),
+     Global         => null;
 
    function Index
      (Source  : 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            => Pattern'Length > 0
+       and then (if Source'Length > 0 then From in Source'Range),
+
+     Post           => Index'Result in 0 | Source'Range,
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Source'Length = 0 => Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Source'Length > 0
+          and then
+            (for some J in
+              (if Going = Forward then From else Source'First)
+              .. (if Going = Forward then Source'Last else From)
+               - (Pattern'Length - 1) =>
+              Match (Source, Pattern, Mapping, J))
+        =>
+
+          --  The result is in the considered range of Source
+
+          Index'Result in
+            (if Going = Forward then From else Source'First)
+            .. (if Going = Forward then Source'Last else From)
+              - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Match (Source, Pattern, Mapping, Index'Result)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in Source'Range =>
+                 (if (if Going = Forward
+                      then J in From .. Index'Result - 1
+                      else J - 1 in Index'Result
+                                    .. From - Pattern'Length)
+                  then not (Match (Source, Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others => Index'Result = 0),
+     Global         => null;
 
    function Index
      (Source  : String;
       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 Mapping /= null
+       and then (if Source'Length > 0 then From in Source'Range),
+
+     Post           => Index'Result in 0 | Source'Range,
+     Contract_Cases =>
+
+       --  If Source is the empty string, then 0 is returned
+
+       (Source'Length = 0 => Index'Result = 0,
+
+        --  If some slice of Source matches Pattern, then a valid index is
+        --  returned.
+
+        Source'Length > 0
+          and then
+            (for some J in
+              (if Going = Forward then From else Source'First)
+              .. (if Going = Forward then Source'Last else From)
+               - (Pattern'Length - 1) =>
+              Match (Source, Pattern, Mapping, J))
+        =>
+
+          --  The result is in the considered range of Source
+
+          Index'Result in
+            (if Going = Forward then From else Source'First)
+            .. (if Going = Forward then Source'Last else From)
+              - (Pattern'Length - 1)
+
+            --  The slice beginning at the returned index matches Pattern
+
+            and then Match (Source, Pattern, Mapping, Index'Result)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the matching, respectively when Going = Forward and Going =
+            --  Backwards.
+
+            and then
+              (for all J in Source'Range =>
+                 (if (if Going = Forward
+                      then J in From .. Index'Result - 1
+                      else J - 1 in Index'Result
+                                    .. From - Pattern'Length)
+                  then not (Match (Source, Pattern, Mapping, J)))),
+
+        --  Otherwise, 0 is returned
+
+        others => Index'Result = 0),
+     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),
+     Post           => Index'Result in 0 | Source'Range,
+     Contract_Cases =>
+
+        --  If Source is the empty string, or no character of the considered
+        --  slice of Source satisfies the property Test on Set, then 0 is
+        --  returned.
+
+        (Source'Length = 0
+          or else
+            (for all J in Source'Range =>
+               (if J = From or else (J > From) = (Going = Forward) then
+                  (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (J), Set)))
+        =>
+          Index'Result = 0,
+
+        --  Otherwise, a index in the considered range of Source is returned
+
+        others =>
+
+          --  The result is in the considered range of Source
+
+          Index'Result in Source'Range
+            and then (Index'Result = From
+                       or else
+                         (Index'Result > From) = (Going = Forward))
+
+            --  The character at the returned index satisfies the property
+            --  Test on Set
+
+            and then
+              (Test = Inside)
+              = Ada.Strings.Maps.Is_In (Source (Index'Result), Set)
+
+            --  The result is the smallest or largest index which satisfies
+            --  the property, respectively when Going = Forward and Going =
+            --  Backward.
+
+            and then
+              (for all J in Source'Range =>
+                 (if J /= Index'Result
+                    and then (J < Index'Result) = (Going = Forward)
+                    and then (J = From
+                                or else (J > From) = (Going = Forward))
+                  then (Test = Inside)
+                       /= Ada.Strings.Maps.Is_In (Source (J), Set)))),
+     Global         => null;
 
    function Index_Non_Blank
      (Source : String;
-      Going  : Direction := Forward) return Natural;
+      Going  : Direction := Forward) return Natural
+   with
+     Post           => Index_Non_Blank'Result in 0 | Source'Range,
+     Contract_Cases =>
+
+        --  If all characters of Source are Space characters, then 0 is
+        --  returned.
+
+       ((for all C of Source => C = ' ') => Index_Non_Blank'Result = 0,
+
+        --  Otherwise, a valid index is returned
+
+        others                           =>
+
+          --  The result is in the range of Source
+
+          Index_Non_Blank'Result in Source'Range
+
+            --  The character at the returned index is not a Space character
+
+            and then Source (Index_Non_Blank'Result) /= ' '
+
+            --  The result is the smallest or largest index which is not a
+            --  Space character, respectively when Going = Forward and
+            --  Going = Backward.
+
+            and then
+              (for all J in Source'Range =>
+                 (if J /= Index_Non_Blank'Result
+                       and then (J < Index_Non_Blank'Result)
+                              = (Going = Forward)
+                  then Source (J) = ' '))),
+     Global         => null;
 
    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),
+     Post           => Index_Non_Blank'Result in 0 | Source'Range,
+     Contract_Cases =>
+
+        --  If Source is the null string, or all characters in the considered
+        --  slice of Source are Space characters, then 0 is returned.
+
+        (Source'Length = 0
+          or else
+            (for all J in Source'Range =>
+               (if J = From or else (J > From) = (Going = Forward) then
+                  Source (J) = ' '))
+        =>
+          Index_Non_Blank'Result = 0,
+
+        --  Otherwise, a valid index is returned
+
+        others =>
+
+          --  The result is in the considered range of Source
+
+          Index_Non_Blank'Result in Source'Range
+            and then (Index_Non_Blank'Result = From
+                        or else (Index_Non_Blank'Result > From)
+                                = (Going = Forward))
+
+            --  The character at the returned index is not a Space character
+
+            and then Source (Index_Non_Blank'Result) /= ' '
+
+            --  The result is the smallest or largest index which is not a
+            --  Space character, respectively when Going = Forward and
+            --  Going = Backward.
+
+            and then
+              (for all J in Source'Range =>
+                 (if J /= Index_Non_Blank'Result
+                       and then (J < Index_Non_Blank'Result)
+                                = (Going = Forward)
+                       and then (J = From or else (J > From)
+                                = (Going = Forward))
+                  then Source (J) = ' '))),
+     Global         => null;
 
    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 and then Mapping /= null,
+     Global => null;
 
    function Count
      (Source : String;
-      Set    : Maps.Character_Set) return Natural;
+      Set    : Maps.Character_Set) return Natural
+   with
+     Global => null;
 
    procedure Find_Token
      (Source : String;
@@ -109,13 +522,104 @@ private package Ada.Strings.Search 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),
+     Contract_Cases =>
+
+        --  If Source is the empty string, or if no character of the considered
+        --  slice of Source satisfies the property Test on Set, then First is
+        --  set to From and Last is set to 0.
+
+       (Source'Length = 0
+         or else
+           (for all C of Source (From .. Source'Last) =>
+              (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set))
+        =>
+          First = From and then Last = 0,
+
+        --  Otherwise, First and Last are set to valid indexes
+
+        others =>
+
+          --  First and Last are in the considered range of Source
+
+          First in From .. Source'Last
+            and then Last in First .. Source'Last
+
+            --  No character between From and First satisfies the property Test
+            --  on Set.
+
+            and then
+              (for all C of Source (From .. First - 1) =>
+                 (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set))
+
+            --  All characters between First and Last satisfy the property Test
+            --  on Set.
+
+            and then
+              (for all C of Source (First .. Last) =>
+                 (Test = Inside) = Ada.Strings.Maps.Is_In (C, Set))
+
+            --  If Last is not Source'Last, then the character at position
+            --  Last + 1 does not satify the property Test on Set.
+
+            and then
+              (if Last < Source'Last
+               then (Test = Inside)
+                 /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))),
+     Global         => null;
 
    procedure Find_Token
      (Source : String;
       Set    : Maps.Character_Set;
       Test   : Membership;
       First  : out Positive;
-      Last   : out Natural);
+      Last   : out Natural)
+   with
+     Pre            => Source'First > 0,
+     Contract_Cases =>
+
+        --  If Source is the empty string, or if no character of Source
+        --  satisfies the property Test on Set, then First is set to From
+        --  and Last is set to 0.
+
+       (Source'Length = 0
+         or else
+           (for all C of Source =>
+              (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set))
+        =>
+          First = Source'First and then Last = 0,
+
+        --  Otherwise, First and Last are set to valid indexes
+
+        others =>
+
+          --  First and Last are in the considered range of Source
+
+          First in Source'Range
+            and then Last in First .. Source'Last
+
+            --  No character before First satisfies the property Test on Set
+
+            and then
+              (for all C of Source (Source'First .. First - 1) =>
+                 (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set))
+
+            --  All characters between First and Last satisfy the property Test
+            --  on Set.
+
+            and then
+              (for all C of Source (First .. Last) =>
+                 (Test = Inside) = Ada.Strings.Maps.Is_In (C, Set))
+
+            --  If Last is not Source'Last, then the character at position
+            --  Last + 1 does not satify the property Test on Set.
+
+            and then
+              (if Last < Source'Last
+               then (Test = Inside)
+                 /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))),
+     Global => null;
 
 end Ada.Strings.Search;