[Ada] Proof of Ada.Characters.Handling

gcc/ada/

	* libgnat/a-chahan.adb: Add loop invariants as needed to prove
	subprograms.  Also use extended return statements where
	appropriate and not done already.  Mark data with
	Relaxed_Initialization where needed for initialization by parts.
	Convert regular functions to expression functions where needed
	for proof.
	* libgnat/a-chahan.ads: Add postconditions.
	* libgnat/a-strmap.ads (Model): New ghost function to create a
	publicly visible model of the private data Character_Mapping,
	needed in order to prove subprograms in Ada.Characters.Handling.

3 files changed, 428 insertions, 84 deletions

diff --git a/gcc/ada/libgnat/a-chahan.adb b/gcc/ada/libgnat/a-chahan.adb
index 827794c..411d485 100644
--- a/gcc/ada/libgnat/a-chahan.adb
+++ b/gcc/ada/libgnat/a-chahan.adb
@@ -29,11 +29,19 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+--  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 --
@@ -299,9 +307,7 @@ package body Ada.Characters.Handling is
    ------------------
 
    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 --
@@ -344,9 +350,7 @@ package body Ada.Characters.Handling is
    ----------------
 
    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
@@ -357,6 +361,8 @@ package body Ada.Characters.Handling is
          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;
@@ -456,6 +462,8 @@ package body Ada.Characters.Handling is
          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;
@@ -475,15 +483,18 @@ package body Ada.Characters.Handling is
    --------------
 
    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;
@@ -511,24 +522,25 @@ package body Ada.Characters.Handling is
    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;
 
    --------------
@@ -536,15 +548,18 @@ package body Ada.Characters.Handling is
    --------------
 
    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;
@@ -557,34 +572,40 @@ package body Ada.Characters.Handling is
      (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;
@@ -607,14 +628,19 @@ package body Ada.Characters.Handling is
    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;
diff --git a/gcc/ada/libgnat/a-chahan.ads b/gcc/ada/libgnat/a-chahan.ads
index 2f93e7c..093237d 100644
--- a/gcc/ada/libgnat/a-chahan.ads
+++ b/gcc/ada/libgnat/a-chahan.ads
@@ -33,7 +33,16 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-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
 
@@ -41,54 +50,296 @@ package Ada.Characters.Handling is
    -- 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 --
@@ -103,8 +354,18 @@ package Ada.Characters.Handling is
    --  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 --
@@ -121,17 +382,49 @@ package Ada.Characters.Handling is
 
    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);
diff --git a/gcc/ada/libgnat/a-strmap.ads b/gcc/ada/libgnat/a-strmap.ads
index c35c392..ffc69a9 100644
--- a/gcc/ada/libgnat/a-strmap.ads
+++ b/gcc/ada/libgnat/a-strmap.ads
@@ -35,9 +35,13 @@
 
 --  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.
+--  setting the corresponding assertion policy to Ignore. Postconditions and
+--  ghost code should not be executed at runtime as well, in order not to slow
+--  down the execution of these functions.
 
-pragma Assertion_Policy (Pre => Ignore);
+pragma Assertion_Policy (Pre   => Ignore,
+                         Post  => Ignore,
+                         Ghost => Ignore);
 
 with Ada.Characters.Latin_1;
 
@@ -210,9 +214,24 @@ package Ada.Strings.Maps is
    pragma Preelaborable_Initialization (Character_Mapping);
    --  Representation for a character to character mapping:
 
+   type SPARK_Proof_Character_Mapping_Model is
+     array (Character) of Character
+   with Ghost;
+   --  Publicly visible model of a Character_Mapping
+
+   function SPARK_Proof_Model
+     (Map : Character_Mapping)
+      return SPARK_Proof_Character_Mapping_Model
+   with Ghost;
+   --  Creation of a publicly visible model of a Character_Mapping
+
    function Value
      (Map     : Character_Mapping;
-      Element : Character) return Character;
+      Element : Character) return Character
+   with
+     Post => Value'Result = SPARK_Proof_Model (Map) (Element);
+   --  The function Value returns the Character value to which Element maps
+   --  with respect to the mapping represented by Map.
 
    Identity : constant Character_Mapping;
 
@@ -285,6 +304,12 @@ private
 
    type Character_Mapping is array (Character) of Character;
 
+   function SPARK_Proof_Model
+     (Map : Character_Mapping)
+      return SPARK_Proof_Character_Mapping_Model
+   is
+     (SPARK_Proof_Character_Mapping_Model (Map));
+
    package L renames Ada.Characters.Latin_1;
 
    Identity : constant Character_Mapping :=