[Ada] Simplify contract of Ada.Strings.Fixed.Trim for proof

gcc/ada/

	* libgnat/a-strfix.ads (Trim): Simplify contracts.
	* libgnat/a-strfix.adb (Trim): Remove white space.

diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb
index 00967c4bb9f0da6d94d6bf870cbf57073023bc2a..e6f882f2799c535396ca5fbba9ccb72b986684e9 100644 (file)
--- a/gcc/ada/libgnat/a-strfix.adb
+++ b/gcc/ada/libgnat/a-strfix.adb
@@ -865,7 +865,7 @@ package body Ada.Strings.Fixed with SPARK_Mode is
       High, Low : Integer;
 
    begin
-      Low := Index (Source, Set => Left, Test  => Outside, Going => Forward);
+      Low := Index (Source, Set => Left, Test => Outside, Going => Forward);
 
       --  Case where source comprises only characters in Left
 

diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads
index 168a8e0dddab77d68666bb39dcbc9e1c3085cc76..3555c7d8e1b0f02bf064fa8a80e68f90af28f340 100644 (file)
--- a/gcc/ada/libgnat/a-strfix.ads
+++ b/gcc/ada/libgnat/a-strfix.ads
@@ -1133,31 +1133,15 @@ package Ada.Strings.Fixed with SPARK_Mode is
             --  Otherwise, the returned string is a slice of Source
 
             else
-              (for some Low in Source'Range =>
-                 (for some High in Source'Range =>
-
-                    --  Trim returns the slice of Source between Low and High
-
-                    Trim'Result = Source (Low .. High)
-
-                      --  Values of Low and High and the characters at their
-                      --  position depend on Side.
-
-                      and then
-                        (if Side = Left then High = Source'Last
-                         else Source (High) /= ' ')
-                      and then
-                        (if Side = Right then Low = Source'First
-                         else Source (Low) /= ' ')
-
-                      --  All characters outside range Low .. High are
-                      --  Space characters.
-
-                      and then
-                        (for all J in Source'Range =>
-                           (if J < Low then Source (J) = ' ')
-                              and then
-                                (if J > High then Source (J) = ' '))))),
+              (declare
+                 Low  : constant Positive :=
+                   (if Side = Right then Source'First
+                    else Index_Non_Blank (Source, Forward));
+                 High : constant Positive :=
+                   (if Side = Left then Source'Last
+                    else Index_Non_Blank (Source, Backward));
+               begin
+                 Trim'Result = Source (Low .. High))),
      Global => null;
    --  Returns the string obtained by removing from Source all leading Space
    --  characters (if Side = Left), all trailing Space characters (if
@@ -1203,30 +1187,13 @@ package Ada.Strings.Fixed with SPARK_Mode is
         --  Otherwise, the returned string is a slice of Source
 
         else
-          (for some Low in Source'Range =>
-             (for some High in Source'Range =>
-
-                --  Trim returns the slice of Source between Low and High
-
-                Trim'Result = Source (Low .. High)
-
-                  --  Characters at the bounds of the returned string are
-                  --  not contained in Left or Right.
-
-                  and then not Ada.Strings.Maps.Is_In (Source (Low), Left)
-                  and then not Ada.Strings.Maps.Is_In (Source (High), Right)
-
-                  --  All characters before Low are contained in Left.
-                  --  All characters after High are contained in Right.
-
-                  and then
-                    (for all K in Source'Range =>
-                       (if K < Low
-                        then
-                          Ada.Strings.Maps.Is_In (Source (K), Left))
-                            and then
-                              (if K > High then
-                               Ada.Strings.Maps.Is_In (Source (K), Right)))))),
+           (declare
+              Low  : constant Positive :=
+                Index (Source, Left, Outside, Forward);
+              High : constant Positive :=
+                Index (Source, Right, Outside, Backward);
+            begin
+              Trim'Result = Source (Low .. High))),
      Global => null;
    --  Returns the string obtained by removing from Source all leading
    --  characters in Left and all trailing characters in Right.