-- --
------------------------------------------------------------------------------
+-- Loop invariants 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 (Loop_Invariant => Ignore);
+
with Ada.Characters.Latin_1; use Ada.Characters.Latin_1;
with Ada.Strings.Maps; use Ada.Strings.Maps;
with Ada.Strings.Maps.Constants; use Ada.Strings.Maps.Constants;
-package body Ada.Characters.Handling is
+package body Ada.Characters.Handling
+ with SPARK_Mode
+is
------------------------------------
-- Character Classification Table --
------------------
function Is_Character (Item : Wide_Character) return Boolean is
- begin
- return Wide_Character'Pos (Item) < 256;
- end Is_Character;
+ (Wide_Character'Pos (Item) < 256);
----------------
-- Is_Control --
----------------
function Is_ISO_646 (Item : Character) return Boolean is
- begin
- return Item in ISO_646;
- end Is_ISO_646;
+ (Item in ISO_646);
-- Note: much more efficient coding of the following function is possible
-- by testing several 16#80# bits in a complete word in a single operation
if Item (J) not in ISO_646 then
return False;
end if;
+ pragma Loop_Invariant
+ (for all K in Item'First .. J => Is_ISO_646 (Item (K)));
end loop;
return True;
if Wide_Character'Pos (Item (J)) >= 256 then
return False;
end if;
+ pragma Loop_Invariant
+ (for all K in Item'First .. J => Is_Character (Item (K)));
end loop;
return True;
--------------
function To_Basic (Item : Character) return Character is
- begin
- return Value (Basic_Map, Item);
- end To_Basic;
+ (Value (Basic_Map, Item));
function To_Basic (Item : String) return String is
begin
- return Result : String (1 .. Item'Length) do
+ return Result : String (1 .. Item'Length) with Relaxed_Initialization do
for J in Item'Range loop
Result (J - (Item'First - 1)) := Value (Basic_Map, Item (J));
+ pragma Loop_Invariant
+ (Result (1 .. J - Item'First + 1)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ Result (K - (Item'First - 1)) = To_Basic (Item (K)));
end loop;
end return;
end To_Basic;
function To_ISO_646
(Item : Character;
Substitute : ISO_646 := ' ') return ISO_646
- is
- begin
- return (if Item in ISO_646 then Item else Substitute);
- end To_ISO_646;
+ is (if Item in ISO_646 then Item else Substitute);
function To_ISO_646
(Item : String;
Substitute : ISO_646 := ' ') return String
is
- Result : String (1 .. Item'Length);
-
begin
- for J in Item'Range loop
- Result (J - (Item'First - 1)) :=
- (if Item (J) in ISO_646 then Item (J) else Substitute);
- end loop;
-
- return Result;
+ return Result : String (1 .. Item'Length) with Relaxed_Initialization do
+ for J in Item'Range loop
+ Result (J - (Item'First - 1)) :=
+ (if Item (J) in ISO_646 then Item (J) else Substitute);
+ pragma Loop_Invariant
+ (Result (1 .. J - Item'First + 1)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ Result (K - (Item'First - 1)) =
+ To_ISO_646 (Item (K), Substitute));
+ end loop;
+ end return;
end To_ISO_646;
--------------
--------------
function To_Lower (Item : Character) return Character is
- begin
- return Value (Lower_Case_Map, Item);
- end To_Lower;
+ (Value (Lower_Case_Map, Item));
function To_Lower (Item : String) return String is
begin
- return Result : String (1 .. Item'Length) do
+ return Result : String (1 .. Item'Length) with Relaxed_Initialization do
for J in Item'Range loop
Result (J - (Item'First - 1)) := Value (Lower_Case_Map, Item (J));
+ pragma Loop_Invariant
+ (Result (1 .. J - Item'First + 1)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ Result (K - (Item'First - 1)) = To_Lower (Item (K)));
end loop;
end return;
end To_Lower;
(Item : Wide_String;
Substitute : Character := ' ') return String
is
- Result : String (1 .. Item'Length);
-
begin
- for J in Item'Range loop
- Result (J - (Item'First - 1)) := To_Character (Item (J), Substitute);
- end loop;
-
- return Result;
+ return Result : String (1 .. Item'Length) with Relaxed_Initialization do
+ for J in Item'Range loop
+ Result (J - (Item'First - 1)) :=
+ To_Character (Item (J), Substitute);
+ pragma Loop_Invariant
+ (Result (1 .. J - (Item'First - 1))'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ Result (K - (Item'First - 1)) =
+ To_Character (Item (K), Substitute));
+ end loop;
+ end return;
end To_String;
--------------
-- To_Upper --
--------------
- function To_Upper
- (Item : Character) return Character
- is
- begin
- return Value (Upper_Case_Map, Item);
- end To_Upper;
+ function To_Upper (Item : Character) return Character is
+ (Value (Upper_Case_Map, Item));
function To_Upper
(Item : String) return String
is
begin
- return Result : String (1 .. Item'Length) do
+ return Result : String (1 .. Item'Length) with Relaxed_Initialization do
for J in Item'Range loop
Result (J - (Item'First - 1)) := Value (Upper_Case_Map, Item (J));
+ pragma Loop_Invariant
+ (Result (1 .. J - Item'First + 1)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ Result (K - (Item'First - 1)) = To_Upper (Item (K)));
end loop;
end return;
end To_Upper;
function To_Wide_String
(Item : String) return Wide_String
is
- Result : Wide_String (1 .. Item'Length);
-
begin
- for J in Item'Range loop
- Result (J - (Item'First - 1)) := To_Wide_Character (Item (J));
- end loop;
-
- return Result;
+ return Result : Wide_String (1 .. Item'Length)
+ with Relaxed_Initialization
+ do
+ for J in Item'Range loop
+ Result (J - (Item'First - 1)) := To_Wide_Character (Item (J));
+ pragma Loop_Invariant
+ (Result (1 .. J - (Item'First - 1))'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ Result (K - (Item'First - 1)) = To_Wide_Character (Item (K)));
+ end loop;
+ end return;
end To_Wide_String;
end Ada.Characters.Handling;
-- --
------------------------------------------------------------------------------
-package Ada.Characters.Handling is
+-- Postconditions in this unit are meant for analysis only, not for run-time
+-- checking, in order not to slow down the execution of these functions.
+
+pragma Assertion_Policy (Post => Ignore);
+
+with Ada.Characters.Latin_1;
+
+package Ada.Characters.Handling
+ with SPARK_Mode
+is
pragma Pure;
-- In accordance with Ada 2005 AI-362
-- Character Classification Functions --
----------------------------------------
- function Is_Control (Item : Character) return Boolean;
- function Is_Graphic (Item : Character) return Boolean;
- function Is_Letter (Item : Character) return Boolean;
- function Is_Lower (Item : Character) return Boolean;
- function Is_Upper (Item : Character) return Boolean;
- function Is_Basic (Item : Character) return Boolean;
- function Is_Digit (Item : Character) return Boolean;
+ -- In the description below for each function that returns a Boolean
+ -- result, the effect is described in terms of the conditions under which
+ -- the value True is returned. If these conditions are not met, then the
+ -- function returns False.
+ --
+ -- Each of the following classification functions has a formal Character
+ -- parameter, Item, and returns a Boolean result.
+
+ function Is_Control (Item : Character) return Boolean
+ with
+ Post => Is_Control'Result =
+ (Character'Pos (Item) in 0 .. 31 | 127 .. 159);
+ -- True if Item is a control character. A control character is a character
+ -- whose position is in one of the ranges 0..31 or 127..159.
+
+ function Is_Graphic (Item : Character) return Boolean
+ with
+ Post => Is_Graphic'Result =
+ (Character'Pos (Item) in 32 .. 126 | 160 .. 255);
+ -- True if Item is a graphic character. A graphic character is a character
+ -- whose position is in one of the ranges 32..126 or 160..255.
+
+ function Is_Letter (Item : Character) return Boolean
+ with
+ Post => Is_Letter'Result =
+ (Item in 'A' .. 'Z' | 'a' .. 'z'
+ or else Character'Pos (Item) in 192 .. 214 | 216 .. 246 | 248 .. 255);
+ -- True if Item is a letter. A letter is a character that is in one of the
+ -- ranges 'A'..'Z' or 'a'..'z', or whose position is in one of the ranges
+ -- 192..214, 216..246, or 248..255.
+
+ function Is_Lower (Item : Character) return Boolean
+ with
+ Post => Is_Lower'Result =
+ (Item in 'a' .. 'z'
+ or else Character'Pos (Item) in 223 .. 246 | 248 .. 255);
+ -- True if Item is a lower-case letter. A lower-case letter is a character
+ -- that is in the range 'a'..'z', or whose position is in one of the ranges
+ -- 223..246 or 248..255.
+
+ function Is_Upper (Item : Character) return Boolean
+ with
+ Post => Is_Upper'Result =
+ (Item in 'A' .. 'Z'
+ or else Character'Pos (Item) in 192 .. 214 | 216 .. 222);
+ -- True if Item is an upper-case letter. An upper-case letter is a
+ -- character that is in the range 'A'..'Z' or whose position is in one
+ -- of the ranges 192..214 or 216..222.
+
+ function Is_Basic (Item : Character) return Boolean
+ with
+ Post => Is_Basic'Result =
+ (Item in 'A' .. 'Z'
+ | 'a' .. 'z'
+ | Latin_1.UC_AE_Diphthong
+ | Latin_1.LC_AE_Diphthong
+ | Latin_1.UC_Icelandic_Eth
+ | Latin_1.LC_Icelandic_Eth
+ | Latin_1.UC_Icelandic_Thorn
+ | Latin_1.LC_Icelandic_Thorn
+ | Latin_1.LC_German_Sharp_S);
+ -- True if Item is a basic letter. A basic letter is a character that
+ -- is in one of the ranges 'A'..'Z' and 'a'..'z', or that is one of
+ -- the following: UC_AE_Diphthong, LC_AE_Diphthong, UC_Icelandic_Eth,
+ -- LC_Icelandic_Eth, UC_Icelandic_Thorn, LC_Icelandic_Thorn, or
+ -- LC_German_Sharp_S.
+
+ function Is_Digit (Item : Character) return Boolean
+ with
+ Post => Is_Digit'Result = (Item in '0' .. '9');
+ -- True if Item is a decimal digit. A decimal digit is a character in the
+ -- range '0'..'9'.
+
function Is_Decimal_Digit (Item : Character) return Boolean
renames Is_Digit;
- function Is_Hexadecimal_Digit (Item : Character) return Boolean;
- function Is_Alphanumeric (Item : Character) return Boolean;
- function Is_Special (Item : Character) return Boolean;
- function Is_Line_Terminator (Item : Character) return Boolean;
- function Is_Mark (Item : Character) return Boolean;
- function Is_Other_Format (Item : Character) return Boolean;
- function Is_Punctuation_Connector (Item : Character) return Boolean;
- function Is_Space (Item : Character) return Boolean;
- function Is_NFKC (Item : Character) return Boolean;
+
+ function Is_Hexadecimal_Digit (Item : Character) return Boolean
+ with
+ Post => Is_Hexadecimal_Digit'Result =
+ (Is_Decimal_Digit (Item) or Item in 'A' .. 'F' | 'a' .. 'f');
+ -- True if Item is a hexadecimal digit. A hexadecimal digit is a character
+ -- that is either a decimal digit or that is in one of the ranges 'A'..'F'
+ -- or 'a'..'f'.
+
+ function Is_Alphanumeric (Item : Character) return Boolean
+ with
+ Post => Is_Alphanumeric'Result =
+ (Is_Letter (Item) or Is_Decimal_Digit (Item));
+ -- True if Item is an alphanumeric character. An alphanumeric character is
+ -- a character that is either a letter or a decimal digit.
+
+ function Is_Special (Item : Character) return Boolean
+ with
+ Post => Is_Special'Result =
+ (Is_Graphic (Item) and not Is_Alphanumeric (Item));
+ -- True if Item is a special graphic character. A special graphic character
+ -- is a graphic character that is not alphanumeric.
+
+ function Is_Line_Terminator (Item : Character) return Boolean
+ with
+ Post => Is_Line_Terminator'Result =
+ (Character'Pos (Item) in 10 .. 13 | 133);
+ -- True if Item is a character with position 10..13 (Line_Feed,
+ -- Line_Tabulation, Form_Feed, Carriage_Return) or 133 (Next_Line).
+
+ function Is_Mark (Item : Character) return Boolean
+ with
+ Post => Is_Mark'Result = False;
+ -- Never True (no value of type Character has categories Mark, Non-Spacing
+ -- or Mark, Spacing Combining).
+
+ function Is_Other_Format (Item : Character) return Boolean
+ with
+ Post => Is_Other_Format'Result = (Character'Pos (Item) = 173);
+ -- True if Item is a character with position 173 (Soft_Hyphen).
+
+ function Is_Punctuation_Connector (Item : Character) return Boolean
+ with
+ Post => Is_Punctuation_Connector'Result =
+ (Character'Pos (Item) = 95);
+ -- True if Item is a character with position 95 ('_', known as Low_Line or
+ -- Underscore).
+
+ function Is_Space (Item : Character) return Boolean
+ with
+ Post => Is_Space'Result = (Character'Pos (Item) in 32 | 160);
+ -- True if Item is a character with position 32 (' ') or 160
+ -- (No_Break_Space).
+
+ function Is_NFKC (Item : Character) return Boolean
+ with
+ Post => Is_NFKC'Result =
+ (Character'Pos (Item) not in
+ 160 | 168 | 170 | 175 | 178 | 179 | 180
+ | 181 | 184 | 185 | 186 | 188 | 189 | 190);
+ -- True if Item could be present in a string normalized to Normalization
+ -- Form KC (as defined by Clause 21 of ISO/IEC 10646:2017); this includes
+ -- all characters except those with positions 160, 168, 170, 175, 178, 179,
+ -- 180, 181, 184, 185, 186, 188, 189, and 190.
---------------------------------------------------
-- Conversion Functions for Character and String --
---------------------------------------------------
- function To_Lower (Item : Character) return Character;
- function To_Upper (Item : Character) return Character;
- function To_Basic (Item : Character) return Character;
+ -- Each of the names To_Lower, To_Upper, and To_Basic refers to two
+ -- functions: one that converts from Character to Character, and
+ -- the other that converts from String to String. The result of each
+ -- Character-to-Character function is described below, in terms of
+ -- the conversion applied to Item, its formal Character parameter. The
+ -- result of each String-to-String conversion is obtained by applying
+ -- to each element of the function's String parameter the corresponding
+ -- Character-to-Character conversion; the result is the null String if the
+ -- value of the formal parameter is the null String. The lower bound of the
+ -- result String is 1.
+
+ function To_Lower (Item : Character) return Character
+ with
+ Post => To_Lower'Result =
+ (if Is_Upper (Item) then
+ Character'Val (Character'Pos (Item) +
+ (if Item in 'A' .. 'Z' then
+ Character'Pos ('a') - Character'Pos ('A')
+ else
+ Character'Pos (Latin_1.LC_A_Grave)
+ - Character'Pos (Latin_1.UC_A_Grave)))
+ else
+ Item);
+ -- Returns the corresponding lower-case value for Item if Is_Upper(Item),
+ -- and returns Item otherwise.
- function To_Lower (Item : String) return String;
- function To_Upper (Item : String) return String;
- function To_Basic (Item : String) return String;
+ function To_Upper (Item : Character) return Character
+ with
+ Post => To_Upper'Result =
+ (if Is_Lower (Item)
+ and then Item not in Latin_1.LC_German_Sharp_S
+ | Latin_1.LC_Y_Diaeresis
+ then
+ Character'Val (Character'Pos (Item) +
+ (if Item in 'A' .. 'Z' then
+ Character'Pos ('A') - Character'Pos ('a')
+ else
+ Character'Pos (Latin_1.UC_A_Grave)
+ - Character'Pos (Latin_1.LC_A_Grave)))
+ else
+ Item);
+ -- Returns the corresponding upper-case value for Item if Is_Lower(Item)
+ -- and Item has an upper-case form, and returns Item otherwise. The lower
+ -- case letters LC_German_Sharp_S and LC_Y_Diaeresis do not have upper case
+ -- forms.
+
+ function To_Basic (Item : Character) return Character
+ with
+ Post => To_Basic'Result =
+ (if not Is_Letter (Item) or else Is_Basic (Item) then
+ Item
+ else
+ (case Item is
+ when Latin_1.UC_A_Grave .. Latin_1.UC_A_Ring => 'A',
+ when Latin_1.UC_C_Cedilla => 'C',
+ when Latin_1.UC_E_Grave .. Latin_1.UC_E_Diaeresis => 'E',
+ when Latin_1.UC_I_Grave .. Latin_1.UC_I_Diaeresis => 'I',
+ when Latin_1.UC_N_Tilde => 'N',
+ when Latin_1.UC_O_Grave .. Latin_1.UC_O_Diaeresis => 'O',
+ when Latin_1.UC_O_Oblique_Stroke => 'O',
+ when Latin_1.UC_U_Grave .. Latin_1.UC_U_Diaeresis => 'U',
+ when Latin_1.UC_Y_Acute => 'Y',
+ when Latin_1.LC_A_Grave .. Latin_1.LC_A_Ring => 'a',
+ when Latin_1.LC_C_Cedilla => 'c',
+ when Latin_1.LC_E_Grave .. Latin_1.LC_E_Diaeresis => 'e',
+ when Latin_1.LC_I_Grave .. Latin_1.LC_I_Diaeresis => 'i',
+ when Latin_1.LC_N_Tilde => 'n',
+ when Latin_1.LC_O_Grave .. Latin_1.LC_O_Diaeresis => 'o',
+ when Latin_1.LC_O_Oblique_Stroke => 'o',
+ when Latin_1.LC_U_Grave .. Latin_1.LC_U_Diaeresis => 'u',
+ when Latin_1.LC_Y_Acute => 'y',
+ when Latin_1.LC_Y_Diaeresis => 'y',
+ when others => raise Program_Error));
+ -- Returns the letter corresponding to Item but with no diacritical mark,
+ -- if Item is a letter but not a basic letter; returns Item otherwise.
+
+ function To_Lower (Item : String) return String
+ with
+ Post => To_Lower'Result'First = 1
+ and then To_Lower'Result'Length = Item'Length
+ and then
+ (for all J in To_Lower'Result'Range =>
+ To_Lower'Result (J) = To_Lower (Item (Item'First + (J - 1))));
+
+ function To_Upper (Item : String) return String
+ with
+ Post => To_Upper'Result'First = 1
+ and then To_Upper'Result'Length = Item'Length
+ and then
+ (for all J in To_Upper'Result'Range =>
+ To_Upper'Result (J) = To_Upper (Item (Item'First + (J - 1))));
+
+ function To_Basic (Item : String) return String
+ with
+ Post => To_Basic'Result'First = 1
+ and then To_Basic'Result'Length = Item'Length
+ and then
+ (for all J in To_Basic'Result'Range =>
+ To_Basic'Result (J) = To_Basic (Item (Item'First + (J - 1))));
----------------------------------------------------------------------
-- Classifications of and Conversions Between Character and ISO 646 --
----------------------------------------------------------------------
+ -- The following set of functions test for membership in the ISO 646
+ -- character range, or convert between ISO 646 and Character.
+
subtype ISO_646 is
Character range Character'Val (0) .. Character'Val (127);
- function Is_ISO_646 (Item : Character) return Boolean;
- function Is_ISO_646 (Item : String) return Boolean;
+ function Is_ISO_646 (Item : Character) return Boolean
+ with
+ Post => Is_ISO_646'Result = (Item in ISO_646);
+ -- The function whose formal parameter, Item, is of type Character returns
+ -- True if Item is in the subtype ISO_646.
+
+ function Is_ISO_646 (Item : String) return Boolean
+ with
+ Post => Is_ISO_646'Result =
+ (for all J in Item'Range => Is_ISO_646 (Item (J)));
+ -- The function whose formal parameter, Item, is of type String returns
+ -- True if Is_ISO_646(Item(I)) is True for each I in Item'Range.
function To_ISO_646
(Item : Character;
- Substitute : ISO_646 := ' ') return ISO_646;
+ Substitute : ISO_646 := ' ') return ISO_646
+ with
+ Post => To_ISO_646'Result =
+ (if Is_ISO_646 (Item) then Item else Substitute);
+ -- The function whose first formal parameter, Item, is of type Character
+ -- returns Item if Is_ISO_646(Item), and returns the Substitute ISO_646
+ -- character otherwise.
function To_ISO_646
(Item : String;
- Substitute : ISO_646 := ' ') return String;
+ Substitute : ISO_646 := ' ') return String
+ with
+ Post => To_ISO_646'Result'First = 1
+ and then To_ISO_646'Result'Length = Item'Length
+ and then
+ (for all J in To_ISO_646'Result'Range =>
+ To_ISO_646'Result (J) =
+ To_ISO_646 (Item (Item'First + (J - 1)), Substitute));
+ -- The function whose first formal parameter, Item, is of type String
+ -- returns the String whose Range is 1..Item'Length and each of whose
+ -- elements is given by To_ISO_646 of the corresponding element in Item.
------------------------------------------------------
-- Classifications of Wide_Character and Characters --
-- We do however have to flag these if the pragma No_Obsolescent_Features
-- restriction is active (see Restrict.Check_Obsolescent_2005_Entity).
- function Is_Character (Item : Wide_Character) return Boolean;
- function Is_String (Item : Wide_String) return Boolean;
+ function Is_Character (Item : Wide_Character) return Boolean
+ with
+ Post => Is_Character'Result =
+ (Wide_Character'Pos (Item) <= Character'Pos (Character'Last));
+ -- Returns True if Wide_Character'Pos(Item) <=
+ -- Character'Pos(Character'Last).
+
+ function Is_String (Item : Wide_String) return Boolean
+ with
+ Post => Is_String'Result =
+ (for all I in Item'Range => Is_Character (Item (I)));
+ -- Returns True if Is_Character(Item(I)) is True for each I in Item'Range.
------------------------------------------------------
-- Conversions between Wide_Character and Character --
function To_Character
(Item : Wide_Character;
- Substitute : Character := ' ') return Character;
+ Substitute : Character := ' ') return Character
+ with
+ Post => To_Character'Result =
+ (if Is_Character (Item) then
+ Character'Val (Wide_Character'Pos (Item))
+ else
+ Substitute);
+ -- Returns the Character corresponding to Item if Is_Character(Item), and
+ -- returns the Substitute Character otherwise.
function To_String
(Item : Wide_String;
- Substitute : Character := ' ') return String;
+ Substitute : Character := ' ') return String
+ with
+ Post => To_String'Result'First = 1
+ and then To_String'Result'Length = Item'Length
+ and then
+ (for all J in To_String'Result'Range =>
+ To_String'Result (J) =
+ To_Character (Item (Item'First + (J - 1)), Substitute));
+ -- Returns the String whose range is 1..Item'Length and each of whose
+ -- elements is given by To_Character of the corresponding element in Item.
function To_Wide_Character
- (Item : Character) return Wide_Character;
+ (Item : Character) return Wide_Character
+ with
+ Post => To_Wide_Character'Result =
+ Wide_Character'Val (Character'Pos (Item));
+ -- Returns the Wide_Character X such that Character'Pos(Item) =
+ -- Wide_Character'Pos (X).
function To_Wide_String
- (Item : String) return Wide_String;
+ (Item : String) return Wide_String
+ with
+ Post => To_Wide_String'Result'First = 1
+ and then To_Wide_String'Result'Length = Item'Length
+ and then
+ (for all J in To_Wide_String'Result'Range =>
+ To_Wide_String'Result (J) =
+ To_Wide_Character (Item (Item'First + (J - 1))));
+ -- Returns the Wide_String whose range is 1..Item'Length and each of whose
+ -- elements is given by To_Wide_Character of the corresponding element in
+ -- Item.
private
pragma Inline (Is_Alphanumeric);
projects / platform / upstream / gcc.git / commitdiff