[Ada] Proof of Interfaces.C with SPARK

gcc/ada/

	* libgnat/i-c.adb: Add ghost code.
	(C_Length_Ghost): New ghost functions to query the C length of a
	string.
	(To_Ada): Insert constant Count_Cst where needed to comply with
	SPARK.  Homogeneize code between variants for char, wchar_t,
	char16_t and char32_t. Use char16_nul and char32_nul
	systematically instead of their value. Fix the type of index To
	to be Integer instead of Positive, to avoid a possible range
	check failure on an empty Target. Insert an exit statement to
	avoid a possible overflow failure when the last index in Target
	is Natural'Last (possibly on a small string as well).
	* libgnat/i-c.ads: Add contracts.
	(C_Length_Ghost): New ghost functions to query the C length of a
	string.
	* libgnat/s-os_lib.adb: Remove pragma Compiler_Unit_Warning
	causing a spurious error during compilation of GNAT, as this
	pragma is not needed anymore now that we bootstrap (stage1) with
	the base compiler runtime.

3 files changed, 825 insertions, 69 deletions

diff --git a/gcc/ada/libgnat/i-c.adb b/gcc/ada/libgnat/i-c.adb
index 5be50ff..4ec920f 100644
--- a/gcc/ada/libgnat/i-c.adb
+++ b/gcc/ada/libgnat/i-c.adb
@@ -29,7 +29,77 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-package body Interfaces.C is
+--  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);
+
+package body Interfaces.C
+  with SPARK_Mode
+is
+
+   --------------------
+   -- C_Length_Ghost --
+   --------------------
+
+   function C_Length_Ghost (Item : char_array) return size_t is
+   begin
+      for J in Item'Range loop
+         if Item (J) = nul then
+            return J - Item'First;
+         end if;
+
+         pragma Loop_Invariant
+           (for all K in Item'First .. J => Item (K) /= nul);
+      end loop;
+
+      raise Program_Error;
+   end C_Length_Ghost;
+
+   function C_Length_Ghost (Item : wchar_array) return size_t is
+   begin
+      for J in Item'Range loop
+         if Item (J) = wide_nul then
+            return J - Item'First;
+         end if;
+
+         pragma Loop_Invariant
+           (for all K in Item'First .. J => Item (K) /= wide_nul);
+      end loop;
+
+      raise Program_Error;
+   end C_Length_Ghost;
+
+   function C_Length_Ghost (Item : char16_array) return size_t is
+   begin
+      for J in Item'Range loop
+         if Item (J) = char16_nul then
+            return J - Item'First;
+         end if;
+
+         pragma Loop_Invariant
+           (for all K in Item'First .. J => Item (K) /= char16_nul);
+      end loop;
+
+      raise Program_Error;
+   end C_Length_Ghost;
+
+   function C_Length_Ghost (Item : char32_array) return size_t is
+   begin
+      for J in Item'Range loop
+         if Item (J) = char32_nul then
+            return J - Item'First;
+         end if;
+
+         pragma Loop_Invariant
+           (for all K in Item'First .. J => Item (K) /= char32_nul);
+      end loop;
+
+      raise Program_Error;
+   end C_Length_Ghost;
 
    -----------------------
    -- Is_Nul_Terminated --
@@ -43,6 +113,9 @@ package body Interfaces.C is
          if Item (J) = nul then
             return True;
          end if;
+
+         pragma Loop_Invariant
+           (for all K in Item'First .. J => Item (K) /= nul);
       end loop;
 
       return False;
@@ -56,6 +129,9 @@ package body Interfaces.C is
          if Item (J) = wide_nul then
             return True;
          end if;
+
+         pragma Loop_Invariant
+           (for all K in Item'First .. J => Item (K) /= wide_nul);
       end loop;
 
       return False;
@@ -69,6 +145,9 @@ package body Interfaces.C is
          if Item (J) = char16_nul then
             return True;
          end if;
+
+         pragma Loop_Invariant
+           (for all K in Item'First .. J => Item (K) /= char16_nul);
       end loop;
 
       return False;
@@ -82,6 +161,9 @@ package body Interfaces.C is
          if Item (J) = char32_nul then
             return True;
          end if;
+
+         pragma Loop_Invariant
+           (for all K in Item'First .. J => Item (K) /= char32_nul);
       end loop;
 
       return False;
@@ -112,6 +194,13 @@ package body Interfaces.C is
          From := Item'First;
 
          loop
+            pragma Loop_Invariant (From in Item'Range);
+            pragma Loop_Invariant
+              (for some J in From .. Item'Last => Item (J) = nul);
+            pragma Loop_Invariant
+              (for all J in Item'First .. From when J /= From =>
+                 Item (J) /= nul);
+
             if From > Item'Last then
                raise Terminator_Error;
             elsif Item (From) = nul then
@@ -121,6 +210,8 @@ package body Interfaces.C is
             end if;
          end loop;
 
+         pragma Assert (From = Item'First + C_Length_Ghost (Item));
+
          Count := Natural (From - Item'First);
 
       else
@@ -128,11 +219,17 @@ package body Interfaces.C is
       end if;
 
       declare
-         R : String (1 .. Count);
+         Count_Cst : constant Natural := Count;
+         R : String (1 .. Count_Cst) with Relaxed_Initialization;
 
       begin
          for J in R'Range loop
-            R (J) := To_Ada (Item (size_t (J) + (Item'First - 1)));
+            R (J) := To_Ada (Item (size_t (J) - 1 + Item'First));
+
+            pragma Loop_Invariant (for all K in 1 .. J => R (K)'Initialized);
+            pragma Loop_Invariant
+              (for all K in 1 .. J =>
+                R (K) = To_Ada (Item (size_t (K) - 1 + Item'First)));
          end loop;
 
          return R;
@@ -148,12 +245,19 @@ package body Interfaces.C is
       Trim_Nul : Boolean := True)
    is
       From : size_t;
-      To   : Positive;
+      To   : Integer;
 
    begin
       if Trim_Nul then
          From := Item'First;
          loop
+            pragma Loop_Invariant (From in Item'Range);
+            pragma Loop_Invariant
+              (for some J in From .. Item'Last => Item (J) = nul);
+            pragma Loop_Invariant
+              (for all J in Item'First .. From when J /= From =>
+                Item (J) /= nul);
+
             if From > Item'Last then
                raise Terminator_Error;
             elsif Item (From) = nul then
@@ -178,11 +282,28 @@ package body Interfaces.C is
 
          for J in 1 .. Count loop
             Target (To) := Character (Item (From));
+
+            pragma Loop_Invariant (From in Item'Range);
+            pragma Loop_Invariant (To in Target'Range);
+            pragma Loop_Invariant (To = Target'First + (J - 1));
+            pragma Loop_Invariant (From = Item'First + size_t (J - 1));
+            pragma Loop_Invariant
+              (for all J in Target'First .. To => Target (J)'Initialized);
+            pragma Loop_Invariant
+              (Target (Target'First .. To)'Initialized);
+            pragma Loop_Invariant
+              (for all K in Target'First .. To =>
+                Target (K) =
+                  To_Ada (Item (size_t (K - Target'First) + Item'First)));
+
+            --  Avoid possible overflow when incrementing To in the last
+            --  iteration of the loop.
+            exit when J = Count;
+
             From := From + 1;
             To   := To + 1;
          end loop;
       end if;
-
    end To_Ada;
 
    --  Convert wchar_t to Wide_Character
@@ -206,6 +327,13 @@ package body Interfaces.C is
          From := Item'First;
 
          loop
+            pragma Loop_Invariant (From in Item'Range);
+            pragma Loop_Invariant
+              (for some J in From .. Item'Last => Item (J) = wide_nul);
+            pragma Loop_Invariant
+              (for all J in Item'First .. From when J /= From =>
+                 Item (J) /= wide_nul);
+
             if From > Item'Last then
                raise Terminator_Error;
             elsif Item (From) = wide_nul then
@@ -215,6 +343,8 @@ package body Interfaces.C is
             end if;
          end loop;
 
+         pragma Assert (From = Item'First + C_Length_Ghost (Item));
+
          Count := Natural (From - Item'First);
 
       else
@@ -222,11 +352,17 @@ package body Interfaces.C is
       end if;
 
       declare
-         R : Wide_String (1 .. Count);
+         Count_Cst : constant Natural := Count;
+         R : Wide_String (1 .. Count_Cst) with Relaxed_Initialization;
 
       begin
          for J in R'Range loop
-            R (J) := To_Ada (Item (size_t (J) + (Item'First - 1)));
+            R (J) := To_Ada (Item (size_t (J) - 1 + Item'First));
+
+            pragma Loop_Invariant (for all K in 1 .. J => R (K)'Initialized);
+            pragma Loop_Invariant
+              (for all K in 1 .. J =>
+                R (K) = To_Ada (Item (size_t (K) - 1 + Item'First)));
          end loop;
 
          return R;
@@ -242,12 +378,19 @@ package body Interfaces.C is
       Trim_Nul : Boolean := True)
    is
       From : size_t;
-      To   : Positive;
+      To   : Integer;
 
    begin
       if Trim_Nul then
          From := Item'First;
          loop
+            pragma Loop_Invariant (From in Item'Range);
+            pragma Loop_Invariant
+              (for some J in From .. Item'Last => Item (J) = wide_nul);
+            pragma Loop_Invariant
+              (for all J in Item'First .. From when J /= From =>
+                Item (J) /= wide_nul);
+
             if From > Item'Last then
                raise Terminator_Error;
             elsif Item (From) = wide_nul then
@@ -272,6 +415,24 @@ package body Interfaces.C is
 
          for J in 1 .. Count loop
             Target (To) := To_Ada (Item (From));
+
+            pragma Loop_Invariant (From in Item'Range);
+            pragma Loop_Invariant (To in Target'Range);
+            pragma Loop_Invariant (To = Target'First + (J - 1));
+            pragma Loop_Invariant (From = Item'First + size_t (J - 1));
+            pragma Loop_Invariant
+              (for all J in Target'First .. To => Target (J)'Initialized);
+            pragma Loop_Invariant
+              (Target (Target'First .. To)'Initialized);
+            pragma Loop_Invariant
+              (for all K in Target'First .. To =>
+                Target (K) =
+                  To_Ada (Item (size_t (K - Target'First) + Item'First)));
+
+            --  Avoid possible overflow when incrementing To in the last
+            --  iteration of the loop.
+            exit when J = Count;
+
             From := From + 1;
             To   := To + 1;
          end loop;
@@ -299,15 +460,24 @@ package body Interfaces.C is
          From := Item'First;
 
          loop
+            pragma Loop_Invariant (From in Item'Range);
+            pragma Loop_Invariant
+              (for some J in From .. Item'Last => Item (J) = char16_nul);
+            pragma Loop_Invariant
+              (for all J in Item'First .. From when J /= From =>
+                 Item (J) /= char16_nul);
+
             if From > Item'Last then
                raise Terminator_Error;
-            elsif Item (From) = char16_t'Val (0) then
+            elsif Item (From) = char16_nul then
                exit;
             else
                From := From + 1;
             end if;
          end loop;
 
+         pragma Assert (From = Item'First + C_Length_Ghost (Item));
+
          Count := Natural (From - Item'First);
 
       else
@@ -315,11 +485,17 @@ package body Interfaces.C is
       end if;
 
       declare
-         R : Wide_String (1 .. Count);
+         Count_Cst : constant Natural := Count;
+         R : Wide_String (1 .. Count_Cst) with Relaxed_Initialization;
 
       begin
          for J in R'Range loop
-            R (J) := To_Ada (Item (size_t (J) + (Item'First - 1)));
+            R (J) := To_Ada (Item (size_t (J) - 1 + Item'First));
+
+            pragma Loop_Invariant (for all K in 1 .. J => R (K)'Initialized);
+            pragma Loop_Invariant
+              (for all K in 1 .. J =>
+                R (K) = To_Ada (Item (size_t (K) - 1 + Item'First)));
          end loop;
 
          return R;
@@ -335,15 +511,22 @@ package body Interfaces.C is
       Trim_Nul : Boolean := True)
    is
       From : size_t;
-      To   : Positive;
+      To   : Integer;
 
    begin
       if Trim_Nul then
          From := Item'First;
          loop
+            pragma Loop_Invariant (From in Item'Range);
+            pragma Loop_Invariant
+              (for some J in From .. Item'Last => Item (J) = char16_nul);
+            pragma Loop_Invariant
+              (for all J in Item'First .. From when J /= From =>
+                Item (J) /= char16_nul);
+
             if From > Item'Last then
                raise Terminator_Error;
-            elsif Item (From) = char16_t'Val (0) then
+            elsif Item (From) = char16_nul then
                exit;
             else
                From := From + 1;
@@ -365,6 +548,24 @@ package body Interfaces.C is
 
          for J in 1 .. Count loop
             Target (To) := To_Ada (Item (From));
+
+            pragma Loop_Invariant (From in Item'Range);
+            pragma Loop_Invariant (To in Target'Range);
+            pragma Loop_Invariant (To = Target'First + (J - 1));
+            pragma Loop_Invariant (From = Item'First + size_t (J - 1));
+            pragma Loop_Invariant
+              (for all J in Target'First .. To => Target (J)'Initialized);
+            pragma Loop_Invariant
+              (Target (Target'First .. To)'Initialized);
+            pragma Loop_Invariant
+              (for all K in Target'First .. To =>
+                Target (K) =
+                  To_Ada (Item (size_t (K - Target'First) + Item'First)));
+
+            --  Avoid possible overflow when incrementing To in the last
+            --  iteration of the loop.
+            exit when J = Count;
+
             From := From + 1;
             To   := To + 1;
          end loop;
@@ -392,15 +593,24 @@ package body Interfaces.C is
          From := Item'First;
 
          loop
+            pragma Loop_Invariant (From in Item'Range);
+            pragma Loop_Invariant
+              (for some J in From .. Item'Last => Item (J) = char32_nul);
+            pragma Loop_Invariant
+              (for all J in Item'First .. From when J /= From =>
+                 Item (J) /= char32_nul);
+
             if From > Item'Last then
                raise Terminator_Error;
-            elsif Item (From) = char32_t'Val (0) then
+            elsif Item (From) = char32_nul then
                exit;
             else
                From := From + 1;
             end if;
          end loop;
 
+         pragma Assert (From = Item'First + C_Length_Ghost (Item));
+
          Count := Natural (From - Item'First);
 
       else
@@ -408,11 +618,17 @@ package body Interfaces.C is
       end if;
 
       declare
-         R : Wide_Wide_String (1 .. Count);
+         Count_Cst : constant Natural := Count;
+         R : Wide_Wide_String (1 .. Count_Cst) with Relaxed_Initialization;
 
       begin
          for J in R'Range loop
-            R (J) := To_Ada (Item (size_t (J) + (Item'First - 1)));
+            R (J) := To_Ada (Item (size_t (J) - 1 + Item'First));
+
+            pragma Loop_Invariant (for all K in 1 .. J => R (K)'Initialized);
+            pragma Loop_Invariant
+              (for all K in 1 .. J =>
+                R (K) = To_Ada (Item (size_t (K) - 1 + Item'First)));
          end loop;
 
          return R;
@@ -428,15 +644,22 @@ package body Interfaces.C is
       Trim_Nul : Boolean := True)
    is
       From : size_t;
-      To   : Positive;
+      To   : Integer;
 
    begin
       if Trim_Nul then
          From := Item'First;
          loop
+            pragma Loop_Invariant (From in Item'Range);
+            pragma Loop_Invariant
+              (for some J in From .. Item'Last => Item (J) = char32_nul);
+            pragma Loop_Invariant
+              (for all J in Item'First .. From when J /= From =>
+                Item (J) /= char32_nul);
+
             if From > Item'Last then
                raise Terminator_Error;
-            elsif Item (From) = char32_t'Val (0) then
+            elsif Item (From) = char32_nul then
                exit;
             else
                From := From + 1;
@@ -458,6 +681,24 @@ package body Interfaces.C is
 
          for J in 1 .. Count loop
             Target (To) := To_Ada (Item (From));
+
+            pragma Loop_Invariant (From in Item'Range);
+            pragma Loop_Invariant (To in Target'Range);
+            pragma Loop_Invariant (To = Target'First + (J - 1));
+            pragma Loop_Invariant (From = Item'First + size_t (J - 1));
+            pragma Loop_Invariant
+              (for all J in Target'First .. To => Target (J)'Initialized);
+            pragma Loop_Invariant
+              (Target (Target'First .. To)'Initialized);
+            pragma Loop_Invariant
+              (for all K in Target'First .. To =>
+                Target (K) =
+                  To_Ada (Item (size_t (K - Target'First) + Item'First)));
+
+            --  Avoid possible overflow when incrementing To in the last
+            --  iteration of the loop.
+            exit when J = Count;
+
             From := From + 1;
             To   := To + 1;
          end loop;
@@ -484,14 +725,26 @@ package body Interfaces.C is
    begin
       if Append_Nul then
          declare
-            R : char_array (0 .. Item'Length);
+            R : char_array (0 .. Item'Length) with Relaxed_Initialization;
 
          begin
             for J in Item'Range loop
                R (size_t (J - Item'First)) := To_C (Item (J));
+
+               pragma Loop_Invariant
+                 (for all K in 0 .. size_t (J - Item'First) =>
+                    R (K)'Initialized);
+               pragma Loop_Invariant
+                 (for all K in Item'First .. J =>
+                    R (size_t (K - Item'First)) = To_C (Item (K)));
             end loop;
 
             R (R'Last) := nul;
+
+            pragma Assert
+              (for all J in Item'Range =>
+                 R (size_t (J - Item'First)) = To_C (Item (J)));
+
             return R;
          end;
 
@@ -512,11 +765,19 @@ package body Interfaces.C is
 
          else
             declare
-               R : char_array (0 .. Item'Length - 1);
+               R : char_array (0 .. Item'Length - 1)
+                 with Relaxed_Initialization;
 
             begin
                for J in Item'Range loop
                   R (size_t (J - Item'First)) := To_C (Item (J));
+
+                  pragma Loop_Invariant
+                    (for all K in 0 .. size_t (J - Item'First) =>
+                       R (K)'Initialized);
+                  pragma Loop_Invariant
+                    (for all K in Item'First .. J =>
+                       R (size_t (K - Item'First)) = To_C (Item (K)));
                end loop;
 
                return R;
@@ -543,6 +804,19 @@ package body Interfaces.C is
          To := Target'First;
          for From in Item'Range loop
             Target (To) := char (Item (From));
+
+            pragma Loop_Invariant (To in Target'Range);
+            pragma Loop_Invariant
+              (To - Target'First = size_t (From - Item'First));
+            pragma Loop_Invariant
+              (for all J in Target'First .. To => Target (J)'Initialized);
+            pragma Loop_Invariant
+              (Target (Target'First .. To)'Initialized);
+            pragma Loop_Invariant
+              (for all J in Item'First .. From =>
+                 Target (Target'First + size_t (J - Item'First)) =
+                   To_C (Item (J)));
+
             To := To + 1;
          end loop;
 
@@ -576,14 +850,26 @@ package body Interfaces.C is
    begin
       if Append_Nul then
          declare
-            R : wchar_array (0 .. Item'Length);
+            R : wchar_array (0 .. Item'Length) with Relaxed_Initialization;
 
          begin
             for J in Item'Range loop
                R (size_t (J - Item'First)) := To_C (Item (J));
+
+               pragma Loop_Invariant
+                 (for all K in 0 .. size_t (J - Item'First) =>
+                    R (K)'Initialized);
+               pragma Loop_Invariant
+                 (for all K in Item'First .. J =>
+                    R (size_t (K - Item'First)) = To_C (Item (K)));
             end loop;
 
             R (R'Last) := wide_nul;
+
+            pragma Assert
+              (for all J in Item'Range =>
+                 R (size_t (J - Item'First)) = To_C (Item (J)));
+
             return R;
          end;
 
@@ -600,11 +886,19 @@ package body Interfaces.C is
 
          else
             declare
-               R : wchar_array (0 .. Item'Length - 1);
+               R : wchar_array (0 .. Item'Length - 1)
+                 with Relaxed_Initialization;
 
             begin
-               for J in size_t range 0 .. Item'Length - 1 loop
-                  R (J) := To_C (Item (Integer (J) + Item'First));
+               for J in Item'Range loop
+                  R (size_t (J - Item'First)) := To_C (Item (J));
+
+                  pragma Loop_Invariant
+                    (for all K in 0 .. size_t (J - Item'First) =>
+                       R (K)'Initialized);
+                  pragma Loop_Invariant
+                    (for all K in Item'First .. J =>
+                       R (size_t (K - Item'First)) = To_C (Item (K)));
                end loop;
 
                return R;
@@ -631,9 +925,31 @@ package body Interfaces.C is
          To := Target'First;
          for From in Item'Range loop
             Target (To) := To_C (Item (From));
+
+            pragma Loop_Invariant (To in Target'Range);
+            pragma Loop_Invariant
+              (To - Target'First = size_t (From - Item'First));
+            pragma Loop_Invariant
+              (for all J in Target'First .. To => Target (J)'Initialized);
+            pragma Loop_Invariant
+              (Target (Target'First .. To)'Initialized);
+            pragma Loop_Invariant
+              (for all J in Item'First .. From =>
+                Target (Target'First + size_t (J - Item'First)) =
+                  To_C (Item (J)));
+
             To := To + 1;
          end loop;
 
+         pragma Assert
+           (for all J in Item'Range =>
+             Target (Target'First + size_t (J - Item'First)) =
+               To_C (Item (J)));
+         pragma Assert
+           (if Item'Length /= 0 then
+             Target (Target'First ..
+                     Target'First + (Item'Length - 1))'Initialized);
+
          if Append_Nul then
             if To > Target'Last then
                raise Constraint_Error;
@@ -664,14 +980,26 @@ package body Interfaces.C is
    begin
       if Append_Nul then
          declare
-            R : char16_array (0 .. Item'Length);
+            R : char16_array (0 .. Item'Length) with Relaxed_Initialization;
 
          begin
             for J in Item'Range loop
                R (size_t (J - Item'First)) := To_C (Item (J));
+
+               pragma Loop_Invariant
+                 (for all K in 0 .. size_t (J - Item'First) =>
+                    R (K)'Initialized);
+               pragma Loop_Invariant
+                 (for all K in Item'First .. J =>
+                    R (size_t (K - Item'First)) = To_C (Item (K)));
             end loop;
 
-            R (R'Last) := char16_t'Val (0);
+            R (R'Last) := char16_nul;
+
+            pragma Assert
+              (for all J in Item'Range =>
+                 R (size_t (J - Item'First)) = To_C (Item (J)));
+
             return R;
          end;
 
@@ -688,11 +1016,19 @@ package body Interfaces.C is
 
          else
             declare
-               R : char16_array (0 .. Item'Length - 1);
+               R : char16_array (0 .. Item'Length - 1)
+                 with Relaxed_Initialization;
 
             begin
-               for J in size_t range 0 .. Item'Length - 1 loop
-                  R (J) := To_C (Item (Integer (J) + Item'First));
+               for J in Item'Range loop
+                  R (size_t (J - Item'First)) := To_C (Item (J));
+
+                  pragma Loop_Invariant
+                    (for all K in 0 .. size_t (J - Item'First) =>
+                       R (K)'Initialized);
+                  pragma Loop_Invariant
+                    (for all K in Item'First .. J =>
+                       R (size_t (K - Item'First)) = To_C (Item (K)));
                end loop;
 
                return R;
@@ -719,14 +1055,36 @@ package body Interfaces.C is
          To := Target'First;
          for From in Item'Range loop
             Target (To) := To_C (Item (From));
+
+            pragma Loop_Invariant (To in Target'Range);
+            pragma Loop_Invariant
+              (To - Target'First = size_t (From - Item'First));
+            pragma Loop_Invariant
+              (for all J in Target'First .. To => Target (J)'Initialized);
+            pragma Loop_Invariant
+              (Target (Target'First .. To)'Initialized);
+            pragma Loop_Invariant
+              (for all J in Item'First .. From =>
+                Target (Target'First + size_t (J - Item'First)) =
+                  To_C (Item (J)));
+
             To := To + 1;
          end loop;
 
+         pragma Assert
+           (for all J in Item'Range =>
+             Target (Target'First + size_t (J - Item'First)) =
+               To_C (Item (J)));
+         pragma Assert
+           (if Item'Length /= 0 then
+             Target (Target'First ..
+                     Target'First + (Item'Length - 1))'Initialized);
+
          if Append_Nul then
             if To > Target'Last then
                raise Constraint_Error;
             else
-               Target (To) := char16_t'Val (0);
+               Target (To) := char16_nul;
                Count := Item'Length + 1;
             end if;
 
@@ -752,14 +1110,26 @@ package body Interfaces.C is
    begin
       if Append_Nul then
          declare
-            R : char32_array (0 .. Item'Length);
+            R : char32_array (0 .. Item'Length) with Relaxed_Initialization;
 
          begin
             for J in Item'Range loop
                R (size_t (J - Item'First)) := To_C (Item (J));
+
+               pragma Loop_Invariant
+                 (for all K in 0 .. size_t (J - Item'First) =>
+                    R (K)'Initialized);
+               pragma Loop_Invariant
+                 (for all K in Item'First .. J =>
+                    R (size_t (K - Item'First)) = To_C (Item (K)));
             end loop;
 
-            R (R'Last) := char32_t'Val (0);
+            R (R'Last) := char32_nul;
+
+            pragma Assert
+              (for all J in Item'Range =>
+                 R (size_t (J - Item'First)) = To_C (Item (J)));
+
             return R;
          end;
 
@@ -775,11 +1145,19 @@ package body Interfaces.C is
 
          else
             declare
-               R : char32_array (0 .. Item'Length - 1);
+               R : char32_array (0 .. Item'Length - 1)
+                 with Relaxed_Initialization;
 
             begin
-               for J in size_t range 0 .. Item'Length - 1 loop
-                  R (J) := To_C (Item (Integer (J) + Item'First));
+               for J in Item'Range loop
+                  R (size_t (J - Item'First)) := To_C (Item (J));
+
+                  pragma Loop_Invariant
+                    (for all K in 0 .. size_t (J - Item'First) =>
+                       R (K)'Initialized);
+                  pragma Loop_Invariant
+                    (for all K in Item'First .. J =>
+                       R (size_t (K - Item'First)) = To_C (Item (K)));
                end loop;
 
                return R;
@@ -806,14 +1184,36 @@ package body Interfaces.C is
          To := Target'First;
          for From in Item'Range loop
             Target (To) := To_C (Item (From));
+
+            pragma Loop_Invariant (To in Target'Range);
+            pragma Loop_Invariant
+              (To - Target'First = size_t (From - Item'First));
+            pragma Loop_Invariant
+              (for all J in Target'First .. To => Target (J)'Initialized);
+            pragma Loop_Invariant
+              (Target (Target'First .. To)'Initialized);
+            pragma Loop_Invariant
+              (for all J in Item'First .. From =>
+                Target (Target'First + size_t (J - Item'First)) =
+                  To_C (Item (J)));
+
             To := To + 1;
          end loop;
 
+         pragma Assert
+           (for all J in Item'Range =>
+             Target (Target'First + size_t (J - Item'First)) =
+               To_C (Item (J)));
+         pragma Assert
+           (if Item'Length /= 0 then
+             Target (Target'First ..
+                     Target'First + (Item'Length - 1))'Initialized);
+
          if Append_Nul then
             if To > Target'Last then
                raise Constraint_Error;
             else
-               Target (To) := char32_t'Val (0);
+               Target (To) := char32_nul;
                Count := Item'Length + 1;
             end if;
 
diff --git a/gcc/ada/libgnat/i-c.ads b/gcc/ada/libgnat/i-c.ads
index 428ea49..2023b75 100644
--- a/gcc/ada/libgnat/i-c.ads
+++ b/gcc/ada/libgnat/i-c.ads
@@ -13,10 +13,30 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+--  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 System.Parameters;
 
-package Interfaces.C is
-   pragma Pure;
+package Interfaces.C
+  with SPARK_Mode, Pure
+is
+   --  Each of the types declared in Interfaces.C is C-compatible.
+
+   --  The types int, short, long, unsigned, ptrdiff_t, size_t, double,
+   --  char, wchar_t, char16_t, and char32_t correspond respectively to the
+   --  C types having the same names. The types signed_char, unsigned_short,
+   --  unsigned_long, unsigned_char, C_bool, C_float, and long_double
+   --  correspond respectively to the C types signed char, unsigned
+   --  short, unsigned long, unsigned char, bool, float, and long double.
 
    --  Declaration's based on C's <limits.h>
 
@@ -49,7 +69,11 @@ package Interfaces.C is
    type unsigned_char is mod (UCHAR_MAX + 1);
    for unsigned_char'Size use CHAR_BIT;
 
-   subtype plain_char is unsigned_char; -- ??? should be parameterized
+   --  Note: Ada RM states that the type of the subtype plain_char is either
+   --  signed_char or unsigned_char, depending on the C implementation. GNAT
+   --  instead choses unsigned_char always.
+
+   subtype plain_char is unsigned_char;
 
    --  Note: the Integer qualifications used in the declaration of ptrdiff_t
    --  avoid ambiguities when compiling in the presence of s-auxdec.ads and
@@ -80,33 +104,133 @@ package Interfaces.C is
 
    nul : constant char := char'First;
 
-   function To_C   (Item : Character) return char;
-   function To_Ada (Item : char)      return Character;
+   --  The functions To_C and To_Ada map between the Ada type Character and the
+   --  C type char.
+
+   function To_C (Item : Character) return char
+   with
+     Post => To_C'Result = char'Val (Character'Pos (Item));
+
+   function To_Ada (Item : char) return Character
+   with
+     Post => To_Ada'Result = Character'Val (char'Pos (Item));
 
    type char_array is array (size_t range <>) of aliased char;
    for char_array'Component_Size use CHAR_BIT;
 
-   function Is_Nul_Terminated (Item : char_array) return Boolean;
+   function Is_Nul_Terminated (Item : char_array) return Boolean
+   with
+     Post => Is_Nul_Terminated'Result = (for some C of Item => C = nul);
+   --  The result of Is_Nul_Terminated is True if Item contains nul, and is
+   --  False otherwise.
+
+   function C_Length_Ghost (Item : char_array) return size_t
+   with
+     Ghost,
+     Pre  => Is_Nul_Terminated (Item),
+     Post => C_Length_Ghost'Result <= Item'Last - Item'First
+       and then Item (Item'First + C_Length_Ghost'Result) = nul
+       and then (for all J in Item'First .. Item'First + C_Length_Ghost'Result
+                   when J /= Item'First + C_Length_Ghost'Result =>
+                     Item (J) /= nul);
+   --  Ghost function to compute the length of a char_array up to the first nul
+   --  character.
 
    function To_C
      (Item       : String;
-      Append_Nul : Boolean := True) return char_array;
+      Append_Nul : Boolean := True) return char_array
+   with
+     Pre  => not (Append_Nul = False and then Item'Length = 0),
+     Post => To_C'Result'First = 0
+       and then To_C'Result'Length =
+         (if Append_Nul then Item'Length + 1 else Item'Length)
+       and then (for all J in Item'Range =>
+                   To_C'Result (size_t (J - Item'First)) = To_C (Item (J)))
+       and then (if Append_Nul then To_C'Result (To_C'Result'Last) = nul);
+   --  The result of To_C is a char_array value of length Item'Length (if
+   --  Append_Nul is False) or Item'Length+1 (if Append_Nul is True). The lower
+   --  bound is 0. For each component Item(I), the corresponding component
+   --  in the result is To_C applied to Item(I). The value nul is appended if
+   --  Append_Nul is True. If Append_Nul is False and Item'Length is 0, then
+   --  To_C propagates Constraint_Error.
 
    function To_Ada
      (Item     : char_array;
-      Trim_Nul : Boolean := True) return String;
+      Trim_Nul : Boolean := True) return String
+   with
+     Pre  => (if Trim_Nul then
+                Is_Nul_Terminated (Item)
+                  and then C_Length_Ghost (Item) <= size_t (Natural'Last)
+              else
+                Item'Last - Item'First < size_t (Natural'Last)),
+     Post => To_Ada'Result'First = 1
+       and then To_Ada'Result'Length =
+         (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
+       and then (for all J in To_Ada'Result'Range =>
+                   To_Ada'Result (J) =
+                     To_Ada (Item (size_t (J) - 1 + Item'First)));
+   --  The result of To_Ada is a String whose length is Item'Length (if
+   --  Trim_Nul is False) or the length of the slice of Item preceding the
+   --  first nul (if Trim_Nul is True). The lower bound of the result is 1.
+   --  If Trim_Nul is False, then for each component Item(I) the corresponding
+   --  component in the result is To_Ada applied to Item(I). If Trim_Nul
+   --  is True, then for each component Item(I) before the first nul the
+   --  corresponding component in the result is To_Ada applied to Item(I). The
+   --  function propagates Terminator_Error if Trim_Nul is True and Item does
+   --  not contain nul.
 
    procedure To_C
      (Item       : String;
       Target     : out char_array;
       Count      : out size_t;
-      Append_Nul : Boolean := True);
+      Append_Nul : Boolean := True)
+   with
+     Relaxed_Initialization => Target,
+     Pre  => Target'Length >=
+       (if Append_Nul then Item'Length + 1 else Item'Length),
+     Post => Count = (if Append_Nul then Item'Length + 1 else Item'Length)
+       and then
+         (if Count /= 0 then
+           Target (Target'First .. Target'First + (Count - 1))'Initialized)
+       and then
+         (for all J in Item'Range =>
+           Target (Target'First + size_t (J - Item'First)) = To_C (Item (J)))
+       and then
+         (if Append_Nul then Target (Target'First + (Count - 1)) = nul);
+   --  For procedure To_C, each element of Item is converted (via the To_C
+   --  function) to a char, which is assigned to the corresponding element of
+   --  Target. If Append_Nul is True, nul is then assigned to the next element
+   --  of Target. In either case, Count is set to the number of Target elements
+   --  assigned. If Target is not long enough, Constraint_Error is propagated.
 
    procedure To_Ada
      (Item     : char_array;
       Target   : out String;
       Count    : out Natural;
-      Trim_Nul : Boolean := True);
+      Trim_Nul : Boolean := True)
+   with
+     Relaxed_Initialization => Target,
+     Pre  => (if Trim_Nul then
+                Is_Nul_Terminated (Item)
+                  and then C_Length_Ghost (Item) <= size_t (Target'Length)
+              else
+                Item'Last - Item'First < size_t (Target'Length)),
+     Post => Count =
+         (if Trim_Nul then Natural (C_Length_Ghost (Item)) else Item'Length)
+       and then
+         (if Count /= 0 then
+           Target (Target'First .. Target'First + (Count - 1))'Initialized)
+       and then
+         (for all J in Target'First .. Target'First + (Count - 1) =>
+           Target (J) =
+             To_Ada (Item (size_t (J - Target'First) + Item'First)));
+   --  For procedure To_Ada, each element of Item (if Trim_Nul is False) or
+   --  each element of Item preceding the first nul (if Trim_Nul is True) is
+   --  converted (via the To_Ada function) to a Character, which is assigned
+   --  to the corresponding element of Target. Count is set to the number of
+   --  Target elements assigned. If Target is not long enough, Constraint_Error
+   --  is propagated. If Trim_Nul is True and Item does not contain nul, then
+   --  Terminator_Error is propagated.
 
    ------------------------------------
    -- Wide Character and Wide String --
@@ -117,32 +241,110 @@ package Interfaces.C is
 
    wide_nul : constant wchar_t := wchar_t'First;
 
-   function To_C   (Item : Wide_Character) return wchar_t;
-   function To_Ada (Item : wchar_t)        return Wide_Character;
+   --  To_C and To_Ada provide the mappings between the Ada and C wide
+   --  character types.
+
+   function To_C (Item : Wide_Character) return wchar_t
+   with
+     Post => To_C'Result = wchar_t (Item);
+
+   function To_Ada (Item : wchar_t) return Wide_Character
+   with
+     Post => To_Ada'Result = Wide_Character (Item);
 
    type wchar_array is array (size_t range <>) of aliased wchar_t;
 
-   function Is_Nul_Terminated (Item : wchar_array) return Boolean;
+   function Is_Nul_Terminated (Item : wchar_array) return Boolean
+   with
+     Post => Is_Nul_Terminated'Result = (for some C of Item => C = wide_nul);
+   --  The result of Is_Nul_Terminated is True if Item contains wide_nul, and
+   --  is False otherwise.
+
+   --  The To_C and To_Ada subprograms that convert between Wide_String and
+   --  wchar_array have analogous effects to the To_C and To_Ada subprograms
+   --  that convert between String and char_array, except that wide_nul is
+   --  used instead of nul.
+
+   function C_Length_Ghost (Item : wchar_array) return size_t
+   with
+     Ghost,
+     Pre  => Is_Nul_Terminated (Item),
+     Post => C_Length_Ghost'Result <= Item'Last - Item'First
+       and then Item (Item'First + C_Length_Ghost'Result) = wide_nul
+       and then (for all J in Item'First .. Item'First + C_Length_Ghost'Result
+                   when J /= Item'First + C_Length_Ghost'Result =>
+                     Item (J) /= wide_nul);
+   --  Ghost function to compute the length of a wchar_array up to the first
+   --  wide_nul character.
 
    function To_C
      (Item       : Wide_String;
-      Append_Nul : Boolean := True) return wchar_array;
+      Append_Nul : Boolean := True) return wchar_array
+   with
+     Pre  => not (Append_Nul = False and then Item'Length = 0),
+     Post => To_C'Result'First = 0
+       and then To_C'Result'Length =
+         (if Append_Nul then Item'Length + 1 else Item'Length)
+       and then (for all J in Item'Range =>
+                   To_C'Result (size_t (J - Item'First)) = To_C (Item (J)))
+       and then (if Append_Nul then To_C'Result (To_C'Result'Last) = wide_nul);
 
    function To_Ada
      (Item     : wchar_array;
-      Trim_Nul : Boolean := True) return Wide_String;
+      Trim_Nul : Boolean := True) return Wide_String
+   with
+     Pre  => (if Trim_Nul then
+                Is_Nul_Terminated (Item)
+                  and then C_Length_Ghost (Item) <= size_t (Natural'Last)
+              else
+                Item'Last - Item'First < size_t (Natural'Last)),
+     Post => To_Ada'Result'First = 1
+       and then To_Ada'Result'Length =
+         (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
+       and then (for all J in To_Ada'Result'Range =>
+                   To_Ada'Result (J) =
+                     To_Ada (Item (size_t (J) - 1 + Item'First)));
 
    procedure To_C
      (Item       : Wide_String;
       Target     : out wchar_array;
       Count      : out size_t;
-      Append_Nul : Boolean := True);
+      Append_Nul : Boolean := True)
+   with
+     Relaxed_Initialization => Target,
+     Pre  => Target'Length >=
+       (if Append_Nul then Item'Length + 1 else Item'Length),
+     Post => Count = (if Append_Nul then Item'Length + 1 else Item'Length)
+       and then
+         (if Count /= 0 then
+           Target (Target'First .. Target'First + (Count - 1))'Initialized)
+       and then
+         (for all J in Item'Range =>
+           Target (Target'First + size_t (J - Item'First)) = To_C (Item (J)))
+       and then
+         (if Append_Nul then Target (Target'First + (Count - 1)) = wide_nul);
 
    procedure To_Ada
      (Item     : wchar_array;
       Target   : out Wide_String;
       Count    : out Natural;
-      Trim_Nul : Boolean := True);
+      Trim_Nul : Boolean := True)
+   with
+     Relaxed_Initialization => Target,
+     Pre  => (if Trim_Nul then
+                Is_Nul_Terminated (Item)
+                  and then C_Length_Ghost (Item) <= size_t (Target'Length)
+              else
+                Item'Last - Item'First < size_t (Target'Length)),
+     Post => Count =
+         (if Trim_Nul then Natural (C_Length_Ghost (Item)) else Item'Length)
+       and then
+         (if Count /= 0 then
+           Target (Target'First .. Target'First + (Count - 1))'Initialized)
+       and then
+         (for all J in Target'First .. Target'First + (Count - 1) =>
+           Target (J) =
+             To_Ada (Item (size_t (J - Target'First) + Item'First)));
 
    Terminator_Error : exception;
 
@@ -156,40 +358,118 @@ package Interfaces.C is
    char16_nul : constant char16_t := char16_t'Val (0);
    pragma Ada_05 (char16_nul);
 
-   function To_C (Item : Wide_Character) return char16_t;
+   --  To_C and To_Ada provide mappings between the Ada and C 16-bit character
+   --  types.
+
+   function To_C (Item : Wide_Character) return char16_t
+   with
+     Post => To_C'Result = char16_t (Item);
    pragma Ada_05 (To_C);
 
-   function To_Ada (Item : char16_t) return Wide_Character;
+   function To_Ada (Item : char16_t) return Wide_Character
+   with
+     Post => To_Ada'Result = Wide_Character (Item);
    pragma Ada_05 (To_Ada);
 
    type char16_array is array (size_t range <>) of aliased char16_t;
    pragma Ada_05 (char16_array);
 
-   function Is_Nul_Terminated (Item : char16_array) return Boolean;
+   function Is_Nul_Terminated (Item : char16_array) return Boolean
+   with
+     Post => Is_Nul_Terminated'Result = (for some C of Item => C = char16_nul);
    pragma Ada_05 (Is_Nul_Terminated);
+   --  The result of Is_Nul_Terminated is True if Item contains char16_nul, and
+   --  is False otherwise.
+
+   --  The To_C and To_Ada subprograms that convert between Wide_String and
+   --  char16_array have analogous effects to the To_C and To_Ada subprograms
+   --  that convert between String and char_array, except that char16_nul is
+   --  used instead of nul.
+
+   function C_Length_Ghost (Item : char16_array) return size_t
+   with
+     Ghost,
+     Pre  => Is_Nul_Terminated (Item),
+     Post => C_Length_Ghost'Result <= Item'Last - Item'First
+       and then Item (Item'First + C_Length_Ghost'Result) = char16_nul
+       and then (for all J in Item'First .. Item'First + C_Length_Ghost'Result
+                   when J /= Item'First + C_Length_Ghost'Result =>
+                     Item (J) /= char16_nul);
+   --  Ghost function to compute the length of a char16_array up to the first
+   --  char16_nul character.
 
    function To_C
      (Item       : Wide_String;
-      Append_Nul : Boolean := True) return char16_array;
+      Append_Nul : Boolean := True) return char16_array
+   with
+     Pre  => not (Append_Nul = False and then Item'Length = 0),
+     Post => To_C'Result'First = 0
+       and then To_C'Result'Length =
+         (if Append_Nul then Item'Length + 1 else Item'Length)
+       and then (for all J in Item'Range =>
+                   To_C'Result (size_t (J - Item'First)) = To_C (Item (J)))
+       and then
+         (if Append_Nul then To_C'Result (To_C'Result'Last) = char16_nul);
    pragma Ada_05 (To_C);
 
    function To_Ada
      (Item     : char16_array;
-      Trim_Nul : Boolean := True) return Wide_String;
+      Trim_Nul : Boolean := True) return Wide_String
+   with
+     Pre  => (if Trim_Nul then
+                Is_Nul_Terminated (Item)
+                  and then C_Length_Ghost (Item) <= size_t (Natural'Last)
+              else
+                Item'Last - Item'First < size_t (Natural'Last)),
+     Post => To_Ada'Result'First = 1
+       and then To_Ada'Result'Length =
+         (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
+       and then (for all J in To_Ada'Result'Range =>
+                   To_Ada'Result (J) =
+                     To_Ada (Item (size_t (J) - 1 + Item'First)));
    pragma Ada_05 (To_Ada);
 
    procedure To_C
      (Item       : Wide_String;
       Target     : out char16_array;
       Count      : out size_t;
-      Append_Nul : Boolean := True);
+      Append_Nul : Boolean := True)
+   with
+     Relaxed_Initialization => Target,
+     Pre  => Target'Length >=
+       (if Append_Nul then Item'Length + 1 else Item'Length),
+     Post => Count = (if Append_Nul then Item'Length + 1 else Item'Length)
+       and then
+         (if Count /= 0 then
+           Target (Target'First .. Target'First + (Count - 1))'Initialized)
+       and then
+         (for all J in Item'Range =>
+           Target (Target'First + size_t (J - Item'First)) = To_C (Item (J)))
+       and then
+         (if Append_Nul then Target (Target'First + (Count - 1)) = char16_nul);
    pragma Ada_05 (To_C);
 
    procedure To_Ada
      (Item     : char16_array;
       Target   : out Wide_String;
       Count    : out Natural;
-      Trim_Nul : Boolean := True);
+      Trim_Nul : Boolean := True)
+   with
+     Relaxed_Initialization => Target,
+     Pre  => (if Trim_Nul then
+                Is_Nul_Terminated (Item)
+                  and then C_Length_Ghost (Item) <= size_t (Target'Length)
+              else
+                Item'Last - Item'First < size_t (Target'Length)),
+     Post => Count =
+         (if Trim_Nul then Natural (C_Length_Ghost (Item)) else Item'Length)
+       and then
+         (if Count /= 0 then
+           Target (Target'First .. Target'First + (Count - 1))'Initialized)
+       and then
+         (for all J in Target'First .. Target'First + (Count - 1) =>
+           Target (J) =
+             To_Ada (Item (size_t (J - Target'First) + Item'First)));
    pragma Ada_05 (To_Ada);
 
    type char32_t is new Wide_Wide_Character;
@@ -198,40 +478,118 @@ package Interfaces.C is
    char32_nul : constant char32_t := char32_t'Val (0);
    pragma Ada_05 (char32_nul);
 
-   function To_C (Item : Wide_Wide_Character) return char32_t;
+   --  To_C and To_Ada provide mappings between the Ada and C 32-bit character
+   --  types.
+
+   function To_C (Item : Wide_Wide_Character) return char32_t
+   with
+     Post => To_C'Result = char32_t (Item);
    pragma Ada_05 (To_C);
 
-   function To_Ada (Item : char32_t) return Wide_Wide_Character;
+   function To_Ada (Item : char32_t) return Wide_Wide_Character
+   with
+     Post => To_Ada'Result = Wide_Wide_Character (Item);
    pragma Ada_05 (To_Ada);
 
    type char32_array is array (size_t range <>) of aliased char32_t;
    pragma Ada_05 (char32_array);
 
-   function Is_Nul_Terminated (Item : char32_array) return Boolean;
+   function Is_Nul_Terminated (Item : char32_array) return Boolean
+   with
+     Post => Is_Nul_Terminated'Result = (for some C of Item => C = char32_nul);
    pragma Ada_05 (Is_Nul_Terminated);
+   --  The result of Is_Nul_Terminated is True if Item contains char32_nul, and
+   --  is False otherwise.
+
+   function C_Length_Ghost (Item : char32_array) return size_t
+   with
+     Ghost,
+     Pre  => Is_Nul_Terminated (Item),
+     Post => C_Length_Ghost'Result <= Item'Last - Item'First
+       and then Item (Item'First + C_Length_Ghost'Result) = char32_nul
+       and then (for all J in Item'First .. Item'First + C_Length_Ghost'Result
+                   when J /= Item'First + C_Length_Ghost'Result =>
+                     Item (J) /= char32_nul);
+   --  Ghost function to compute the length of a char32_array up to the first
+   --  char32_nul character.
+
+   --  The To_C and To_Ada subprograms that convert between Wide_Wide_String
+   --  and char32_array have analogous effects to the To_C and To_Ada
+   --  subprograms that convert between String and char_array, except
+   --  that char32_nul is used instead of nul.
 
    function To_C
      (Item       : Wide_Wide_String;
-      Append_Nul : Boolean := True) return char32_array;
+      Append_Nul : Boolean := True) return char32_array
+   with
+     Pre  => not (Append_Nul = False and then Item'Length = 0),
+     Post => To_C'Result'First = 0
+       and then To_C'Result'Length =
+         (if Append_Nul then Item'Length + 1 else Item'Length)
+       and then (for all J in Item'Range =>
+                   To_C'Result (size_t (J - Item'First)) = To_C (Item (J)))
+       and then
+         (if Append_Nul then To_C'Result (To_C'Result'Last) = char32_nul);
    pragma Ada_05 (To_C);
 
    function To_Ada
      (Item     : char32_array;
-      Trim_Nul : Boolean := True) return Wide_Wide_String;
+      Trim_Nul : Boolean := True) return Wide_Wide_String
+   with
+     Pre  => (if Trim_Nul then
+                Is_Nul_Terminated (Item)
+                  and then C_Length_Ghost (Item) <= size_t (Natural'Last)
+              else
+                Item'Last - Item'First < size_t (Natural'Last)),
+     Post => To_Ada'Result'First = 1
+       and then To_Ada'Result'Length =
+         (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
+       and then (for all J in To_Ada'Result'Range =>
+                   To_Ada'Result (J) =
+                     To_Ada (Item (size_t (J) - 1 + Item'First)));
    pragma Ada_05 (To_Ada);
 
    procedure To_C
      (Item       : Wide_Wide_String;
       Target     : out char32_array;
       Count      : out size_t;
-      Append_Nul : Boolean := True);
+      Append_Nul : Boolean := True)
+   with
+     Relaxed_Initialization => Target,
+     Pre  => Target'Length >=
+       (if Append_Nul then Item'Length + 1 else Item'Length),
+     Post => Count = (if Append_Nul then Item'Length + 1 else Item'Length)
+       and then
+         (if Count /= 0 then
+           Target (Target'First .. Target'First + (Count - 1))'Initialized)
+       and then
+         (for all J in Item'Range =>
+           Target (Target'First + size_t (J - Item'First)) = To_C (Item (J)))
+       and then
+         (if Append_Nul then Target (Target'First + (Count - 1)) = char32_nul);
    pragma Ada_05 (To_C);
 
    procedure To_Ada
      (Item     : char32_array;
       Target   : out Wide_Wide_String;
       Count    : out Natural;
-      Trim_Nul : Boolean := True);
+      Trim_Nul : Boolean := True)
+   with
+     Relaxed_Initialization => Target,
+     Pre  => (if Trim_Nul then
+                Is_Nul_Terminated (Item)
+                  and then C_Length_Ghost (Item) <= size_t (Target'Length)
+              else
+                Item'Last - Item'First < size_t (Target'Length)),
+     Post => Count =
+         (if Trim_Nul then Natural (C_Length_Ghost (Item)) else Item'Length)
+       and then
+         (if Count /= 0 then
+           Target (Target'First .. Target'First + (Count - 1))'Initialized)
+       and then
+         (for all J in Target'First .. Target'First + (Count - 1) =>
+           Target (J) =
+             To_Ada (Item (size_t (J - Target'First) + Item'First)));
    pragma Ada_05 (To_Ada);
 
 end Interfaces.C;
diff --git a/gcc/ada/libgnat/s-os_lib.adb b/gcc/ada/libgnat/s-os_lib.adb
index 19f4cf7..7df06c4 100644
--- a/gcc/ada/libgnat/s-os_lib.adb
+++ b/gcc/ada/libgnat/s-os_lib.adb
@@ -29,8 +29,6 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-pragma Compiler_Unit_Warning;
-
 with Ada.Unchecked_Conversion;
 with Ada.Unchecked_Deallocation;
 with System; use System;