diff options
| -rw-r--r-- | gcc/ada/libgnat/a-strfix.adb | 280 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-strfix.ads | 376 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-strsea.adb | 319 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-strsea.ads | 540 |
4 files changed, 1166 insertions, 349 deletions
diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb index ee72b6b..00967c4 100644 --- a/gcc/ada/libgnat/a-strfix.adb +++ b/gcc/ada/libgnat/a-strfix.adb @@ -38,10 +38,17 @@ -- bounds of function return results were also fixed, and use of & removed for -- efficiency reasons. +-- Ghost code, loop invariants and assertions in this unit are meant for +-- analysis only, not for run-time checking, as it would be too costly +-- otherwise. This is enforced by setting the assertion policy to Ignore. + +pragma Assertion_Policy (Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); + with Ada.Strings.Maps; use Ada.Strings.Maps; -with Ada.Strings.Search; -package body Ada.Strings.Fixed is +package body Ada.Strings.Fixed with SPARK_Mode is ------------------------ -- Search Subprograms -- @@ -146,9 +153,12 @@ package body Ada.Strings.Fixed is Right : Character) return String is begin - return Result : String (1 .. Left) do + return Result : String (1 .. Left) with Relaxed_Initialization do for J in Result'Range loop Result (J) := Right; + pragma Loop_Invariant + (for all K in 1 .. J => + Result (K)'Initialized and then Result (K) = Right); end loop; end return; end "*"; @@ -157,12 +167,82 @@ package body Ada.Strings.Fixed is (Left : Natural; Right : String) return String is - Ptr : Integer := 1; + Ptr : Integer := 0; + + -- Parts of the proof involving manipulations with the modulo operator + -- are complicated for the prover and can't be done automatically in + -- the global subprogram. That's why we isolate them in these two ghost + -- lemmas. + + procedure Lemma_Mod (K : Integer) with + Ghost, + Pre => + Right'Length /= 0 + and then Ptr mod Right'Length = 0 + and then Ptr in 0 .. Natural'Last - Right'Length + and then K in Ptr .. Ptr + Right'Length - 1, + Post => K mod Right'Length = K - Ptr; + -- Lemma_Mod is applied to an index considered in Lemma_Split to prove + -- that it has the right value modulo Right'Length. + + procedure Lemma_Split (Result : String) with + Ghost, + Relaxed_Initialization => Result, + Pre => + Right'Length /= 0 + and then Result'First = 1 + and then Result'Last >= 0 + and then Ptr mod Right'Length = 0 + and then Ptr in 0 .. Result'Last - Right'Length + and then Result (Result'First .. Ptr + Right'Length)'Initialized + and then Result (Ptr + 1 .. Ptr + Right'Length) = Right, + Post => + (for all K in Ptr + 1 .. Ptr + Right'Length => + Result (K) = Right (Right'First + (K - 1) mod Right'Length)); + -- Lemma_Split is used after Result (Ptr + 1 .. Ptr + Right'Length) is + -- updated to Right and concludes that the characters match for each + -- index when taken modulo Right'Length, as the considered slice starts + -- at index 1 modulo Right'Length. + + --------------- + -- Lemma_Mod -- + --------------- + + procedure Lemma_Mod (K : Integer) is null; + + ----------------- + -- Lemma_Split -- + ----------------- + + procedure Lemma_Split (Result : String) is + begin + for K in Ptr + 1 .. Ptr + Right'Length loop + Lemma_Mod (K - 1); + pragma Loop_Invariant + (for all J in Ptr + 1 .. K => + Result (J) = Right (Right'First + (J - 1) mod Right'Length)); + end loop; + end Lemma_Split; + + -- Start of processing for "*" + begin - return Result : String (1 .. Left * Right'Length) do + if Right'Length = 0 then + return ""; + end if; + + return Result : String (1 .. Left * Right'Length) + with Relaxed_Initialization + do for J in 1 .. Left loop - Result (Ptr .. Ptr + Right'Length - 1) := Right; + Result (Ptr + 1 .. Ptr + Right'Length) := Right; + Lemma_Split (Result); Ptr := Ptr + Right'Length; + pragma Loop_Invariant (Ptr = J * Right'Length); + pragma Loop_Invariant (Result (1 .. Ptr)'Initialized); + pragma Loop_Invariant + (for all K in 1 .. Ptr => + Result (K) = Right (Right'First + (K - 1) mod Right'Length)); end loop; end return; end "*"; @@ -176,7 +256,6 @@ package body Ada.Strings.Fixed is From : Positive; Through : Natural) return String is - Front : Integer; begin if From > Through then declare @@ -204,13 +283,22 @@ package body Ada.Strings.Fixed is end if; else - Front := From - Source'First; - return Result : String (1 .. Source'Length - (Through - From + 1)) do - Result (1 .. Front) := - Source (Source'First .. From - 1); - Result (Front + 1 .. Result'Last) := - Source (Through + 1 .. Source'Last); - end return; + declare + Front : constant Integer := From - Source'First; + + begin + return Result : String (1 .. Source'Length - (Through - From + 1)) + with Relaxed_Initialization + do + Result (1 .. Front) := + Source (Source'First .. From - 1); + + if Through < Source'Last then + Result (Front + 1 .. Result'Last) := + Source (Through + 1 .. Source'Last); + end if; + end return; + end; end if; end Delete; @@ -219,8 +307,7 @@ package body Ada.Strings.Fixed is From : Positive; Through : Natural; Justify : Alignment := Left; - Pad : Character := Space) - is + Pad : Character := Space) with SPARK_Mode => Off is begin Move (Source => Delete (Source, From, Through), Target => Source, @@ -240,16 +327,19 @@ package body Ada.Strings.Fixed is subtype Result_Type is String (1 .. Count); begin - if Count < Source'Length then + if Count <= Source'Length then return - Result_Type (Source (Source'First .. Source'First + Count - 1)); + Result_Type (Source (Source'First .. Source'First + (Count - 1))); else - return Result : Result_Type do + return Result : Result_Type with Relaxed_Initialization do Result (1 .. Source'Length) := Source; for J in Source'Length + 1 .. Count loop Result (J) := Pad; + pragma Loop_Invariant + (for all K in Source'Length + 1 .. J => + Result (K)'Initialized and then Result (K) = Pad); end loop; end return; end if; @@ -281,17 +371,31 @@ package body Ada.Strings.Fixed is Front : constant Integer := Before - Source'First; begin - if Before not in Source'First .. Source'Last + 1 then + if Before - 1 not in Source'First - 1 .. Source'Last then raise Index_Error; end if; - return Result : String (1 .. Source'Length + New_Item'Length) do + return Result : String (1 .. Source'Length + New_Item'Length) + with Relaxed_Initialization + do Result (1 .. Front) := Source (Source'First .. Before - 1); Result (Front + 1 .. Front + New_Item'Length) := New_Item; - Result (Front + New_Item'Length + 1 .. Result'Last) := - Source (Before .. Source'Last); + pragma Assert + (Result + (Before - Source'First + 1 + .. Before - Source'First + New_Item'Length) + = New_Item); + + if Before <= Source'Last then + Result (Front + New_Item'Length + 1 .. Result'Last) := + Source (Before .. Source'Last); + end if; + + pragma Assert + (Result (1 .. Before - Source'First) + = Source (Source'First .. Before - 1)); end return; end Insert; @@ -299,8 +403,7 @@ package body Ada.Strings.Fixed is (Source : in out String; Before : Positive; New_Item : String; - Drop : Truncation := Error) - is + Drop : Truncation := Error) with SPARK_Mode => Off is begin Move (Source => Insert (Source, Before, New_Item), Target => Source, @@ -316,7 +419,7 @@ package body Ada.Strings.Fixed is Target : out String; Drop : Truncation := Error; Justify : Alignment := Left; - Pad : Character := Space) + Pad : Character := Space) with SPARK_Mode => Off is Sfirst : constant Integer := Source'First; Slast : constant Integer := Source'Last; @@ -423,7 +526,7 @@ package body Ada.Strings.Fixed is Position : Positive; New_Item : String) return String is begin - if Position not in Source'First .. Source'Last + 1 then + if Position - 1 not in Source'First - 1 .. Source'Last then raise Index_Error; end if; @@ -434,11 +537,32 @@ package body Ada.Strings.Fixed is Front : constant Integer := Position - Source'First; begin - return Result : String (1 .. Result_Length) do + return Result : String (1 .. Result_Length) + with Relaxed_Initialization + do Result (1 .. Front) := Source (Source'First .. Position - 1); + pragma Assert + (Result (1 .. Position - Source'First) + = Source (Source'First .. Position - 1)); Result (Front + 1 .. Front + New_Item'Length) := New_Item; - Result (Front + New_Item'Length + 1 .. Result'Length) := - Source (Position + New_Item'Length .. Source'Last); + pragma Assert + (Result + (Position - Source'First + 1 + .. Position - Source'First + New_Item'Length) + = New_Item); + + if Position <= Source'Last - New_Item'Length then + Result (Front + New_Item'Length + 1 .. Result'Last) := + Source (Position + New_Item'Length .. Source'Last); + end if; + + pragma Assert + (if Position <= Source'Last - New_Item'Length + then + Result + (Position - Source'First + New_Item'Length + 1 + .. Result'Last) + = Source (Position + New_Item'Length .. Source'Last)); end return; end; end Overwrite; @@ -447,8 +571,7 @@ package body Ada.Strings.Fixed is (Source : in out String; Position : Positive; New_Item : String; - Drop : Truncation := Right) - is + Drop : Truncation := Right) with SPARK_Mode => Off is begin Move (Source => Overwrite (Source, Position, New_Item), Target => Source, @@ -463,10 +586,9 @@ package body Ada.Strings.Fixed is (Source : String; Low : Positive; High : Natural; - By : String) return String - is + By : String) return String is begin - if Low > Source'Last + 1 or else High < Source'First - 1 then + if Low - 1 > Source'Last or else High < Source'First - 1 then raise Index_Error; end if; @@ -484,11 +606,34 @@ package body Ada.Strings.Fixed is -- Length of result begin - return Result : String (1 .. Result_Length) do + return Result : String (1 .. Result_Length) + with Relaxed_Initialization do Result (1 .. Front_Len) := Source (Source'First .. Low - 1); + pragma Assert + (Result (1 .. Integer'Max (0, Low - Source'First)) + = Source (Source'First .. Low - 1)); Result (Front_Len + 1 .. Front_Len + By'Length) := By; - Result (Front_Len + By'Length + 1 .. Result'Length) := - Source (High + 1 .. Source'Last); + + if High < Source'Last then + Result (Front_Len + By'Length + 1 .. Result'Last) := + Source (High + 1 .. Source'Last); + end if; + + pragma Assert + (Result (1 .. Integer'Max (0, Low - Source'First)) + = Source (Source'First .. Low - 1)); + pragma Assert + (Result + (Integer'Max (0, Low - Source'First) + 1 + .. Integer'Max (0, Low - Source'First) + By'Length) + = By); + pragma Assert + (if High < Source'Last + then + Result + (Integer'Max (0, Low - Source'First) + By'Length + 1 + .. Result'Last) + = Source (High + 1 .. Source'Last)); end return; end; else @@ -503,8 +648,7 @@ package body Ada.Strings.Fixed is By : String; Drop : Truncation := Error; Justify : Alignment := Left; - Pad : Character := Space) - is + Pad : Character := Space) with SPARK_Mode => Off is begin Move (Replace_Slice (Source, Low, High, By), Source, Drop, Justify, Pad); end Replace_Slice; @@ -521,18 +665,26 @@ package body Ada.Strings.Fixed is subtype Result_Type is String (1 .. Count); begin - if Count < Source'Length then + if Count = 0 then + return ""; + + elsif Count < Source'Length then return Result_Type (Source (Source'Last - Count + 1 .. Source'Last)); -- Pad on left else - return Result : Result_Type do + return Result : Result_Type with Relaxed_Initialization do for J in 1 .. Count - Source'Length loop Result (J) := Pad; + pragma Loop_Invariant + (for all K in 1 .. J => + Result (K)'Initialized and then Result (K) = Pad); end loop; - Result (Count - Source'Length + 1 .. Count) := Source; + if Source'Length /= 0 then + Result (Count - Source'Length + 1 .. Count) := Source; + end if; end return; end if; end Tail; @@ -560,9 +712,18 @@ package body Ada.Strings.Fixed is Mapping : Maps.Character_Mapping) return String is begin - return Result : String (1 .. Source'Length) do + return Result : String (1 .. Source'Length) + with Relaxed_Initialization + do for J in Source'Range loop Result (J - (Source'First - 1)) := Value (Mapping, Source (J)); + pragma Loop_Invariant + (for all K in Source'First .. J => + Result (K - (Source'First - 1))'Initialized); + pragma Loop_Invariant + (for all K in Source'First .. J => + Result (K - (Source'First - 1)) = + Value (Mapping, Source (K))); end loop; end return; end Translate; @@ -574,6 +735,9 @@ package body Ada.Strings.Fixed is begin for J in Source'Range loop Source (J) := Value (Mapping, Source (J)); + pragma Loop_Invariant + (for all K in Source'First .. J => + Source (K) = Value (Mapping, Source'Loop_Entry (K))); end loop; end Translate; @@ -583,9 +747,17 @@ package body Ada.Strings.Fixed is is pragma Unsuppress (Access_Check); begin - return Result : String (1 .. Source'Length) do + return Result : String (1 .. Source'Length) + with Relaxed_Initialization + do for J in Source'Range loop Result (J - (Source'First - 1)) := Mapping.all (Source (J)); + pragma Loop_Invariant + (for all K in Source'First .. J => + Result (K - (Source'First - 1))'Initialized); + pragma Loop_Invariant + (for all K in Source'First .. J => + Result (K - (Source'First - 1)) = Mapping (Source (K))); end loop; end return; end Translate; @@ -598,6 +770,9 @@ package body Ada.Strings.Fixed is begin for J in Source'Range loop Source (J) := Mapping.all (Source (J)); + pragma Loop_Invariant + (for all K in Source'First .. J => + Source (K) = Mapping (Source'Loop_Entry (K))); end loop; end Translate; @@ -609,6 +784,9 @@ package body Ada.Strings.Fixed is (Source : String; Side : Trim_End) return String is + Empty_String : constant String (1 .. 0) := ""; + -- Without declaring the empty string as a separate string starting + -- at 1, SPARK provers have trouble proving the postcondition. begin case Side is when Strings.Left => @@ -618,7 +796,7 @@ package body Ada.Strings.Fixed is -- All blanks case if Low = 0 then - return ""; + return Empty_String; end if; declare @@ -635,7 +813,7 @@ package body Ada.Strings.Fixed is -- All blanks case if High = 0 then - return ""; + return Empty_String; end if; declare @@ -652,7 +830,7 @@ package body Ada.Strings.Fixed is -- All blanks case if Low = 0 then - return ""; + return Empty_String; end if; declare @@ -695,8 +873,7 @@ package body Ada.Strings.Fixed is return ""; end if; - High := - Index (Source, Set => Right, Test => Outside, Going => Backward); + High := Index (Source, Set => Right, Test => Outside, Going => Backward); -- Case where source comprises only characters in Right @@ -705,7 +882,8 @@ package body Ada.Strings.Fixed is end if; declare - subtype Result_Type is String (1 .. High - Low + 1); + Result_Length : constant Integer := High - Low + 1; + subtype Result_Type is String (1 .. Result_Length); begin return Result_Type (Source (Low .. High)); diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads index 4214157..1a5ee94 100644 --- a/gcc/ada/libgnat/a-strfix.ads +++ b/gcc/ada/libgnat/a-strfix.ads @@ -13,14 +13,6 @@ -- -- ------------------------------------------------------------------------------ --- Preconditions in this unit are meant for analysis only, not for run-time --- checking, so that the expected exceptions are raised. This is enforced by --- setting the corresponding assertion policy to Ignore. - -pragma Assertion_Policy (Pre => Ignore); - -with Ada.Strings.Maps; - -- The language-defined package Strings.Fixed provides string-handling -- subprograms for fixed-length strings; that is, for values of type -- Standard.String. Several of these subprograms are procedures that modify @@ -40,6 +32,20 @@ with Ada.Strings.Maps; -- these effects. Similar control is provided by the string transformation -- procedures. +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. This is enforced by +-- setting the corresponding assertion policy to Ignore. Postconditions and +-- contract cases should not be executed at runtime as well, in order not to +-- slow down the execution of these functions. + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore); + +with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; +with Ada.Strings.Search; + package Ada.Strings.Fixed with SPARK_Mode is pragma Preelaborate; @@ -108,56 +114,60 @@ package Ada.Strings.Fixed with SPARK_Mode is Going : Direction := Forward; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => - Pattern'Length /= 0 - and then (if Source'Length /= 0 then From in Source'Range), + Pre => Pattern'Length > 0 + and then Mapping /= null + and then (if Source'Length > 0 then From in Source'Range), Post => Index'Result in 0 | Source'Range, Contract_Cases => - -- If no slice in the considered range of Source matches Pattern, - -- then 0 is returned. + -- If Source is the empty string, then 0 is returned - ((for all J in Source'Range => - (if (if Going = Forward - then J in From .. Source'Last - Pattern'Length + 1 - else J <= From - Pattern'Length + 1) - then Translate (Source (J .. J - 1 + Pattern'Length), Mapping) - /= Pattern)) + (Source'Length = 0 => Index'Result = 0, - -- Otherwise, a valid index is returned + -- If some slice of Source matches Pattern, then a valid index is + -- returned. - others + Source'Length > 0 + and then + (for some J in + (if Going = Forward then From else Source'First) + .. (if Going = Forward then Source'Last else From) + - (Pattern'Length - 1) => + Ada.Strings.Search.Match (Source, Pattern, Mapping, J)) => - -- The result is in the considered range of Source - (if Going = Forward - then Index'Result in From .. Source'Last - Pattern'Length + 1 - else Index'Result in Source'First .. From - Pattern'Length + 1) + Index'Result in + (if Going = Forward then From else Source'First) + .. (if Going = Forward then Source'Last else From) + - (Pattern'Length - 1) -- The slice beginning at the returned index matches Pattern and then - Translate (Source (Index'Result - .. Index'Result - 1 + Pattern'Length), - Mapping) - = Pattern + Ada.Strings.Search.Match (Source, Pattern, Mapping, Index'Result) - -- The result is the smallest or largest index which satisfies the - -- matching, respectively when Going = Forward and - -- Going = Backwards. + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. and then (for all J in Source'Range => (if (if Going = Forward then J in From .. Index'Result - 1 - else J - 1 in Index'Result .. From - Pattern'Length) - then Translate (Source (J .. J - 1 + Pattern'Length), - Mapping) - /= Pattern))), + else J - 1 in Index'Result + .. From - Pattern'Length) + then not (Ada.Strings.Search.Match + (Source, Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others + => + Index'Result = 0), Global => null; pragma Ada_05 (Index); @@ -168,56 +178,59 @@ package Ada.Strings.Fixed with SPARK_Mode is Going : Direction := Forward; Mapping : Maps.Character_Mapping := Maps.Identity) return Natural with - Pre => - Pattern'Length /= 0 - and then (if Source'Length /= 0 then From in Source'Range), + Pre => Pattern'Length > 0 + and then (if Source'Length > 0 then From in Source'Range), Post => Index'Result in 0 | Source'Range, Contract_Cases => - -- If no slice in the considered range of Source matches Pattern, - -- then 0 is returned. + -- If Source is the empty string, then 0 is returned - ((for all J in Source'Range => - (if (if Going = Forward - then J in From .. Source'Last - Pattern'Length + 1 - else J <= From - Pattern'Length + 1) - then Translate (Source (J .. J - 1 + Pattern'Length), Mapping) - /= Pattern)) + (Source'Length = 0 => Index'Result = 0, - -- Otherwise, a valid index is returned + -- If some slice of Source matches Pattern, then a valid index is + -- returned. - others + Source'Length > 0 + and then + (for some J in + (if Going = Forward then From else Source'First) + .. (if Going = Forward then Source'Last else From) + - (Pattern'Length - 1) => + Ada.Strings.Search.Match (Source, Pattern, Mapping, J)) => - -- The result is in the considered range of Source - (if Going = Forward - then Index'Result in From .. Source'Last - Pattern'Length + 1 - else Index'Result in Source'First .. From - Pattern'Length + 1) + Index'Result in + (if Going = Forward then From else Source'First) + .. (if Going = Forward then Source'Last else From) + - (Pattern'Length - 1) - -- The slice beginning at the returned index matches Pattern + -- The slice beginning at the returned index matches Pattern - and then - Translate (Source (Index'Result - .. Index'Result - 1 + Pattern'Length), - Mapping) - = Pattern + and then + Ada.Strings.Search.Match (Source, Pattern, Mapping, Index'Result) -- The result is the smallest or largest index which satisfies the -- matching, respectively when Going = Forward and - -- Going = Backwards. + -- Going = Backward. and then (for all J in Source'Range => (if (if Going = Forward then J in From .. Index'Result - 1 - else J - 1 in Index'Result .. From - Pattern'Length) - then Translate (Source (J .. J - 1 + Pattern'Length), - Mapping) - /= Pattern))), + else J - 1 in Index'Result + .. From - Pattern'Length) + then not (Ada.Strings.Search.Match + (Source, Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others + => + Index'Result = 0), Global => null; pragma Ada_05 (Index); @@ -245,37 +258,33 @@ package Ada.Strings.Fixed with SPARK_Mode is Post => Index'Result in 0 | Source'Range, Contract_Cases => - -- If Source is empty, or if no slice of Source matches Pattern, then - -- 0 is returned. + -- If Source is the empty string, then 0 is returned (Source'Length = 0 - or else - (for all J in Source'First .. Source'Last - Pattern'Length + 1 => - Translate (Source (J .. J - 1 + Pattern'Length), Mapping) - /= Pattern) => Index'Result = 0, - -- Otherwise, a valid index is returned + -- If some slice of Source matches Pattern, then a valid index is + -- returned. - others + Source'Length > 0 + and then + (for some J in + Source'First .. Source'Last - (Pattern'Length - 1) => + Ada.Strings.Search.Match (Source, Pattern, Mapping, J)) => - -- The result is in the considered range of Source - Index'Result in Source'First .. Source'Last - Pattern'Length + 1 + Index'Result in Source'First .. Source'Last - (Pattern'Length - 1) -- The slice beginning at the returned index matches Pattern and then - Translate (Source (Index'Result - .. Index'Result - 1 + Pattern'Length), - Mapping) - = Pattern + Ada.Strings.Search.Match (Source, Pattern, Mapping, Index'Result) - -- The result is the smallest or largest index which satisfies the - -- matching, respectively when Going = Forward and - -- Going = Backwards. + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. and then (for all J in Source'Range => @@ -283,9 +292,14 @@ package Ada.Strings.Fixed with SPARK_Mode is then J <= Index'Result - 1 else J - 1 in Index'Result .. Source'Last - Pattern'Length) - then Translate (Source (J .. J - 1 + Pattern'Length), - Mapping) - /= Pattern))), + then not (Ada.Strings.Search.Match + (Source, Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others + => + Index'Result = 0), Global => null; function Index @@ -294,42 +308,38 @@ package Ada.Strings.Fixed with SPARK_Mode is Going : Direction := Forward; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => Pattern'Length > 0, + Pre => Pattern'Length > 0 and then Mapping /= null, Post => Index'Result in 0 | Source'Range, Contract_Cases => - -- If Source is empty, or if no slice of Source matches Pattern, then - -- 0 is returned. + -- If Source is the empty string, then 0 is returned (Source'Length = 0 - or else - (for all J in Source'First .. Source'Last - Pattern'Length + 1 => - Translate (Source (J .. J - 1 + Pattern'Length), Mapping) - /= Pattern) => Index'Result = 0, - -- Otherwise, a valid index is returned + -- If some slice of Source matches Pattern, then a valid index is + -- returned. - others + Source'Length > 0 + and then + (for some J in + Source'First .. Source'Last - (Pattern'Length - 1) => + Ada.Strings.Search.Match (Source, Pattern, Mapping, J)) => - -- The result is in the considered range of Source - Index'Result in Source'First .. Source'Last - Pattern'Length + 1 + Index'Result in Source'First .. Source'Last - (Pattern'Length - 1) - -- The slice beginning at the returned index matches Pattern + -- The slice beginning at the returned index matches Pattern - and then - Translate (Source (Index'Result - .. Index'Result - 1 + Pattern'Length), - Mapping) - = Pattern + and then + Ada.Strings.Search.Match (Source, Pattern, Mapping, Index'Result) - -- The result is the smallest or largest index which satisfies the - -- matching, respectively when Going = Forward and - -- Going = Backwards. + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. and then (for all J in Source'Range => @@ -337,9 +347,14 @@ package Ada.Strings.Fixed with SPARK_Mode is then J <= Index'Result - 1 else J - 1 in Index'Result .. Source'Last - Pattern'Length) - then Translate (Source (J .. J - 1 + Pattern'Length), - Mapping) - /= Pattern))), + then not (Ada.Strings.Search.Match + (Source, Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others + => + Index'Result = 0), Global => null; -- If Going = Forward, returns: @@ -383,9 +398,9 @@ package Ada.Strings.Fixed with SPARK_Mode is (Test = Inside) = Ada.Strings.Maps.Is_In (Source (Index'Result), Set) - -- The result is the smallest or largest index which satisfies the - -- property, respectively when Going = Forward and - -- Going = Backwards. + -- The result is the smallest or largest index which satisfies + -- the property, respectively when Going = Forward and Going = + -- Backward. and then (for all J in Source'Range => @@ -402,22 +417,23 @@ package Ada.Strings.Fixed with SPARK_Mode is Test : Membership := Inside; Going : Direction := Forward) return Natural with - Pre => (if Source'Length /= 0 then From in Source'Range), - + Pre => (if Source'Length > 0 then From in Source'Range), Post => Index'Result in 0 | Source'Range, Contract_Cases => - -- If no character in the considered slice of Source satisfies the - -- property Test on Set, then 0 is returned. + -- If Source is the empty string, or no character of the considered + -- slice of Source satisfies the property Test on Set, then 0 is + -- returned. - ((for all I in Source'Range => - (if I = From - or else (I > From) = (Going = Forward) - then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (I), Set))) + (Source'Length = 0 + or else + (for all J in Source'Range => + (if J = From or else (J > From) = (Going = Forward) then + (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (J), Set))) => Index'Result = 0, - -- Otherwise, an index in the range of Source is returned + -- Otherwise, a index in the considered range of Source is returned others => @@ -426,7 +442,8 @@ package Ada.Strings.Fixed with SPARK_Mode is Index'Result in Source'Range and then (Index'Result = From - or else (Index'Result > From) = (Going = Forward)) + or else + (Index'Result > From) = (Going = Forward)) -- The character at the returned index satisfies the property -- Test on Set. @@ -435,19 +452,18 @@ package Ada.Strings.Fixed with SPARK_Mode is (Test = Inside) = Ada.Strings.Maps.Is_In (Source (Index'Result), Set) - -- The result is the smallest or largest index which satisfies the - -- property, respectively when Going = Forward and - -- Going = Backwards. + -- The result is the smallest or largest index which satisfies + -- the property, respectively when Going = Forward and Going = + -- Backward. and then (for all J in Source'Range => (if J /= Index'Result - and then (J < Index'Result) = (Going = Forward) - and then (J = From - or else (J > From) = (Going = Forward)) - then - (Test = Inside) - /= Ada.Strings.Maps.Is_In (Source (J), Set)))), + and then (J < Index'Result) = (Going = Forward) + and then (J = From + or else (J > From) = (Going = Forward)) + then (Test = Inside) + /= Ada.Strings.Maps.Is_In (Source (J), Set)))), Global => null; pragma Ada_05 (Index); -- Index searches for the first or last occurrence of any of a set of @@ -469,12 +485,14 @@ package Ada.Strings.Fixed with SPARK_Mode is Post => Index_Non_Blank'Result in 0 | Source'Range, Contract_Cases => - -- If all characters in the considered slice of Source are Space - -- characters, then 0 is returned. + -- If Source is the empty string, or all characters in the considered + -- slice of Source are Space characters, then 0 is returned. - ((for all J in Source'Range => - (if J = From or else (J > From) = (Going = Forward) - then Source (J) = ' ')) + (Source'Length = 0 + or else + (for all J in Source'Range => + (if J = From or else (J > From) = (Going = Forward) then + Source (J) = ' ')) => Index_Non_Blank'Result = 0, @@ -496,7 +514,7 @@ package Ada.Strings.Fixed with SPARK_Mode is -- The result is the smallest or largest index which is not a -- Space character, respectively when Going = Forward and - -- Going = Backwards. + -- Going = Backward. and then (for all J in Source'Range => @@ -535,8 +553,8 @@ package Ada.Strings.Fixed with SPARK_Mode is and then Source (Index_Non_Blank'Result) /= ' ' -- The result is the smallest or largest index which is not a - -- Space character, respectively when Going = Forward and - -- Going = Backwards. + -- Space character, respectively when Going = Forward and Going + -- = Backward. and then (for all J in Source'Range => @@ -560,7 +578,7 @@ package Ada.Strings.Fixed with SPARK_Mode is Pattern : String; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => Pattern'Length /= 0, + Pre => Pattern'Length /= 0 and then Mapping /= null, Global => null; -- Returns the maximum number of nonoverlapping slices of Source that match @@ -646,6 +664,7 @@ package Ada.Strings.Fixed with SPARK_Mode is First : out Positive; Last : out Natural) with + Pre => Source'First > 0, Contract_Cases => -- If Source is the empty string, or if no character of Source @@ -701,6 +720,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : String; Mapping : Maps.Character_Mapping_Function) return String with + Pre => Mapping /= null, Post => -- Lower bound of the returned string is 1 @@ -751,10 +771,11 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : in out String; Mapping : Maps.Character_Mapping_Function) with + Pre => Mapping /= null, Post => - -- Each character in Source after the call is the translation of - -- the character at the same position before the call, through Mapping. + -- Each character in Source after the call is the translation of the + -- character at the same position before the call, through Mapping. (for all J in Source'Range => Source (J) = Mapping (Source'Old (J))), Global => null; @@ -765,8 +786,8 @@ package Ada.Strings.Fixed with SPARK_Mode is with Post => - -- Each character in Source after the call is the translation of - -- the character at the same position before the call, through Mapping. + -- Each character in Source after the call is the translation of the + -- character at the same position before the call, through Mapping. (for all J in Source'Range => Source (J) = Ada.Strings.Maps.Value (Mapping, Source'Old (J))), @@ -778,32 +799,6 @@ package Ada.Strings.Fixed with SPARK_Mode is -- String Transformation Subprograms -- --------------------------------------- - procedure Replace_Slice - (Source : in out String; - Low : Positive; - High : Natural; - By : String; - Drop : Truncation := Error; - Justify : Alignment := Left; - Pad : Character := Space) - with - Pre => - - -- Incomplete contract - - Low - 1 <= Source'Last - and then High >= Source'First - 1, - Global => null; - -- If Low > Source'Last+1, or High < Source'First - 1, then Index_Error is - -- propagated. Otherwise: - -- - -- * If High >= Low, then the returned string comprises - -- Source (Source'First .. Low - 1) - -- & By & Source(High + 1 .. Source'Last), but with lower bound 1. - -- - -- * If High < Low, then the returned string is - -- Insert (Source, Before => Low, New_Item => By). - function Replace_Slice (Source : String; Low : Positive; @@ -834,19 +829,19 @@ package Ada.Strings.Fixed with SPARK_Mode is -- Length of the returned string Replace_Slice'Result'Length - = Natural'Max (0, Low - Source'First) + = Integer'Max (0, Low - Source'First) + By'Length - + Natural'Max (Source'Last - High, 0) + + Integer'Max (Source'Last - High, 0) -- Elements starting at Low are replaced by elements of By and then - Replace_Slice'Result (1 .. Natural'Max (0, Low - Source'First)) + Replace_Slice'Result (1 .. Integer'Max (0, Low - Source'First)) = Source (Source'First .. Low - 1) and then Replace_Slice'Result - (Natural'Max (0, Low - Source'First) + 1 - .. Natural'Max (0, Low - Source'First) + By'Length) + (Integer'Max (0, Low - Source'First) + 1 + .. Integer'Max (0, Low - Source'First) + By'Length) = By -- When there are remaining characters after the replaced slice, @@ -856,7 +851,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (if High < Source'Last then Replace_Slice'Result - (Natural'Max (0, Low - Source'First) + By'Length + 1 + (Integer'Max (0, Low - Source'First) + By'Length + 1 .. Replace_Slice'Result'Last) = Source (High + 1 .. Source'Last)), @@ -890,6 +885,30 @@ package Ada.Strings.Fixed with SPARK_Mode is .. Replace_Slice'Result'Last) = Source (Low .. Source'Last))), Global => null; + -- If Low > Source'Last + 1, or High < Source'First - 1, then Index_Error + -- is propagated. Otherwise: + -- + -- * If High >= Low, then the returned string comprises + -- Source (Source'First .. Low - 1) + -- & By & Source(High + 1 .. Source'Last), but with lower bound 1. + -- + -- * If High < Low, then the returned string is + -- Insert (Source, Before => Low, New_Item => By). + + procedure Replace_Slice + (Source : in out String; + Low : Positive; + High : Natural; + By : String; + Drop : Truncation := Error; + Justify : Alignment := Left; + Pad : Character := Space) + with + Pre => Low - 1 <= Source'Last, + + -- Incomplete contract + + Global => null; -- Equivalent to: -- -- Move (Replace_Slice (Source, Low, High, By), @@ -929,7 +948,7 @@ package Ada.Strings.Fixed with SPARK_Mode is -- are appended to the returned string. and then - (if Before - 1 < Source'Last + (if Before <= Source'Last then Insert'Result (Before - Source'First + New_Item'Length + 1 @@ -937,7 +956,7 @@ package Ada.Strings.Fixed with SPARK_Mode is = Source (Before .. Source'Last)), Global => null; -- Propagates Index_Error if Before is not in - -- Source'First .. Source'Last+1; otherwise, returns + -- Source'First .. Source'Last + 1; otherwise, returns -- Source (Source'First .. Before - 1) -- & New_Item & Source(Before..Source'Last), but with lower bound 1. @@ -1384,9 +1403,8 @@ package Ada.Strings.Fixed with SPARK_Mode is -- Content of the string is Right concatenated with itself Left times and then - (for all J in 0 .. Left - 1 => - "*"'Result (J * Right'Length + 1 .. (J + 1) * Right'Length) - = Right), + (for all K in "*"'Result'Range => + "*"'Result (K) = Right (Right'First + (K - 1) mod Right'Length)), Global => null; -- These functions replicate a character or string a specified number of diff --git a/gcc/ada/libgnat/a-strsea.adb b/gcc/ada/libgnat/a-strsea.adb index d96a4c7..243c92c 100644 --- a/gcc/ada/libgnat/a-strsea.adb +++ b/gcc/ada/libgnat/a-strsea.adb @@ -35,10 +35,18 @@ -- case of identity mappings for Count and Index, and also Index_Non_Blank -- is specialized (rather than using the general Index routine). +-- Ghost code, loop invariants and assertions in this unit are meant for +-- analysis only, not for run-time checking, as it would be too costly +-- otherwise. This is enforced by setting the assertion policy to Ignore. + +pragma Assertion_Policy (Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); + with Ada.Strings.Maps; use Ada.Strings.Maps; with System; use System; -package body Ada.Strings.Search is +package body Ada.Strings.Search with SPARK_Mode is ----------------------- -- Local Subprograms -- @@ -61,13 +69,9 @@ package body Ada.Strings.Search is Set : Maps.Character_Set; Test : Membership) return Boolean is - begin - if Test = Inside then - return Is_In (Element, Set); - else - return not Is_In (Element, Set); - end if; - end Belongs; + (if Test = Inside then + Is_In (Element, Set) + else not (Is_In (Element, Set))); ----------- -- Count -- @@ -81,47 +85,63 @@ package body Ada.Strings.Search is PL1 : constant Integer := Pattern'Length - 1; Num : Natural; Ind : Natural; - Cur : Natural; begin if Pattern = "" then raise Pattern_Error; end if; + -- Isolating the null string case to ensure Source'First, Source'Last in + -- Positive. + + if Source = "" then + return 0; + end if; + Num := 0; - Ind := Source'First; + Ind := Source'First - 1; -- Unmapped case - if Mapping'Address = Maps.Identity'Address then - while Ind <= Source'Last - PL1 loop + if Is_Identity (Mapping) then + while Ind < Source'Last - PL1 loop + Ind := Ind + 1; if Pattern = Source (Ind .. Ind + PL1) then Num := Num + 1; - Ind := Ind + Pattern'Length; - else - Ind := Ind + 1; + Ind := Ind + PL1; end if; + + pragma Loop_Invariant (Num <= Ind - (Source'First - 1)); + pragma Loop_Invariant (Ind >= Source'First); end loop; -- Mapped case else - while Ind <= Source'Last - PL1 loop - Cur := Ind; + while Ind < Source'Last - PL1 loop + Ind := Ind + 1; for K in Pattern'Range loop - if Pattern (K) /= Value (Mapping, Source (Cur)) then - Ind := Ind + 1; + if Pattern (K) /= Value (Mapping, + Source (Ind + (K - Pattern'First))) + then + pragma Assert (not (Match (Source, Pattern, Mapping, Ind))); goto Cont; - else - Cur := Cur + 1; end if; + + pragma Loop_Invariant + (for all J in Pattern'First .. K => + Pattern (J) = Value (Mapping, + Source (Ind + (J - Pattern'First)))); end loop; + pragma Assert (Match (Source, Pattern, Mapping, Ind)); Num := Num + 1; - Ind := Ind + Pattern'Length; + Ind := Ind + PL1; - <<Cont>> + <<Cont>> null; + pragma Loop_Invariant (Num <= Ind - (Source'First - 1)); + pragma Loop_Invariant (Ind >= Source'First); end loop; end if; @@ -138,13 +158,19 @@ package body Ada.Strings.Search is PL1 : constant Integer := Pattern'Length - 1; Num : Natural; Ind : Natural; - Cur : Natural; begin if Pattern = "" then raise Pattern_Error; end if; + -- Isolating the null string case to ensure Source'First, Source'Last in + -- Positive. + + if Source = "" then + return 0; + end if; + -- Check for null pointer in case checks are off if Mapping = null then @@ -152,23 +178,28 @@ package body Ada.Strings.Search is end if; Num := 0; - Ind := Source'First; - while Ind <= Source'Last - PL1 loop - Cur := Ind; + Ind := Source'First - 1; + while Ind < Source'Last - PL1 loop + Ind := Ind + 1; for K in Pattern'Range loop - if Pattern (K) /= Mapping (Source (Cur)) then - Ind := Ind + 1; + if Pattern (K) /= Mapping (Source (Ind + (K - Pattern'First))) then + pragma Assert (not (Match (Source, Pattern, Mapping, Ind))); goto Cont; - else - Cur := Cur + 1; end if; + + pragma Loop_Invariant + (for all J in Pattern'First .. K => + Pattern (J) = Mapping (Source (Ind + (J - Pattern'First)))); end loop; + pragma Assert (Match (Source, Pattern, Mapping, Ind)); Num := Num + 1; - Ind := Ind + Pattern'Length; + Ind := Ind + PL1; <<Cont>> null; + pragma Loop_Invariant (Num <= Ind - (Source'First - 1)); + pragma Loop_Invariant (Ind >= Source'First); end loop; return Num; @@ -182,6 +213,7 @@ package body Ada.Strings.Search is begin for J in Source'Range loop + pragma Loop_Invariant (N <= J - Source'First); if Is_In (Source (J), Set) then N := N + 1; end if; @@ -217,12 +249,18 @@ package body Ada.Strings.Search is if Belongs (Source (J), Set, Test) then First := J; - for K in J + 1 .. Source'Last loop - if not Belongs (Source (K), Set, Test) then - Last := K - 1; - return; - end if; - end loop; + if J < Source'Last then + for K in J + 1 .. Source'Last loop + if not Belongs (Source (K), Set, Test) then + Last := K - 1; + return; + end if; + + pragma Loop_Invariant + (for all L in J .. K => + Belongs (Source (L), Set, Test)); + end loop; + end if; -- Here if J indexes first char of token, and all chars after J -- are in the token. @@ -230,6 +268,10 @@ package body Ada.Strings.Search is Last := Source'Last; return; end if; + + pragma Loop_Invariant + (for all K in Integer'Max (From, Source'First) .. J => + not (Belongs (Source (K), Set, Test))); end loop; -- Here if no token found @@ -250,12 +292,18 @@ package body Ada.Strings.Search is if Belongs (Source (J), Set, Test) then First := J; - for K in J + 1 .. Source'Last loop - if not Belongs (Source (K), Set, Test) then - Last := K - 1; - return; - end if; - end loop; + if J < Source'Last then + for K in J + 1 .. Source'Last loop + if not Belongs (Source (K), Set, Test) then + Last := K - 1; + return; + end if; + + pragma Loop_Invariant + (for all L in J .. K => + Belongs (Source (L), Set, Test)); + end loop; + end if; -- Here if J indexes first char of token, and all chars after J -- are in the token. @@ -263,6 +311,10 @@ package body Ada.Strings.Search is Last := Source'Last; return; end if; + + pragma Loop_Invariant + (for all K in Source'First .. J => + not (Belongs (Source (K), Set, Test))); end loop; -- Here if no token found @@ -292,53 +344,61 @@ package body Ada.Strings.Search is Mapping : Maps.Character_Mapping := Maps.Identity) return Natural is PL1 : constant Integer := Pattern'Length - 1; - Cur : Natural; - - Ind : Integer; - -- Index for start of match check. This can be negative if the pattern - -- length is greater than the string length, which is why this variable - -- is Integer instead of Natural. In this case, the search loops do not - -- execute at all, so this Ind value is never used. begin if Pattern = "" then raise Pattern_Error; end if; + -- If Pattern is longer than Source, it can't be found + + if Pattern'Length > Source'Length then + return 0; + end if; + -- Forwards case if Going = Forward then - Ind := Source'First; -- Unmapped forward case - if Mapping'Address = Maps.Identity'Address then - for J in 1 .. Source'Length - PL1 loop + if Is_Identity (Mapping) then + for Ind in Source'First .. Source'Last - PL1 loop if Pattern = Source (Ind .. Ind + PL1) then + pragma Assert (Match (Source, Pattern, Mapping, Ind)); return Ind; - else - Ind := Ind + 1; end if; + + pragma Loop_Invariant + (for all J in Source'First .. Ind => + not (Match (Source, Pattern, Mapping, J))); end loop; -- Mapped forward case else - for J in 1 .. Source'Length - PL1 loop - Cur := Ind; - + for Ind in Source'First .. Source'Last - PL1 loop for K in Pattern'Range loop - if Pattern (K) /= Value (Mapping, Source (Cur)) then + if Pattern (K) /= Value (Mapping, + Source (Ind + (K - Pattern'First))) + then goto Cont1; - else - Cur := Cur + 1; end if; + + pragma Loop_Invariant + (for all J in Pattern'First .. K => + Pattern (J) = Value (Mapping, + Source (Ind + (J - Pattern'First)))); end loop; + pragma Assert (Match (Source, Pattern, Mapping, Ind)); return Ind; - <<Cont1>> - Ind := Ind + 1; + <<Cont1>> + pragma Loop_Invariant + (for all J in Source'First .. Ind => + not (Match (Source, Pattern, Mapping, J))); + null; end loop; end if; @@ -347,35 +407,43 @@ package body Ada.Strings.Search is else -- Unmapped backward case - Ind := Source'Last - PL1; - - if Mapping'Address = Maps.Identity'Address then - for J in reverse 1 .. Source'Length - PL1 loop + if Is_Identity (Mapping) then + for Ind in reverse Source'First .. Source'Last - PL1 loop if Pattern = Source (Ind .. Ind + PL1) then + pragma Assert (Match (Source, Pattern, Mapping, Ind)); return Ind; - else - Ind := Ind - 1; end if; + + pragma Loop_Invariant + (for all J in Ind .. Source'Last - PL1 => + not (Match (Source, Pattern, Mapping, J))); end loop; -- Mapped backward case else - for J in reverse 1 .. Source'Length - PL1 loop - Cur := Ind; - + for Ind in reverse Source'First .. Source'Last - PL1 loop for K in Pattern'Range loop - if Pattern (K) /= Value (Mapping, Source (Cur)) then + if Pattern (K) /= Value (Mapping, + Source (Ind + (K - Pattern'First))) + then goto Cont2; - else - Cur := Cur + 1; end if; + + pragma Loop_Invariant + (for all J in Pattern'First .. K => + Pattern (J) = Value (Mapping, + Source (Ind + (J - Pattern'First)))); end loop; + pragma Assert (Match (Source, Pattern, Mapping, Ind)); return Ind; - <<Cont2>> - Ind := Ind - 1; + <<Cont2>> + pragma Loop_Invariant + (for all J in Ind .. Source'Last - PL1 => + not (Match (Source, Pattern, Mapping, J))); + null; end loop; end if; end if; @@ -393,9 +461,6 @@ package body Ada.Strings.Search is Mapping : Maps.Character_Mapping_Function) return Natural is PL1 : constant Integer := Pattern'Length - 1; - Ind : Natural; - Cur : Natural; - begin if Pattern = "" then raise Pattern_Error; @@ -416,43 +481,52 @@ package body Ada.Strings.Search is -- Forwards case if Going = Forward then - Ind := Source'First; - for J in 1 .. Source'Length - PL1 loop - Cur := Ind; - + for Ind in Source'First .. Source'Last - PL1 loop for K in Pattern'Range loop - if Pattern (K) /= Mapping.all (Source (Cur)) then + if Pattern (K) /= Mapping.all + (Source (Ind + (K - Pattern'First))) + then goto Cont1; - else - Cur := Cur + 1; end if; + + pragma Loop_Invariant + (for all J in Pattern'First .. K => + Pattern (J) = Mapping (Source (Ind + (J - Pattern'First)))); end loop; + pragma Assert (Match (Source, Pattern, Mapping, Ind)); return Ind; - <<Cont1>> - Ind := Ind + 1; + <<Cont1>> + pragma Loop_Invariant + (for all J in Source'First .. Ind => + not (Match (Source, Pattern, Mapping, J))); + null; end loop; -- Backwards case else - Ind := Source'Last - PL1; - for J in reverse 1 .. Source'Length - PL1 loop - Cur := Ind; - + for Ind in reverse Source'First .. Source'Last - PL1 loop for K in Pattern'Range loop - if Pattern (K) /= Mapping.all (Source (Cur)) then + if Pattern (K) /= Mapping.all + (Source (Ind + (K - Pattern'First))) + then goto Cont2; - else - Cur := Cur + 1; end if; + + pragma Loop_Invariant + (for all J in Pattern'First .. K => + Pattern (J) = Mapping (Source (Ind + (J - Pattern'First)))); end loop; return Ind; - <<Cont2>> - Ind := Ind - 1; + <<Cont2>> + pragma Loop_Invariant + (for all J in Ind .. (Source'Last - PL1) => + not (Match (Source, Pattern, Mapping, J))); + null; end loop; end if; @@ -476,6 +550,10 @@ package body Ada.Strings.Search is if Belongs (Source (J), Set, Test) then return J; end if; + + pragma Loop_Invariant + (for all C of Source (Source'First .. J) => + not (Belongs (C, Set, Test))); end loop; -- Backwards case @@ -485,6 +563,10 @@ package body Ada.Strings.Search is if Belongs (Source (J), Set, Test) then return J; end if; + + pragma Loop_Invariant + (for all C of Source (J .. Source'Last) => + not (Belongs (C, Set, Test))); end loop; end if; @@ -500,6 +582,8 @@ package body Ada.Strings.Search is Going : Direction := Forward; Mapping : Maps.Character_Mapping := Maps.Identity) return Natural is + Result : Natural; + PL1 : constant Integer := Pattern'Length - 1; begin -- AI05-056: If source is empty result is always zero @@ -512,17 +596,29 @@ package body Ada.Strings.Search is raise Index_Error; end if; - return + Result := Index (Source (From .. Source'Last), Pattern, Forward, Mapping); + pragma Assert + (if (for some J in From .. Source'Last - PL1 => + Match (Source, Pattern, Mapping, J)) + then Result in From .. Source'Last - PL1 + else Result = 0); else if From > Source'Last then raise Index_Error; end if; - return + Result := Index (Source (Source'First .. From), Pattern, Backward, Mapping); + pragma Assert + (if (for some J in Source'First .. From - PL1 => + Match (Source, Pattern, Mapping, J)) + then Result in Source'First .. From - PL1 + else Result = 0); end if; + + return Result; end Index; function Index @@ -603,6 +699,9 @@ package body Ada.Strings.Search is if Source (J) /= ' ' then return J; end if; + + pragma Loop_Invariant + (for all C of Source (Source'First .. J) => C = ' '); end loop; else -- Going = Backward @@ -610,6 +709,9 @@ package body Ada.Strings.Search is if Source (J) /= ' ' then return J; end if; + + pragma Loop_Invariant + (for all C of Source (J .. Source'Last) => C = ' '); end loop; end if; @@ -624,6 +726,13 @@ package body Ada.Strings.Search is Going : Direction := Forward) return Natural is begin + + -- For equivalence with Index, if Source is empty the result is 0 + + if Source'Length = 0 then + return 0; + end if; + if Going = Forward then if From < Source'First then raise Index_Error; @@ -642,4 +751,12 @@ package body Ada.Strings.Search is end if; end Index_Non_Blank; + function Is_Identity + (Mapping : Maps.Character_Mapping) return Boolean + with SPARK_Mode => Off + is + begin + return Mapping'Address = Maps.Identity'Address; + end Is_Identity; + end Ada.Strings.Search; diff --git a/gcc/ada/libgnat/a-strsea.ads b/gcc/ada/libgnat/a-strsea.ads index 623c0f4..4396747 100644 --- a/gcc/ada/libgnat/a-strsea.ads +++ b/gcc/ada/libgnat/a-strsea.ads @@ -32,76 +32,489 @@ -- This package contains the search functions from Ada.Strings.Fixed. They -- are separated out because they are shared by Ada.Strings.Bounded and -- Ada.Strings.Unbounded, and we don't want to drag in other irrelevant stuff --- from Ada.Strings.Fixed when using the other two packages. We make this a --- private package, since user programs should access these subprograms via --- one of the standard string packages. +-- from Ada.Strings.Fixed when using the other two packages. Although user +-- programs should access these subprograms via one of the standard string +-- packages, we do not make this a private package, since ghost function +-- Match is used in the contracts of the standard string packages. -with Ada.Strings.Maps; +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. This is enforced +-- by setting the corresponding assertion policy to Ignore. Postconditions, +-- contract cases and ghost code should not be executed at runtime as well, +-- in order not to slow down the execution of these functions. -private package Ada.Strings.Search is +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore); + +with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; + +package Ada.Strings.Search with SPARK_Mode is pragma Preelaborate; + -- The ghost function Match tells whether the slice of Source starting at + -- From and of length Pattern'Length matches with Pattern with respect to + -- Mapping. Pattern should be non-empty and the considered slice should be + -- fully included in Source'Range. + + function Match + (Source : String; + Pattern : String; + Mapping : Maps.Character_Mapping_Function; + From : Integer) return Boolean + is + (for all K in Pattern'Range => + Pattern (K) = Mapping (Source (From + (K - Pattern'First)))) + with + Ghost, + Pre => Mapping /= null + and then Pattern'Length > 0 + and then Source'Length > 0 + and then From in Source'First .. Source'Last - (Pattern'Length - 1), + Global => null; + + function Match + (Source : String; + Pattern : String; + Mapping : Maps.Character_Mapping; + From : Integer) return Boolean + is + (for all K in Pattern'Range => + Pattern (K) = + Ada.Strings.Maps.Value + (Mapping, Source (From + (K - Pattern'First)))) + with + Ghost, + Pre => Pattern'Length > 0 + and then Source'Length > 0 + and then From in Source'First .. Source'Last - (Pattern'Length - 1), + Global => null; + + function Is_Identity + (Mapping : Maps.Character_Mapping) return Boolean + with + Post => (if Is_Identity'Result then + (for all K in Character => + Ada.Strings.Maps.Value (Mapping, K) = K)), + Global => null; + function Index (Source : String; Pattern : String; Going : Direction := Forward; - Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; + Mapping : Maps.Character_Mapping := Maps.Identity) return Natural + with + Pre => Pattern'Length > 0, + + Post => Index'Result in 0 | Source'Range, + Contract_Cases => + + -- If Source is the empty string, then 0 is returned + + (Source'Length = 0 => Index'Result = 0, + + -- If some slice of Source matches Pattern, then a valid index is + -- returned. + + Source'Length > 0 + and then + (for some J in + Source'First .. Source'Last - (Pattern'Length - 1) => + Match (Source, Pattern, Mapping, J)) + => + + -- The result is in the considered range of Source + + Index'Result in Source'First .. Source'Last - (Pattern'Length - 1) + + -- The slice beginning at the returned index matches Pattern + + and then Match (Source, Pattern, Mapping, Index'Result) + + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in Source'Range => + (if (if Going = Forward + then J <= Index'Result - 1 + else J - 1 in Index'Result + .. Source'Last - Pattern'Length) + then not (Match (Source, Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others => Index'Result = 0), + Global => null; function Index (Source : String; Pattern : String; Going : Direction := Forward; - Mapping : Maps.Character_Mapping_Function) return Natural; + Mapping : Maps.Character_Mapping_Function) return Natural + with + Pre => Pattern'Length > 0 and then Mapping /= null, + Post => Index'Result in 0 | Source'Range, + Contract_Cases => + + -- If Source is the null string, then 0 is returned + + (Source'Length = 0 => Index'Result = 0, + + -- If some slice of Source matches Pattern, then a valid index is + -- returned. + + Source'Length > 0 and then + (for some J in Source'First .. Source'Last - (Pattern'Length - 1) => + Match (Source, Pattern, Mapping, J)) + => + + -- The result is in the considered range of Source + + Index'Result in Source'First .. Source'Last - (Pattern'Length - 1) + + -- The slice beginning at the returned index matches Pattern + + and then Match (Source, Pattern, Mapping, Index'Result) + + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in Source'Range => + (if (if Going = Forward + then J <= Index'Result - 1 + else J - 1 in Index'Result + .. Source'Last - Pattern'Length) + then not (Match (Source, Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others => Index'Result = 0), + Global => null; function Index (Source : String; Set : Maps.Character_Set; Test : Membership := Inside; - Going : Direction := Forward) return Natural; + Going : Direction := Forward) return Natural + with + Post => Index'Result in 0 | Source'Range, + Contract_Cases => + + -- If no character of Source satisfies the property Test on Set, then + -- 0 is returned. + + ((for all C of Source => + (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) + => + Index'Result = 0, + + -- Otherwise, a index in the range of Source is returned + + others => + + -- The result is in the range of Source + + Index'Result in Source'Range + + -- The character at the returned index satisfies the property + -- Test on Set + + and then (Test = Inside) + = Ada.Strings.Maps.Is_In (Source (Index'Result), Set) + + -- The result is the smallest or largest index which satisfies + -- the property, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in Source'Range => + (if J /= Index'Result + and then (J < Index'Result) = (Going = Forward) + then (Test = Inside) + /= Ada.Strings.Maps.Is_In (Source (J), Set)))), + Global => null; function Index (Source : String; Pattern : String; From : Positive; Going : Direction := Forward; - Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; + Mapping : Maps.Character_Mapping := Maps.Identity) return Natural + with + Pre => Pattern'Length > 0 + and then (if Source'Length > 0 then From in Source'Range), + + Post => Index'Result in 0 | Source'Range, + Contract_Cases => + + -- If Source is the empty string, then 0 is returned + + (Source'Length = 0 => Index'Result = 0, + + -- If some slice of Source matches Pattern, then a valid index is + -- returned. + + Source'Length > 0 + and then + (for some J in + (if Going = Forward then From else Source'First) + .. (if Going = Forward then Source'Last else From) + - (Pattern'Length - 1) => + Match (Source, Pattern, Mapping, J)) + => + + -- The result is in the considered range of Source + + Index'Result in + (if Going = Forward then From else Source'First) + .. (if Going = Forward then Source'Last else From) + - (Pattern'Length - 1) + + -- The slice beginning at the returned index matches Pattern + + and then Match (Source, Pattern, Mapping, Index'Result) + + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in Source'Range => + (if (if Going = Forward + then J in From .. Index'Result - 1 + else J - 1 in Index'Result + .. From - Pattern'Length) + then not (Match (Source, Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others => Index'Result = 0), + Global => null; function Index (Source : String; Pattern : String; From : Positive; Going : Direction := Forward; - Mapping : Maps.Character_Mapping_Function) return Natural; + Mapping : Maps.Character_Mapping_Function) return Natural + with + Pre => Pattern'Length > 0 + and then Mapping /= null + and then (if Source'Length > 0 then From in Source'Range), + + Post => Index'Result in 0 | Source'Range, + Contract_Cases => + + -- If Source is the empty string, then 0 is returned + + (Source'Length = 0 => Index'Result = 0, + + -- If some slice of Source matches Pattern, then a valid index is + -- returned. + + Source'Length > 0 + and then + (for some J in + (if Going = Forward then From else Source'First) + .. (if Going = Forward then Source'Last else From) + - (Pattern'Length - 1) => + Match (Source, Pattern, Mapping, J)) + => + + -- The result is in the considered range of Source + + Index'Result in + (if Going = Forward then From else Source'First) + .. (if Going = Forward then Source'Last else From) + - (Pattern'Length - 1) + + -- The slice beginning at the returned index matches Pattern + + and then Match (Source, Pattern, Mapping, Index'Result) + + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backwards. + + and then + (for all J in Source'Range => + (if (if Going = Forward + then J in From .. Index'Result - 1 + else J - 1 in Index'Result + .. From - Pattern'Length) + then not (Match (Source, Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others => Index'Result = 0), + Global => null; function Index (Source : String; Set : Maps.Character_Set; From : Positive; Test : Membership := Inside; - Going : Direction := Forward) return Natural; + Going : Direction := Forward) return Natural + with + Pre => (if Source'Length > 0 then From in Source'Range), + Post => Index'Result in 0 | Source'Range, + Contract_Cases => + + -- If Source is the empty string, or no character of the considered + -- slice of Source satisfies the property Test on Set, then 0 is + -- returned. + + (Source'Length = 0 + or else + (for all J in Source'Range => + (if J = From or else (J > From) = (Going = Forward) then + (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (J), Set))) + => + Index'Result = 0, + + -- Otherwise, a index in the considered range of Source is returned + + others => + + -- The result is in the considered range of Source + + Index'Result in Source'Range + and then (Index'Result = From + or else + (Index'Result > From) = (Going = Forward)) + + -- The character at the returned index satisfies the property + -- Test on Set + + and then + (Test = Inside) + = Ada.Strings.Maps.Is_In (Source (Index'Result), Set) + + -- The result is the smallest or largest index which satisfies + -- the property, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in Source'Range => + (if J /= Index'Result + and then (J < Index'Result) = (Going = Forward) + and then (J = From + or else (J > From) = (Going = Forward)) + then (Test = Inside) + /= Ada.Strings.Maps.Is_In (Source (J), Set)))), + Global => null; function Index_Non_Blank (Source : String; - Going : Direction := Forward) return Natural; + Going : Direction := Forward) return Natural + with + Post => Index_Non_Blank'Result in 0 | Source'Range, + Contract_Cases => + + -- If all characters of Source are Space characters, then 0 is + -- returned. + + ((for all C of Source => C = ' ') => Index_Non_Blank'Result = 0, + + -- Otherwise, a valid index is returned + + others => + + -- The result is in the range of Source + + Index_Non_Blank'Result in Source'Range + + -- The character at the returned index is not a Space character + + and then Source (Index_Non_Blank'Result) /= ' ' + + -- The result is the smallest or largest index which is not a + -- Space character, respectively when Going = Forward and + -- Going = Backward. + + and then + (for all J in Source'Range => + (if J /= Index_Non_Blank'Result + and then (J < Index_Non_Blank'Result) + = (Going = Forward) + then Source (J) = ' '))), + Global => null; function Index_Non_Blank (Source : String; From : Positive; - Going : Direction := Forward) return Natural; + Going : Direction := Forward) return Natural + with + Pre => (if Source'Length /= 0 then From in Source'Range), + Post => Index_Non_Blank'Result in 0 | Source'Range, + Contract_Cases => + + -- If Source is the null string, or all characters in the considered + -- slice of Source are Space characters, then 0 is returned. + + (Source'Length = 0 + or else + (for all J in Source'Range => + (if J = From or else (J > From) = (Going = Forward) then + Source (J) = ' ')) + => + Index_Non_Blank'Result = 0, + + -- Otherwise, a valid index is returned + + others => + + -- The result is in the considered range of Source + + Index_Non_Blank'Result in Source'Range + and then (Index_Non_Blank'Result = From + or else (Index_Non_Blank'Result > From) + = (Going = Forward)) + + -- The character at the returned index is not a Space character + + and then Source (Index_Non_Blank'Result) /= ' ' + + -- The result is the smallest or largest index which is not a + -- Space character, respectively when Going = Forward and + -- Going = Backward. + + and then + (for all J in Source'Range => + (if J /= Index_Non_Blank'Result + and then (J < Index_Non_Blank'Result) + = (Going = Forward) + and then (J = From or else (J > From) + = (Going = Forward)) + then Source (J) = ' '))), + Global => null; function Count (Source : String; Pattern : String; - Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; + Mapping : Maps.Character_Mapping := Maps.Identity) return Natural + with + Pre => Pattern'Length > 0, + Global => null; function Count (Source : String; Pattern : String; - Mapping : Maps.Character_Mapping_Function) return Natural; + Mapping : Maps.Character_Mapping_Function) return Natural + with + Pre => Pattern'Length > 0 and then Mapping /= null, + Global => null; function Count (Source : String; - Set : Maps.Character_Set) return Natural; + Set : Maps.Character_Set) return Natural + with + Global => null; procedure Find_Token (Source : String; @@ -109,13 +522,104 @@ private package Ada.Strings.Search is From : Positive; Test : Membership; First : out Positive; - Last : out Natural); + Last : out Natural) + with + Pre => (if Source'Length /= 0 then From in Source'Range), + Contract_Cases => + + -- If Source is the empty string, or if no character of the considered + -- slice of Source satisfies the property Test on Set, then First is + -- set to From and Last is set to 0. + + (Source'Length = 0 + or else + (for all C of Source (From .. Source'Last) => + (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) + => + First = From and then Last = 0, + + -- Otherwise, First and Last are set to valid indexes + + others => + + -- First and Last are in the considered range of Source + + First in From .. Source'Last + and then Last in First .. Source'Last + + -- No character between From and First satisfies the property Test + -- on Set. + + and then + (for all C of Source (From .. First - 1) => + (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) + + -- All characters between First and Last satisfy the property Test + -- on Set. + + and then + (for all C of Source (First .. Last) => + (Test = Inside) = Ada.Strings.Maps.Is_In (C, Set)) + + -- If Last is not Source'Last, then the character at position + -- Last + 1 does not satify the property Test on Set. + + and then + (if Last < Source'Last + then (Test = Inside) + /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), + Global => null; procedure Find_Token (Source : String; Set : Maps.Character_Set; Test : Membership; First : out Positive; - Last : out Natural); + Last : out Natural) + with + Pre => Source'First > 0, + Contract_Cases => + + -- If Source is the empty string, or if no character of Source + -- satisfies the property Test on Set, then First is set to From + -- and Last is set to 0. + + (Source'Length = 0 + or else + (for all C of Source => + (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) + => + First = Source'First and then Last = 0, + + -- Otherwise, First and Last are set to valid indexes + + others => + + -- First and Last are in the considered range of Source + + First in Source'Range + and then Last in First .. Source'Last + + -- No character before First satisfies the property Test on Set + + and then + (for all C of Source (Source'First .. First - 1) => + (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) + + -- All characters between First and Last satisfy the property Test + -- on Set. + + and then + (for all C of Source (First .. Last) => + (Test = Inside) = Ada.Strings.Maps.Is_In (C, Set)) + + -- If Last is not Source'Last, then the character at position + -- Last + 1 does not satify the property Test on Set. + + and then + (if Last < Source'Last + then (Test = Inside) + /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), + Global => null; end Ada.Strings.Search; |