diff options
| author | Yannick Moy <moy@adacore.com> | 2021-07-27 15:57:04 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-09-22 15:01:51 +0000 |
| commit | 0988829edde6f7357e875ddd2b6ab09de44bea3a (patch) | |
| tree | 71a100825a37fece2e32835989ff44a35384fcd6 /gcc | |
| parent | dfe93fd5f5a5e271d7f3b03984f837d8597ee3bf (diff) | |
| download | gcc-0988829edde6f7357e875ddd2b6ab09de44bea3a.zip gcc-0988829edde6f7357e875ddd2b6ab09de44bea3a.tar.gz gcc-0988829edde6f7357e875ddd2b6ab09de44bea3a.tar.bz2 | |
[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.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/libgnat/a-strfix.adb | 2 | ||||
| -rw-r--r-- | 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. |