From 0988829edde6f7357e875ddd2b6ab09de44bea3a Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 27 Jul 2021 15:57:04 +0200 Subject: [PATCH] [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. --- gcc/ada/libgnat/a-strfix.adb | 2 +- gcc/ada/libgnat/a-strfix.ads | 65 +++++++++++--------------------------------- 2 files changed, 17 insertions(+), 50 deletions(-) diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb index 00967c4..e6f882f 100644 --- 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 168a8e0..3555c7d 100644 --- 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. -- 2.7.4