ada: Update contracts on Strings libraries

The contracts of Ada.Strings.Bounded.To_String and
Ada.Strings.Fixed.Delete are updated to reflect the standard spec and to
allow proof of callers.

gcc/ada/

	* libgnat/a-strbou.ads (To_String): Add a postcondition to state
	the value of bounds of the returned string, which helps with proof
	of callers.
	* libgnat/a-strfix.adb (Delete): Fix implementation to produce
	correct result in all cases. For example, returned string should
	always have a lower bound of 1, which was not respected in one
	case. This was not detected by proof, since this code was dead
	according to the too strict precondition.
	* libgnat/a-strfix.ads (Delete): State the correct precondition
	from standard which allows a value of Through beyond the last
	valid index, and also restricts values of From from below. Update
	the Contract_Cases accordingly to allow new values of parameters.

diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads
index 827c0dc7448546552a872c16f5a0718dcd5b46cd..a4830e56b7880880ea5536dd65d762e3e08e0ed4 100644 (file)
--- a/gcc/ada/libgnat/a-strbou.ads
+++ b/gcc/ada/libgnat/a-strbou.ads
@@ -127,6 +127,9 @@ is
       --  * If Drop=Error, then Strings.Length_Error is propagated.
 
       function To_String (Source : Bounded_String) return String with
+        Post   =>
+          To_String'Result'First = 1
+            and then To_String'Result'Length = Length (Source),
         Global => null;
       --  To_String returns the String value with lower bound 1
       --  represented by Source. If B is a Bounded_String, then

diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb
index 901fd60284bc27403808fd8bd972111d90fccb88..2da5367985b8c44c12574d2e3e7ef8155a2b464a 100644 (file)
--- a/gcc/ada/libgnat/a-strfix.adb
+++ b/gcc/ada/libgnat/a-strfix.adb
@@ -266,36 +266,27 @@ package body Ada.Strings.Fixed with SPARK_Mode is
             return Result_Type (Source);
          end;
 
-      elsif From not in Source'Range
-        or else Through > Source'Last
-      then
-         pragma Annotate
-           (CodePeer, False_Positive,
-            "test always false", "self fullfilling prophecy");
-
-         --  In most cases this raises an exception, but the case of deleting
-         --  a null string at the end of the current one is a special-case, and
-         --  reflects the equivalence with Replace_String (RM A.4.3 (86/3)).
-
-         if From = Source'Last + 1 and then From = Through then
-            return Source;
-         else
-            raise Index_Error;
-         end if;
-
       else
          declare
-            Front : constant Integer := From - Source'First;
+            Front_Len     : constant Integer :=
+              Integer'Max (0, From - Source'First);
+            --  Length of prefix of Source copied to result
 
+            Back_Len      : constant Integer :=
+              Integer'Max (0, Source'Last - Through);
+            --  Length of suffix of Source copied to result
+
+            Result_Length : constant Integer := Front_Len + Back_Len;
+            --  Length of result
          begin
-            return Result : String (1 .. Source'Length - (Through - From + 1))
+            return Result : String (1 .. Result_Length)
               with Relaxed_Initialization
             do
-               Result (1 .. Front) :=
+               Result (1 .. Front_Len) :=
                  Source (Source'First .. From - 1);
 
                if Through < Source'Last then
-                  Result (Front + 1 .. Result'Last) :=
+                  Result (Front_Len + 1 .. Result'Last) :=
                     Source (Through + 1 .. Source'Last);
                end if;
             end return;

diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads
index 9d5e9d9234161e3afb77e512ca7967d647f1b944..aed0851493bc396737582801d07356ed9cb97b47 100644 (file)
--- a/gcc/ada/libgnat/a-strfix.ads
+++ b/gcc/ada/libgnat/a-strfix.ads
@@ -1061,9 +1061,9 @@ is
       From    : Positive;
       Through : Natural) return String
    with
-     Pre            => (if From <= Through
-                        then (From in Source'Range
-                                and then Through <= Source'Last)),
+     Pre            => From > Through
+       or else (From - 1 <= Source'Last
+                 and then Through >= Source'First - 1),
 
      --  Lower bound of the returned string is 1
 
@@ -1079,12 +1079,14 @@ is
 
           --  Length of the returned string
 
-          Delete'Result'Length = Source'Length - (Through - From + 1)
+          Delete'Result'Length =
+            Integer'Max (0, From - Source'First)
+            + Integer'Max (Source'Last - Through, 0)
 
             --  Elements before From are preserved
 
             and then
-              Delete'Result (1 .. From - Source'First)
+              Delete'Result (1 .. Integer'Max (0, From - Source'First))
               = Source (Source'First .. From - 1)
 
             --  If there are remaining characters after Through, they are
@@ -1092,9 +1094,11 @@ is
 
             and then
               (if Through < Source'Last
-               then Delete'Result
-                      (From - Source'First + 1 .. Delete'Result'Last)
-                    = Source (Through + 1 .. Source'Last)),
+               then
+                 Delete'Result
+                   (Integer'Max (0, From - Source'First) + 1
+                    .. Delete'Result'Last)
+                 = Source (Through + 1 .. Source'Last)),
 
         --  Otherwise, the returned string is Source with lower bound 1