[Ada] Remove global parameter in Global contracts of Ada.Strings.Bounded

gcc/ada/

	* libgnat/a-strbou.ads (Generic_Bounded_Length): Remove non-null
	Global contracts.

diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads
index b88e04935b1056562535b95214e025cc5e7a40e0..cc24f707e5f851cfd952ff7c75370ec8a2b288fa 100644 (file)
--- a/gcc/ada/libgnat/a-strbou.ads
+++ b/gcc/ada/libgnat/a-strbou.ads
@@ -95,8 +95,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
            others  --  Drop = Right
            =>
              To_String (To_Bounded_String'Result) =
-               Source (Source'First .. Source'First - 1 + Max_Length)),
-        Global         => Max_Length;
+               Source (Source'First .. Source'First - 1 + Max_Length));
 
       function To_String (Source : Bounded_String) return String with
         Global => null;
@@ -120,8 +119,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
            others  --  Drop = Right
            =>
              To_String (Target) =
-               Source (Source'First .. Source'First - 1 + Max_Length)),
-        Global         => (Proof_In => Max_Length);
+               Source (Source'First .. Source'First - 1 + Max_Length));
       pragma Ada_05 (Set_Bounded_String);
 
       function Append
@@ -167,8 +165,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                and then
                  (if Length (Left) < Max_Length then
                     Slice (Append'Result, Length (Left) + 1, Max_Length) =
-                      Slice (Right, 1, Max_Length - Length (Left)))),
-        Global         => (Proof_In => Max_Length);
+                      Slice (Right, 1, Max_Length - Length (Left))));
 
       function Append
         (Left  : Bounded_String;
@@ -222,9 +219,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                  (if Length (Left) < Max_Length then
                     Slice (Append'Result, Length (Left) + 1, Max_Length) =
                       Right (Right'First
-                        .. Max_Length - Length (Left) - 1 + Right'First))),
-        Global         => (Proof_In => Max_Length);
-
+                        .. Max_Length - Length (Left) - 1 + Right'First)));
       function Append
         (Left  : String;
          Right : Bounded_String;
@@ -274,8 +269,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                     --  The result is the first Max_Length characters of Left
 
                     To_String (Append'Result) =
-                      Left (Left'First .. Max_Length - 1 + Left'First))),
-        Global         => (Proof_In => Max_Length);
+                      Left (Left'First .. Max_Length - 1 + Left'First)));
 
       function Append
         (Left  : Bounded_String;
@@ -302,8 +296,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                and then
                  Slice (Append'Result, 1, Max_Length - 1) =
                    Slice (Left, 2, Max_Length)
-               and then Element (Append'Result, Max_Length) = Right),
-        Global         => (Proof_In => Max_Length);
+               and then Element (Append'Result, Max_Length) = Right);
 
       function Append
         (Left  : Character;
@@ -331,8 +324,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                and then
                  Slice (Append'Result, 2, Max_Length) =
                    Slice (Right, 1, Max_Length - 1)
-               and then Element (Append'Result, 1) = Left),
-        Global         => (Proof_In => Max_Length);
+               and then Element (Append'Result, 1) = Left);
 
       procedure Append
         (Source   : in out Bounded_String;
@@ -378,8 +370,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                and then
                  (if Length (Source'Old) < Max_Length then
                     Slice (Source, Length (Source'Old) + 1, Max_Length) =
-                      Slice (New_Item, 1, Max_Length - Length (Source'Old)))),
-        Global         => (Proof_In => Max_Length);
+                      Slice (New_Item, 1, Max_Length - Length (Source'Old))));
 
       procedure Append
         (Source   : in out Bounded_String;
@@ -436,8 +427,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                     Slice (Source, Length (Source'Old) + 1, Max_Length) =
                       New_Item (New_Item'First
                         .. Max_Length - Length (Source'Old) - 1
-                          + New_Item'First))),
-        Global         => (Proof_In => Max_Length);
+                          + New_Item'First)));
 
       procedure Append
         (Source   : in out Bounded_String;
@@ -465,68 +455,62 @@ package Ada.Strings.Bounded with SPARK_Mode is
                and then
                  Slice (Source, 1, Max_Length - 1) =
                    Slice (Source'Old, 2, Max_Length)
-               and then Element (Source, Max_Length) = New_Item),
-        Global         => (Proof_In => Max_Length);
+               and then Element (Source, Max_Length) = New_Item);
 
       function "&"
         (Left  : Bounded_String;
          Right : Bounded_String) return Bounded_String
       with
-        Pre    => Length (Left) <= Max_Length - Length (Right),
-        Post   => Length ("&"'Result) = Length (Left) + Length (Right)
+        Pre  => Length (Left) <= Max_Length - Length (Right),
+        Post => Length ("&"'Result) = Length (Left) + Length (Right)
           and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left)
           and then
             (if Length (Right) > 0 then
                Slice ("&"'Result, Length (Left) + 1, Length ("&"'Result)) =
-                 To_String (Right)),
-        Global => (Proof_In => Max_Length);
+                 To_String (Right));
 
       function "&"
         (Left  : Bounded_String;
          Right : String) return Bounded_String
       with
-        Pre    => Right'Length <= Max_Length - Length (Left),
-        Post   => Length ("&"'Result) = Length (Left) + Right'Length
+        Pre  => Right'Length <= Max_Length - Length (Left),
+        Post => Length ("&"'Result) = Length (Left) + Right'Length
           and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left)
           and then
             (if Right'Length > 0 then
                Slice ("&"'Result, Length (Left) + 1, Length ("&"'Result)) =
-                 Right),
-        Global => (Proof_In => Max_Length);
+                 Right);
 
       function "&"
         (Left  : String;
          Right : Bounded_String) return Bounded_String
       with
-        Pre    => Left'Length <= Max_Length - Length (Right),
-        Post   => Length ("&"'Result) = Left'Length + Length (Right)
+        Pre  => Left'Length <= Max_Length - Length (Right),
+        Post => Length ("&"'Result) = Left'Length + Length (Right)
           and then Slice ("&"'Result, 1, Left'Length) = Left
           and then
             (if Length (Right) > 0 then
                Slice ("&"'Result, Left'Length + 1, Length ("&"'Result)) =
-                 To_String (Right)),
-        Global => (Proof_In => Max_Length);
+                 To_String (Right));
 
       function "&"
         (Left  : Bounded_String;
          Right : Character) return Bounded_String
       with
-        Pre    => Length (Left) < Max_Length,
-        Post   => Length ("&"'Result) = Length (Left) + 1
+        Pre  => Length (Left) < Max_Length,
+        Post => Length ("&"'Result) = Length (Left) + 1
           and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left)
-          and then Element ("&"'Result, Length (Left) + 1) = Right,
-        Global => (Proof_In => Max_Length);
+          and then Element ("&"'Result, Length (Left) + 1) = Right;
 
       function "&"
         (Left  : Character;
          Right : Bounded_String) return Bounded_String
       with
-        Pre    => Length (Right) < Max_Length,
-        Post   => Length ("&"'Result) = 1 + Length (Right)
+        Pre  => Length (Right) < Max_Length,
+        Post => Length ("&"'Result) = 1 + Length (Right)
           and then Element ("&"'Result, 1) = Left
           and then
-            Slice ("&"'Result, 2, Length ("&"'Result)) = To_String (Right),
-        Global => (Proof_In => Max_Length);
+            Slice ("&"'Result, 2, Length ("&"'Result)) = To_String (Right);
 
       function Element
         (Source : Bounded_String;
@@ -1426,8 +1410,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                         Low + By'Length, Max_Length) =
                           Slice (Source, Integer'Max (High + 1, Low),
                             Integer'Max (High + 1, Low) +
-                              (Max_Length - Low - By'Length)))),
-        Global         => (Proof_In => Max_Length);
+                              (Max_Length - Low - By'Length))));
 
       procedure Replace_Slice
         (Source   : in out Bounded_String;
@@ -1551,8 +1534,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                       and then Slice (Source, Low + By'Length, Max_Length) =
                         Slice (Source'Old, Integer'Max (High + 1, Low),
                           Integer'Max (High + 1, Low) +
-                            (Max_Length - Low - By'Length)))),
-        Global         => (Proof_In => Max_Length);
+                            (Max_Length - Low - By'Length))));
 
       function Insert
         (Source   : Bounded_String;
@@ -1666,8 +1648,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                       and then Slice (Insert'Result,
                         Before + New_Item'Length, Max_Length) =
                           Slice (Source,
-                            Before, Max_Length - New_Item'Length))),
-        Global         => (Proof_In => Max_Length);
+                            Before, Max_Length - New_Item'Length)));
 
       procedure Insert
         (Source   : in out Bounded_String;
@@ -1780,8 +1761,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                       and then
                         Slice (Source, Before + New_Item'Length, Max_Length) =
                           Slice (Source'Old,
-                            Before, Max_Length - New_Item'Length))),
-        Global         => (Proof_In => Max_Length);
+                            Before, Max_Length - New_Item'Length)));
 
       function Overwrite
         (Source   : Bounded_String;
@@ -1867,8 +1847,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
 
                and then Slice (Overwrite'Result, Position, Max_Length) =
                  New_Item
-                   (New_Item'First .. Max_Length - Position + New_Item'First)),
-        Global         => (Proof_In => Max_Length);
+                   (New_Item'First .. Max_Length - Position + New_Item'First));
 
       procedure Overwrite
         (Source    : in out Bounded_String;
@@ -1953,8 +1932,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
 
                and then Slice (Source, Position, Max_Length) =
                  New_Item
-                   (New_Item'First .. Max_Length - Position + New_Item'First)),
-        Global         => (Proof_In => Max_Length);
+                   (New_Item'First .. Max_Length - Position + New_Item'First));
 
       function Delete
         (Source  : Bounded_String;
@@ -2166,8 +2144,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                and then
                  Slice (Head'Result,
                    Max_Length - Count + Length (Source) + 1, Max_Length) =
-                     (1 .. Count - Length (Source) => Pad)),
-        Global         => (Proof_In => Max_Length);
+                     (1 .. Count - Length (Source) => Pad));
 
       procedure Head
         (Source : in out Bounded_String;
@@ -2225,8 +2202,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                and then
                  Slice (Source,
                    Max_Length - Count + Length (Source'Old) + 1, Max_Length) =
-                     (1 .. Count - Length (Source'Old) => Pad)),
-        Global         => (Proof_In => Max_Length);
+                     (1 .. Count - Length (Source'Old) => Pad));
 
       function Tail
         (Source : Bounded_String;
@@ -2287,8 +2263,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                    (1 .. Count - Length (Source) => Pad)
                and then
                  Slice (Tail'Result, Count - Length (Source) + 1, Max_Length) =
-                   Slice (Source, 1, Max_Length - Count + Length (Source))),
-        Global         => (Proof_In => Max_Length);
+                   Slice (Source, 1, Max_Length - Count + Length (Source)));
 
       procedure Tail
         (Source : in out Bounded_String;
@@ -2351,8 +2326,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                and then
                  Slice (Source, Count - Length (Source'Old) + 1, Max_Length) =
                    Slice (Source'Old,
-                     1, Max_Length - Count + Length (Source'Old))),
-        Global         => (Proof_In => Max_Length);
+                     1, Max_Length - Count + Length (Source'Old)));
 
       ------------------------------------
       -- String Constructor Subprograms --
@@ -2362,48 +2336,44 @@ package Ada.Strings.Bounded with SPARK_Mode is
         (Left  : Natural;
          Right : Character) return Bounded_String
       with
-        Pre    => Left <= Max_Length,
-        Post   => To_String ("*"'Result) = (1 .. Left => Right),
-        Global => Max_Length;
+        Pre  => Left <= Max_Length,
+        Post => To_String ("*"'Result) = (1 .. Left => Right);
 
       function "*"
         (Left  : Natural;
          Right : String) return Bounded_String
       with
-        Pre    => (if Left /= 0 then Right'Length <= Max_Length / Left),
-        Post   =>
+        Pre  => (if Left /= 0 then Right'Length <= Max_Length / Left),
+        Post =>
           Length ("*"'Result) = Left * Right'Length
             and then
               (if Right'Length > 0 then
                  (for all K in 1 .. Left * Right'Length =>
                     Element ("*"'Result, K) =
-                      Right (Right'First + (K - 1) mod Right'Length))),
-        Global => Max_Length;
+                      Right (Right'First + (K - 1) mod Right'Length)));
 
       function "*"
         (Left  : Natural;
          Right : Bounded_String) return Bounded_String
       with
-        Pre    => (if Left /= 0 then Length (Right) <= Max_Length / Left),
-        Post   =>
+        Pre  => (if Left /= 0 then Length (Right) <= Max_Length / Left),
+        Post =>
           Length ("*"'Result) = Left * Length (Right)
             and then
               (if Length (Right) > 0 then
                  (for all K in 1 .. Left * Length (Right) =>
                     Element ("*"'Result, K) =
-                      Element (Right, 1 + (K - 1) mod Length (Right)))),
-        Global => (Proof_In => Max_Length);
+                      Element (Right, 1 + (K - 1) mod Length (Right))));
 
       function Replicate
         (Count : Natural;
          Item  : Character;
          Drop  : Truncation := Error) return Bounded_String
       with
-        Pre    => (if Count > Max_Length then Drop /= Error),
-        Post   =>
+        Pre  => (if Count > Max_Length then Drop /= Error),
+        Post =>
           To_String (Replicate'Result) =
-            (1 .. Natural'Min (Max_Length, Count) => Item),
-        Global => Max_Length;
+            (1 .. Natural'Min (Max_Length, Count) => Item);
 
       function Replicate
         (Count : Natural;
@@ -2437,8 +2407,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                and then
                  (for all K in 1 .. Max_Length =>
                     Element (Replicate'Result, K) =
-                      Item (Item'Last - (Max_Length - K) mod Item'Length))),
-        Global         => Max_Length;
+                      Item (Item'Last - (Max_Length - K) mod Item'Length)));
 
       function Replicate
         (Count : Natural;
@@ -2473,8 +2442,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
                  (for all K in 1 .. Max_Length =>
                     Element (Replicate'Result, K) =
                       Element (Item,
-                        Length (Item) - (Max_Length - K) mod Length (Item)))),
-        Global         => (Proof_In => Max_Length);
+                        Length (Item) - (Max_Length - K) mod Length (Item))));
 
    private
       --  Most of the implementation is in the separate non generic package