Use of two nested existential quantications makes proof brittle. Use
instead explicit values for the bounds given by Index_Non_Blank, like
done in Ada.Strings.Bounded.
Tested on x86_64-pc-linux-gnu, committed on trunk
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
--- 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
--- 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.
