------------------------------------------------------------------------------
-- --
-- GNAT RUN-TIME COMPONENTS --
-- --
-- A D A . S T R I N G S . F I X E D --
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2023, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
-- --
-- GNAT was originally developed by the GNAT team at New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc. --
-- --
------------------------------------------------------------------------------
-- Note: This code is derived from the ADAR.CSH public domain Ada 83 versions
-- of the Appendix C string handling packages. One change is to avoid the use
-- of Is_In, so that we are not dependent on inlining. Note that the search
-- function implementations are to be found in the auxiliary package
-- Ada.Strings.Search. Also the Move procedure is directly incorporated (ADAR
-- used a subunit for this procedure). The number of errors having to do with
-- 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;
package body Ada.Strings.Fixed with SPARK_Mode is
------------------------
-- Search Subprograms --
------------------------
function Index
(Source : String;
Pattern : String;
Going : Direction := Forward;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
renames Ada.Strings.Search.Index;
function Index
(Source : String;
Pattern : String;
Going : Direction := Forward;
Mapping : Maps.Character_Mapping_Function) return Natural
renames Ada.Strings.Search.Index;
function Index
(Source : String;
Set : Maps.Character_Set;
Test : Membership := Inside;
Going : Direction := Forward) return Natural
renames Ada.Strings.Search.Index;
function Index
(Source : String;
Pattern : String;
From : Positive;
Going : Direction := Forward;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
renames Ada.Strings.Search.Index;
function Index
(Source : String;
Pattern : String;
From : Positive;
Going : Direction := Forward;
Mapping : Maps.Character_Mapping_Function) return Natural
renames Ada.Strings.Search.Index;
function Index
(Source : String;
Set : Maps.Character_Set;
From : Positive;
Test : Membership := Inside;
Going : Direction := Forward) return Natural
renames Ada.Strings.Search.Index;
function Index_Non_Blank
(Source : String;
Going : Direction := Forward) return Natural
renames Ada.Strings.Search.Index_Non_Blank;
function Index_Non_Blank
(Source : String;
From : Positive;
Going : Direction := Forward) return Natural
renames Ada.Strings.Search.Index_Non_Blank;
function Count
(Source : String;
Pattern : String;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
renames Ada.Strings.Search.Count;
function Count
(Source : String;
Pattern : String;
Mapping : Maps.Character_Mapping_Function) return Natural
renames Ada.Strings.Search.Count;
function Count
(Source : String;
Set : Maps.Character_Set) return Natural
renames Ada.Strings.Search.Count;
procedure Find_Token
(Source : String;
Set : Maps.Character_Set;
From : Positive;
Test : Membership;
First : out Positive;
Last : out Natural)
renames Ada.Strings.Search.Find_Token;
procedure Find_Token
(Source : String;
Set : Maps.Character_Set;
Test : Membership;
First : out Positive;
Last : out Natural)
renames Ada.Strings.Search.Find_Token;
---------
-- "*" --
---------
function "*"
(Left : Natural;
Right : Character) return String
is
begin
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 "*";
function "*"
(Left : Natural;
Right : String) return String
is
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
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 + 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 "*";
------------
-- Delete --
------------
function Delete
(Source : String;
From : Positive;
Through : Natural) return String
is
begin
if From > Through then
declare
subtype Result_Type is String (1 .. Source'Length);
begin
return Result_Type (Source);
end;
elsif From not in Source'Range
or else Through > Source'Last
then
pragma Annotate
(CodePeer, False_Positive,
"test always false", "self fullfilling prophecy");
-- In most cases this raises an exception, but the case of deleting
-- a null string at the end of the current one is a special-case, and
-- reflects the equivalence with Replace_String (RM A.4.3 (86/3)).
if From = Source'Last + 1 and then From = Through then
return Source;
else
raise Index_Error;
end if;
else
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;
procedure Delete
(Source : in out String;
From : Positive;
Through : Natural;
Justify : Alignment := Left;
Pad : Character := Space)
is
begin
Move (Source => Delete (Source, From, Through),
Target => Source,
Justify => Justify,
Pad => Pad);
end Delete;
----------
-- Head --
----------
function Head
(Source : String;
Count : Natural;
Pad : Character := Space) return String
is
subtype Result_Type is String (1 .. Count);
begin
if Count <= Source'Length then
return
Result_Type (Source (Source'First .. Source'First + (Count - 1)));
else
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;
end Head;
procedure Head
(Source : in out String;
Count : Natural;
Justify : Alignment := Left;
Pad : Character := Space)
is
begin
Move (Source => Head (Source, Count, Pad),
Target => Source,
Drop => Error,
Justify => Justify,
Pad => Pad);
end Head;
------------
-- Insert --
------------
function Insert
(Source : String;
Before : Positive;
New_Item : String) return String
is
Front : constant Integer := Before - Source'First;
begin
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)
with Relaxed_Initialization
do
Result (1 .. Front) :=
Source (Source'First .. Before - 1);
Result (Front + 1 .. Front + New_Item'Length) :=
New_Item;
pragma Assert
(Result (1 .. Before - Source'First)
= Source (Source'First .. Before - 1));
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;
procedure Insert
(Source : in out String;
Before : Positive;
New_Item : String;
Drop : Truncation := Error)
is
begin
Move (Source => Insert (Source, Before, New_Item),
Target => Source,
Drop => Drop);
end Insert;
----------
-- Move --
----------
procedure Move
(Source : String;
Target : out String;
Drop : Truncation := Error;
Justify : Alignment := Left;
Pad : Character := Space)
with SPARK_Mode => Off
is
Sfirst : constant Integer := Source'First;
Slast : constant Integer := Source'Last;
Slength : constant Integer := Source'Length;
Tfirst : constant Integer := Target'First;
Tlast : constant Integer := Target'Last;
Tlength : constant Integer := Target'Length;
function Is_Padding (Item : String) return Boolean;
-- Check if Item is all Pad characters, return True if so, False if not
function Is_Padding (Item : String) return Boolean is
begin
for J in Item'Range loop
if Item (J) /= Pad then
return False;
end if;
end loop;
return True;
end Is_Padding;
-- Start of processing for Move
begin
if Slength = Tlength then
Target := Source;
elsif Slength > Tlength then
case Drop is
when Left =>
Target := Source (Slast - Tlength + 1 .. Slast);
when Right =>
Target := Source (Sfirst .. Sfirst + Tlength - 1);
when Error =>
case Justify is
when Left =>
if Is_Padding (Source (Sfirst + Tlength .. Slast)) then
Target :=
Source (Sfirst .. Sfirst + Target'Length - 1);
else
raise Length_Error;
end if;
when Right =>
if Is_Padding (Source (Sfirst .. Slast - Tlength)) then
Target := Source (Slast - Tlength + 1 .. Slast);
else
raise Length_Error;
end if;
when Center =>
raise Length_Error;
end case;
end case;
-- Source'Length < Target'Length
else
case Justify is
when Left =>
Target (Tfirst .. Tfirst + Slength - 1) := Source;
for I in Tfirst + Slength .. Tlast loop
Target (I) := Pad;
end loop;
when Right =>
for I in Tfirst .. Tlast - Slength loop
Target (I) := Pad;
end loop;
Target (Tlast - Slength + 1 .. Tlast) := Source;
when Center =>
declare
Front_Pad : constant Integer := (Tlength - Slength) / 2;
Tfirst_Fpad : constant Integer := Tfirst + Front_Pad;
begin
for I in Tfirst .. Tfirst_Fpad - 1 loop
Target (I) := Pad;
end loop;
Target (Tfirst_Fpad .. Tfirst_Fpad + Slength - 1) := Source;
for I in Tfirst_Fpad + Slength .. Tlast loop
Target (I) := Pad;
end loop;
end;
end case;
end if;
end Move;
---------------
-- Overwrite --
---------------
function Overwrite
(Source : String;
Position : Positive;
New_Item : String) return String is
begin
if Position - 1 not in Source'First - 1 .. Source'Last then
raise Index_Error;
end if;
declare
Result_Length : constant Natural :=
Integer'Max (Source'Length,
Position - Source'First + New_Item'Length);
Front : constant Integer := Position - Source'First;
begin
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;
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);
pragma Assert
(Result
(Position - Source'First + 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;
procedure Overwrite
(Source : in out String;
Position : Positive;
New_Item : String;
Drop : Truncation := Right)
is
begin
Move (Source => Overwrite (Source, Position, New_Item),
Target => Source,
Drop => Drop);
end Overwrite;
-------------------
-- Replace_Slice --
-------------------
function Replace_Slice
(Source : String;
Low : Positive;
High : Natural;
By : String) return String is
begin
if Low - 1 > Source'Last or else High < Source'First - 1 then
raise Index_Error;
end if;
if High >= Low then
declare
Front_Len : constant Integer :=
Integer'Max (0, Low - Source'First);
-- Length of prefix of Source copied to result
Back_Len : constant Integer := Integer'Max (0, Source'Last - High);
-- Length of suffix of Source copied to result
Result_Length : constant Integer :=
Front_Len + By'Length + Back_Len;
-- Length of result
begin
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;
pragma Assert
(Result
(Integer'Max (0, Low - Source'First) + 1
.. Integer'Max (0, Low - Source'First) + By'Length)
= By);
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
return Insert (Source, Before => Low, New_Item => By);
end if;
end Replace_Slice;
procedure Replace_Slice
(Source : in out String;
Low : Positive;
High : Natural;
By : String;
Drop : Truncation := Error;
Justify : Alignment := Left;
Pad : Character := Space)
is
begin
Move (Replace_Slice (Source, Low, High, By), Source, Drop, Justify, Pad);
end Replace_Slice;
----------
-- Tail --
----------
function Tail
(Source : String;
Count : Natural;
Pad : Character := Space) return String
is
subtype Result_Type is String (1 .. Count);
begin
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 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;
if Source'Length /= 0 then
Result (Count - Source'Length + 1 .. Count) := Source;
end if;
end return;
end if;
end Tail;
procedure Tail
(Source : in out String;
Count : Natural;
Justify : Alignment := Left;
Pad : Character := Space)
is
begin
Move (Source => Tail (Source, Count, Pad),
Target => Source,
Drop => Error,
Justify => Justify,
Pad => Pad);
end Tail;
---------------
-- Translate --
---------------
function Translate
(Source : String;
Mapping : Maps.Character_Mapping) return String
is
begin
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;
procedure Translate
(Source : in out String;
Mapping : Maps.Character_Mapping)
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;
function Translate
(Source : String;
Mapping : Maps.Character_Mapping_Function) return String
is
pragma Unsuppress (Access_Check);
begin
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 Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
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)));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
end loop;
end return;
end Translate;
procedure Translate
(Source : in out String;
Mapping : Maps.Character_Mapping_Function)
is
pragma Unsuppress (Access_Check);
begin
for J in Source'Range loop
Source (J) := Mapping.all (Source (J));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
pragma Loop_Invariant
(for all K in Source'First .. J =>
Source (K) = Mapping (Source'Loop_Entry (K)));
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
end loop;
end Translate;
----------
-- Trim --
----------
function Trim
(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 =>
declare
Low : constant Natural := Index_Non_Blank (Source, Forward);
begin
-- All blanks case
if Low = 0 then
return Empty_String;
end if;
declare
subtype Result_Type is String (1 .. Source'Last - Low + 1);
begin
return Result_Type (Source (Low .. Source'Last));
end;
end;
when Strings.Right =>
declare
High : constant Natural := Index_Non_Blank (Source, Backward);
begin
-- All blanks case
if High = 0 then
return Empty_String;
end if;
declare
subtype Result_Type is String (1 .. High - Source'First + 1);
begin
return Result_Type (Source (Source'First .. High));
end;
end;
when Strings.Both =>
declare
Low : constant Natural := Index_Non_Blank (Source, Forward);
begin
-- All blanks case
if Low = 0 then
return Empty_String;
end if;
declare
High : constant Natural :=
Index_Non_Blank (Source, Backward);
subtype Result_Type is String (1 .. High - Low + 1);
begin
return Result_Type (Source (Low .. High));
end;
end;
end case;
end Trim;
procedure Trim
(Source : in out String;
Side : Trim_End;
Justify : Alignment := Left;
Pad : Character := Space)
is
begin
Move (Trim (Source, Side),
Source,
Justify => Justify,
Pad => Pad);
end Trim;
function Trim
(Source : String;
Left : Maps.Character_Set;
Right : Maps.Character_Set) return String
is
High, Low : Integer;
begin
Low := Index (Source, Set => Left, Test => Outside, Going => Forward);
-- Case where source comprises only characters in Left
if Low = 0 then
return "";
end if;
High := Index (Source, Set => Right, Test => Outside, Going => Backward);
-- Case where source comprises only characters in Right
if High = 0 then
return "";
end if;
declare
Result_Length : constant Integer := High - Low + 1;
subtype Result_Type is String (1 .. Result_Length);
begin
return Result_Type (Source (Low .. High));
end;
end Trim;
procedure Trim
(Source : in out String;
Left : Maps.Character_Set;
Right : Maps.Character_Set;
Justify : Alignment := Strings.Left;
Pad : Character := Space)
is
begin
Move (Source => Trim (Source, Left, Right),
Target => Source,
Justify => Justify,
Pad => Pad);
end Trim;
end Ada.Strings.Fixed;