diff mbox series

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

Message ID 20210923131229.GA2726990@adacore.com
State New
Headers show
Series [Ada] Remove global parameter in Global contracts of Ada.Strings.Bounded | expand

Commit Message

Pierre-Marie de Rodat Sept. 23, 2021, 1:12 p.m. UTC 
The predefined Ada.Strings.Bounded unit has been annotated SPARK
contracts that reference a local constant:

   generic
      Max : Positive;
   package Generic_Bounded_Length
      Max_Length : constant Positive := Max;
      function XXX return YYY with Global => Max_Length;
      ...

When this unit is instantiated with an plain integer as the Max
parameter, the Global contract will use a constant that has no variable
inputs, which is illegal in SPARK.

This patch removes Global contracts wich reference Max_Length, leaving
their generation to GNATprove. Alternatively, it would have been
possible to replace Max_Length in the Global contracts with Max,
which gets erased by the tool when the actual parameter of an instance
has no variable inputs. This is explained in SPARK RM 6.1.4(19) and
implemented in the flow analysis part of GNATprove. But this solution
forces the use of Max instead of Max_Length everywhere in the code
and functional contracts, so was considered less appealing.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

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

Patch

diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads
--- 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