diff mbox series

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

Message ID 20210922151612.GA1908282@adacore.com
State New
Headers show
Series [Ada] Simplify contract of Ada.Strings.Fixed.Trim for proof | expand

Commit Message

Pierre-Marie de Rodat Sept. 22, 2021, 3:16 p.m. UTC 
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 mbox series

Patch

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.