OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] SPARK proof of the Ada.Strings.Fixed library

Browse Source 
gcc/ada/

	* libgnat/a-strfix.adb ("*"): Added loop invariants and lemmas
	for proof.
	(Delete): Added assertions for proof, and conditions to avoid
	overflow.
	(Head): Added loop invariant.
	(Insert): Same as Delete.
	(Move): Declared with SPARK_Mode Off.
	(Overwrite): Added assertions for proof, and conditions to avoid
	overflow.
	(Replace_Slice): Added assertions for proof, and conditions to
	avoid overflow.
	(Tail): Added loop invariant and avoided overflows.
	(Translate): Added loop invariants.
	(Trim): Ensured empty strings returned start at 1.
	* libgnat/a-strfix.ads (Index): Rewrote contract cases for
	easier proof.
	(Index_Non_Blank): Separated the null string case.
	(Count): Specified Mapping shouldn't be null.
	(Find_Token): Specified Source'First should be Positive when no
	From is given.
	(Translate): Specified Mapping shouldn't be null.
	("*"): Rewrote postcondition for easier proof.
	* libgnat/a-strsea.adb (Belongs): Added postcondition.
	(Count): Rewrote loops and added loop invariants to avoid
	overflows.
	(Find_Token): Added loop invariants.
	(Index): Rewrote loops to avoid overflows and added loop
	invariants for proof.
	(Index_Non_Blank): Added loop invariants.
	(Is_Identity): New function isolated without SPARK_Mode.
	* libgnat/a-strsea.ads: Fix starting comment as package is no
	longer private.
	(Match): Declared ghost expression function Match.
	(Is_Identity): Described identity in the postcondition.
	(Index, Index_Non_Blank, Count, Find_Token): Added contract from
	a-strfix.ads.
This commit is contained in:
Pierre-Alexandre Bazin 2021-06-18 12:09:48 +02:00 committed by Pierre-Marie de Rodat
parent 8582e5d07e
commit 6c5ca4cf42
4 changed files with 1169 additions and 352 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

282
gcc/ada/libgnat/a-strfix.adb
View File

@ -38,10 +38,17 @@
-- bounds of function return results were also fixed, and use of & removed for
-- efficiency reasons.
with Ada.Strings.Maps; use Ada.Strings.Maps;
with Ada.Strings.Search;
-- 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.
package body Ada.Strings.Fixed is
pragma Assertion_Policy (Ghost => Ignore,
Loop_Invariant => Ignore,
Assert => Ignore);
with Ada.Strings.Maps; use Ada.Strings.Maps;
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));

376
gcc/ada/libgnat/a-strfix.ads
View File

@ -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

319
gcc/ada/libgnat/a-strsea.adb
View File

@ -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;

544
gcc/ada/libgnat/a-strsea.ads
View File

@ -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;
function Index
-- 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;
Going : Direction := Forward;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
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_Function) 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
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;