[Ada] Proof of System.Generic_Array_Operations at silver level

gcc/ada/

	* libgnat/a-ngcoar.adb: Add pragma to ignore assertions in
	instance.
	* libgnat/a-ngrear.adb: Likewise.
	* libgnat/s-gearop.adb: Prove implementation is free of runtime
	errors.
	* libgnat/s-gearop.ads: Add contracts to protect against runtime
	errors in the generic part.

4 files changed, 490 insertions, 51 deletions

diff --git a/gcc/ada/libgnat/a-ngcoar.adb b/gcc/ada/libgnat/a-ngcoar.adb
index ed9be6a..953cb09 100644
--- a/gcc/ada/libgnat/a-ngcoar.adb
+++ b/gcc/ada/libgnat/a-ngcoar.adb
@@ -29,6 +29,17 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+--  Preconditions, postconditions, 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 (Pre            => Ignore,
+                         Post           => Ignore,
+                         Ghost          => Ignore,
+                         Loop_Invariant => Ignore,
+                         Assert         => Ignore);
+
 with System.Generic_Array_Operations; use System.Generic_Array_Operations;
 
 package body Ada.Numerics.Generic_Complex_Arrays is
diff --git a/gcc/ada/libgnat/a-ngrear.adb b/gcc/ada/libgnat/a-ngrear.adb
index 5095db8..c34cdd6 100644
--- a/gcc/ada/libgnat/a-ngrear.adb
+++ b/gcc/ada/libgnat/a-ngrear.adb
@@ -36,6 +36,17 @@
 --  BLAS/LAPACK implementation. Finally, on some platforms there are more
 --  floating point types than supported by BLAS/LAPACK.
 
+--  Preconditions, postconditions, 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 (Pre            => Ignore,
+                         Post           => Ignore,
+                         Ghost          => Ignore,
+                         Loop_Invariant => Ignore,
+                         Assert         => Ignore);
+
 with Ada.Containers.Generic_Anonymous_Array_Sort; use Ada.Containers;
 
 with System; use System;
diff --git a/gcc/ada/libgnat/s-gearop.adb b/gcc/ada/libgnat/s-gearop.adb
index 92af09d..e86d982 100644
--- a/gcc/ada/libgnat/s-gearop.adb
+++ b/gcc/ada/libgnat/s-gearop.adb
@@ -29,18 +29,44 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+--  Preconditions, postconditions, 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 (Pre            => Ignore,
+                         Post           => Ignore,
+                         Ghost          => Ignore,
+                         Loop_Invariant => Ignore,
+                         Assert         => Ignore);
+
 with Ada.Numerics; use Ada.Numerics;
-package body System.Generic_Array_Operations is
+
+package body System.Generic_Array_Operations
+  with SPARK_Mode
+is
+   pragma Warnings
+     (Off, "aspect * not enforced on inlined subprogram",
+      Reason => "Contracts in this unit are never executed");
+
    function Check_Unit_Last
      (Index : Integer;
       Order : Positive;
-      First : Integer) return Integer;
+      First : Integer) return Integer
+   with
+     Pre => Index >= First
+       and then First <= Integer'Last - Order + 1
+       and then Index <= First + (Order - 1),
+     Post => Check_Unit_Last'Result = First + (Order - 1);
+
    pragma Inline_Always (Check_Unit_Last);
    --  Compute index of last element returned by Unit_Vector or Unit_Matrix.
    --  A separate function is needed to allow raising Constraint_Error before
    --  declaring the function result variable. The result variable needs to be
    --  declared first, to allow front-end inlining.
 
+   pragma Warnings (On, "aspect * not enforced on inlined subprogram");
+
    --------------
    -- Diagonal --
    --------------
@@ -48,9 +74,14 @@ package body System.Generic_Array_Operations is
    function Diagonal (A : Matrix) return Vector is
       N : constant Natural := Natural'Min (A'Length (1), A'Length (2));
    begin
-      return R : Vector (A'First (1) .. A'First (1) + N - 1) do
+      return R : Vector (A'First (1) .. A'First (1) + (N - 1))
+        with Relaxed_Initialization
+      do
          for J in 0 .. N - 1 loop
             R (R'First + J) := A (A'First (1) + J, A'First (2) + J);
+
+            pragma Loop_Invariant
+              (for all JJ in R'First .. R'First + J => R (JJ)'Initialized);
          end loop;
       end return;
    end Diagonal;
@@ -103,7 +134,10 @@ package body System.Generic_Array_Operations is
         (M      : in out Matrix;
          Target : Integer;
          Source : Integer;
-         Factor : Scalar);
+         Factor : Scalar)
+      with
+        Pre => Target in M'Range (1)
+          and then Source in M'Range (1);
       --  Elementary row operation that subtracts Factor * M (Source, <>) from
       --  M (Target, <>)
 
@@ -131,6 +165,9 @@ package body System.Generic_Array_Operations is
 
    begin
       Do_Rows : for Row in reverse M'Range (1) loop
+
+         pragma Loop_Invariant (Max_Col <= M'Last (2));
+
          Find_Non_Zero : for Col in reverse M'First (2) .. Max_Col loop
             if Is_Non_Zero (M (Row, Col)) then
 
@@ -144,12 +181,15 @@ package body System.Generic_Array_Operations is
                   --  equals Integer'First, which is true for aggregates
                   --  without explicit bounds..
 
-                  J : Integer := M'First (1);
+                  J  : Integer := M'First (1);
+                  NZ : constant Scalar := M (Row, Col);
 
                begin
                   while J < Row loop
-                     Sub_Row (N, J, Row, (M (J, Col) / M (Row, Col)));
-                     Sub_Row (M, J, Row, (M (J, Col) / M (Row, Col)));
+                     pragma Loop_Invariant (J in M'Range (1));
+
+                     Sub_Row (N, J, Row, (M (J, Col) / NZ));
+                     Sub_Row (M, J, Row, (M (J, Col) / NZ));
                      J := J + 1;
                   end loop;
                end;
@@ -189,19 +229,38 @@ package body System.Generic_Array_Operations is
         (M      : in out Matrix;
          Target : Integer;
          Source : Integer;
-         Factor : Scalar);
+         Factor : Scalar)
+      with
+        Pre => Target in M'Range (1)
+          and then Source in M'Range (1);
       --  Subtrace Factor * M (Source, <>) from M (Target, <>)
 
       procedure Divide_Row
         (M, N  : in out Matrix;
          Row   : Integer;
-         Scale : Scalar);
+         Scale : Scalar)
+      with
+        Pre => Row in M'Range (1)
+          and then M'First (1) = N'First (1)
+          and then M'Last (1) = N'Last (1)
+          and then Scale /= Zero;
       --  Divide M (Row) and N (Row) by Scale, and update Det
 
       procedure Switch_Row
         (M, N  : in out Matrix;
          Row_1 : Integer;
-         Row_2 : Integer);
+         Row_2 : Integer)
+      with
+        Pre  => Row_1 in M'Range (1)
+          and then Row_2 in M'Range (1)
+          and then M'First (1) = N'First (1)
+          and then M'Last (1) = N'Last (1),
+        Post => (for all J in M'Range (2) =>
+                   M (Row_1, J) = M'Old (Row_2, J)
+                     and then M (Row_2, J) = M'Old (Row_1, J))
+          and then (for all J in N'Range (2) =>
+                      N (Row_1, J) = N'Old (Row_2, J)
+                        and then N (Row_2, J) = N'Old (Row_1, J));
       --  Exchange M (Row_1) and N (Row_1) with M (Row_2) and N (Row_2),
       --  negating Det in the process.
 
@@ -238,8 +297,7 @@ package body System.Generic_Array_Operations is
          end loop;
 
          for J in N'Range (2) loop
-            N (Row - M'First (1) + N'First (1), J) :=
-              N (Row - M'First (1) + N'First (1), J) / Scale;
+            N (Row, J) := N (Row, J) / Scale;
             pragma Annotate
               (CodePeer, False_Positive, "divide by zero", "Scale /= 0");
          end loop;
@@ -254,7 +312,9 @@ package body System.Generic_Array_Operations is
          Row_1 : Integer;
          Row_2 : Integer)
       is
-         procedure Swap (X, Y : in out Scalar);
+         procedure Swap (X, Y : in out Scalar)
+         with
+           Post => X = Y'Old and then Y = X'Old;
          --  Exchange the values of X and Y
 
          ----------
@@ -276,11 +336,28 @@ package body System.Generic_Array_Operations is
 
             for J in M'Range (2) loop
                Swap (M (Row_1, J), M (Row_2, J));
+               pragma Annotate
+                 (GNATprove, False_Positive,
+                  "formal parameters ""X"" and ""Y"" might be aliased",
+                  "Row_1 /= Row_2");
+
+               pragma Loop_Invariant
+                 (for all JJ in M'First (2) .. J =>
+                    M (Row_1, JJ) = M'Loop_Entry (Row_2, JJ)
+                      and then M (Row_2, JJ) = M'Loop_Entry (Row_1, JJ));
             end loop;
 
             for J in N'Range (2) loop
-               Swap (N (Row_1 - M'First (1) + N'First (1), J),
-                     N (Row_2 - M'First (1) + N'First (1), J));
+               Swap (N (Row_1, J), N (Row_2, J));
+               pragma Annotate
+                 (GNATprove, False_Positive,
+                  "formal parameters ""X"" and ""Y"" might be aliased",
+                  "Row_1 /= Row_2");
+
+               pragma Loop_Invariant
+                 (for all JJ in N'First (2) .. J =>
+                    N (Row_1, JJ) = N'Loop_Entry (Row_2, JJ)
+                      and then N (Row_2, JJ) = N'Loop_Entry (Row_1, JJ));
             end loop;
          end if;
       end Switch_Row;
@@ -295,6 +372,8 @@ package body System.Generic_Array_Operations is
       Det := One;
 
       for J in M'Range (2) loop
+         pragma Loop_Invariant (Row >= M'First (1));
+
          declare
             Max_Row : Integer := Row;
             Max_Abs : Real'Base := 0.0;
@@ -303,6 +382,10 @@ package body System.Generic_Array_Operations is
             --  Find best pivot in column J, starting in row Row
 
             for K in Row .. M'Last (1) loop
+               pragma Loop_Invariant (Max_Row in M'Range (1));
+               pragma Loop_Invariant
+                 (if Max_Abs /= 0.0 then Max_Abs = abs M (Max_Row, J));
+
                declare
                   New_Abs : constant Real'Base := abs M (K, J);
                begin
@@ -316,6 +399,8 @@ package body System.Generic_Array_Operations is
             if Max_Abs > 0.0 then
                Switch_Row (M, N, Row, Max_Row);
 
+               pragma Assert (Max_Abs = abs M (Row, J));
+
                --  The temporaries below are necessary to force a copy of the
                --  value and avoid improper aliasing.
 
@@ -325,7 +410,7 @@ package body System.Generic_Array_Operations is
                   Divide_Row (M, N, Row, Scale);
                end;
 
-               for U in Row + 1 .. M'Last (1) loop
+               for U in Row .. M'Last (1) when U /= Row loop
                   declare
                      Factor : constant Scalar := M (U, J);
                   begin
@@ -379,7 +464,11 @@ package body System.Generic_Array_Operations is
 
    begin
       for J in X'Range loop
+         pragma Loop_Invariant (Sum >= 0.0);
          Sum := Sum + Result_Real'Base (abs X (J))**2;
+         pragma Annotate
+           (GNATprove, Intentional, "float overflow check might fail",
+            "Intermediate computation might overflow in L2_Norm");
       end loop;
 
       return Sqrt (Sum);
@@ -391,11 +480,25 @@ package body System.Generic_Array_Operations is
 
    function Matrix_Elementwise_Operation (X : X_Matrix) return Result_Matrix is
    begin
-      return R : Result_Matrix (X'Range (1), X'Range (2)) do
+      return R : Result_Matrix (X'Range (1), X'Range (2))
+        with Relaxed_Initialization
+      do
          for J in R'Range (1) loop
             for K in R'Range (2) loop
                R (J, K) := Operation (X (J, K));
+
+               pragma Loop_Invariant
+                 (for all JJ in R'First (1) .. J when JJ /= J =>
+                    (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+               pragma Loop_Invariant
+                 (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
             end loop;
+
+            pragma Loop_Invariant
+              (for all JJ in R'First (1) .. J when JJ /= J =>
+                 (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+            pragma Loop_Invariant
+              (for all KK in R'Range (2) => R (J, KK)'Initialized);
          end loop;
       end return;
    end Matrix_Elementwise_Operation;
@@ -422,7 +525,9 @@ package body System.Generic_Array_Operations is
       Right : Right_Matrix) return Result_Matrix
    is
    begin
-      return R : Result_Matrix (Left'Range (1), Left'Range (2)) do
+      return R : Result_Matrix (Left'Range (1), Left'Range (2))
+        with Relaxed_Initialization
+      do
          if Left'Length (1) /= Right'Length (1)
               or else
             Left'Length (2) /= Right'Length (2)
@@ -439,7 +544,19 @@ package body System.Generic_Array_Operations is
                     Right
                       (J - R'First (1) + Right'First (1),
                        K - R'First (2) + Right'First (2)));
+
+               pragma Loop_Invariant
+                 (for all JJ in R'First (1) .. J when JJ /= J =>
+                    (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+               pragma Loop_Invariant
+                 (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
             end loop;
+
+            pragma Loop_Invariant
+              (for all JJ in R'First (1) .. J when JJ /= J =>
+                 (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+            pragma Loop_Invariant
+              (for all KK in R'Range (2) => R (J, KK)'Initialized);
          end loop;
       end return;
    end Matrix_Matrix_Elementwise_Operation;
@@ -454,7 +571,9 @@ package body System.Generic_Array_Operations is
       Z : Z_Scalar) return Result_Matrix
    is
    begin
-      return R : Result_Matrix (X'Range (1), X'Range (2)) do
+      return R : Result_Matrix (X'Range (1), X'Range (2))
+        with Relaxed_Initialization
+      do
          if X'Length (1) /= Y'Length (1)
               or else
             X'Length (2) /= Y'Length (2)
@@ -471,7 +590,19 @@ package body System.Generic_Array_Operations is
                     Y (J - R'First (1) + Y'First (1),
                        K - R'First (2) + Y'First (2)),
                     Z);
+
+               pragma Loop_Invariant
+                 (for all JJ in R'First (1) .. J when JJ /= J =>
+                    (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+               pragma Loop_Invariant
+                 (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
             end loop;
+
+            pragma Loop_Invariant
+              (for all JJ in R'First (1) .. J when JJ /= J =>
+                 (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+            pragma Loop_Invariant
+              (for all KK in R'Range (2) => R (J, KK)'Initialized);
          end loop;
       end return;
    end Matrix_Matrix_Scalar_Elementwise_Operation;
@@ -527,11 +658,25 @@ package body System.Generic_Array_Operations is
       Right : Right_Scalar) return Result_Matrix
    is
    begin
-      return R : Result_Matrix (Left'Range (1), Left'Range (2)) do
+      return R : Result_Matrix (Left'Range (1), Left'Range (2))
+        with Relaxed_Initialization
+      do
          for J in R'Range (1) loop
             for K in R'Range (2) loop
                R (J, K) := Operation (Left (J, K), Right);
+
+               pragma Loop_Invariant
+                 (for all JJ in R'First (1) .. J when JJ /= J =>
+                    (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+               pragma Loop_Invariant
+                 (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
             end loop;
+
+            pragma Loop_Invariant
+              (for all JJ in R'First (1) .. J when JJ /= J =>
+                 (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+            pragma Loop_Invariant
+              (for all KK in R'Range (2) => R (J, KK)'Initialized);
          end loop;
       end return;
    end Matrix_Scalar_Elementwise_Operation;
@@ -561,11 +706,25 @@ package body System.Generic_Array_Operations is
       Right : Right_Matrix) return Result_Matrix
    is
    begin
-      return R : Result_Matrix (Right'Range (1), Right'Range (2)) do
+      return R : Result_Matrix (Right'Range (1), Right'Range (2))
+        with Relaxed_Initialization
+      do
          for J in R'Range (1) loop
             for K in R'Range (2) loop
                R (J, K) := Operation (Left, Right (J, K));
+
+               pragma Loop_Invariant
+                 (for all JJ in R'First (1) .. J when JJ /= J =>
+                    (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+               pragma Loop_Invariant
+                 (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
             end loop;
+
+            pragma Loop_Invariant
+              (for all JJ in R'First (1) .. J when JJ /= J =>
+                 (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+            pragma Loop_Invariant
+              (for all KK in R'Range (2) => R (J, KK)'Initialized);
          end loop;
       end return;
    end Scalar_Matrix_Elementwise_Operation;
@@ -590,7 +749,9 @@ package body System.Generic_Array_Operations is
    -- Sqrt --
    ----------
 
-   function Sqrt (X : Real'Base) return Real'Base is
+   function Sqrt (X : Real'Base) return Real'Base
+     with SPARK_Mode => Off  --  Not in SPARK due to use of Real'Exponent
+   is
       Root, Next : Real'Base;
 
    begin
@@ -651,7 +812,9 @@ package body System.Generic_Array_Operations is
       Right : Right_Matrix) return Result_Matrix
    is
    begin
-      return R : Result_Matrix (Left'Range (1), Right'Range (2)) do
+      return R : Result_Matrix (Left'Range (1), Right'Range (2))
+        with Relaxed_Initialization
+      do
          if Left'Length (2) /= Right'Length (1) then
             raise Constraint_Error with
               "incompatible dimensions in matrix multiplication";
@@ -671,7 +834,19 @@ package body System.Generic_Array_Operations is
 
                   R (J, K) := S;
                end;
+
+               pragma Loop_Invariant
+                 (for all JJ in R'First (1) .. J when JJ /= J =>
+                    (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+               pragma Loop_Invariant
+                 (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
             end loop;
+
+            pragma Loop_Invariant
+              (for all JJ in R'First (1) .. J when JJ /= J =>
+                 (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+            pragma Loop_Invariant
+              (for all KK in R'Range (2) => R (J, KK)'Initialized);
          end loop;
       end return;
    end  Matrix_Matrix_Product;
@@ -681,10 +856,21 @@ package body System.Generic_Array_Operations is
    ----------------------------
 
    function Matrix_Vector_Solution (A : Matrix; X : Vector) return Vector is
+
+      procedure Ignore (M : Matrix)
+      with
+        Ghost,
+        Depends => (null => M);
+
+      procedure Ignore (M : Matrix) is null;
+      --  Ghost procedure to document that the value of argument M is ignored,
+      --  which prevents a warning being issued about the value not being used
+      --  in the rest of the code.
+
       N   : constant Natural := A'Length (1);
       MA  : Matrix := A;
-      MX  : Matrix (A'Range (1), 1 .. 1);
-      R   : Vector (A'Range (2));
+      MX  : Matrix (A'Range (1), 1 .. 1) with Relaxed_Initialization;
+      R   : Vector (A'Range (2)) with Relaxed_Initialization;
       Det : Scalar;
 
    begin
@@ -698,18 +884,29 @@ package body System.Generic_Array_Operations is
 
       for J in 0 .. MX'Length (1) - 1 loop
          MX (MX'First (1) + J, 1) := X (X'First + J);
+
+         pragma Loop_Invariant
+           (for all JJ in MX'First (1) .. MX'First (1) + J =>
+              MX (JJ, 1)'Initialized);
       end loop;
 
       Forward_Eliminate (MA, MX, Det);
 
       if Det = Zero then
          raise Constraint_Error with "matrix is singular";
+         pragma Annotate
+           (GNATprove, Intentional, "exception might be raised",
+            "An exception should be raised on a singular matrix");
       end if;
 
       Back_Substitute (MA, MX);
+      Ignore (MA);
 
       for J in 0 .. R'Length - 1 loop
          R (R'First + J) := MX (MX'First (1) + J, 1);
+
+         pragma Loop_Invariant
+           (for all JJ in R'First .. R'First + J => R (JJ)'Initialized);
       end loop;
 
       return R;
@@ -720,9 +917,20 @@ package body System.Generic_Array_Operations is
    ----------------------------
 
    function Matrix_Matrix_Solution (A, X : Matrix) return Matrix is
+
+      procedure Ignore (M : Matrix)
+      with
+        Ghost,
+        Depends => (null => M);
+
+      procedure Ignore (M : Matrix) is null;
+      --  Ghost procedure to document that the value of argument M is ignored,
+      --  which prevents a warning being issued about the value not being used
+      --  in the rest of the code.
+
       N   : constant Natural := A'Length (1);
-      MA  : Matrix (A'Range (2), A'Range (2));
-      MB  : Matrix (A'Range (2), X'Range (2));
+      MA  : Matrix (A'Range (2), A'Range (2)) with Relaxed_Initialization;
+      MB  : Matrix (A'Range (2), X'Range (2)) with Relaxed_Initialization;
       Det : Scalar;
 
    begin
@@ -737,20 +945,53 @@ package body System.Generic_Array_Operations is
       for J in 0 .. A'Length (1) - 1 loop
          for K in MA'Range (2) loop
             MA (MA'First (1) + J, K) := A (A'First (1) + J, K);
+
+            pragma Loop_Invariant
+              (for all JJ in MA'First (1) .. MA'First (1) + J
+                 when JJ /= MA'First (1) + J
+               =>
+                 (for all KK in MA'Range (2) =>
+                    MA (JJ, KK)'Initialized));
+            pragma Loop_Invariant
+              (for all KK in MA'First (2) .. K =>
+                 MA (MA'First (1) + J, KK)'Initialized);
          end loop;
 
          for K in MB'Range (2) loop
             MB (MB'First (1) + J, K) := X (X'First (1) + J, K);
+
+            pragma Loop_Invariant
+              (for all JJ in MB'First (1) .. MB'First (1) + J
+                 when JJ /= MB'First (1) + J
+               =>
+                 (for all KK in MB'Range (2) =>
+                    MB (JJ, KK)'Initialized));
+            pragma Loop_Invariant
+              (for all KK in MB'First (2) .. K =>
+                 MB (MB'First (1) + J, KK)'Initialized);
          end loop;
+
+         pragma Loop_Invariant
+           (for all JJ in MA'First (1) .. MA'First (1) + J =>
+              (for all KK in MA'Range (2) =>
+                 MA (JJ, KK)'Initialized));
+         pragma Loop_Invariant
+           (for all JJ in MB'First (1) .. MB'First (1) + J =>
+              (for all KK in MB'Range (2) =>
+                 MB (JJ, KK)'Initialized));
       end loop;
 
       Forward_Eliminate (MA, MB, Det);
 
       if Det = Zero then
          raise Constraint_Error with "matrix is singular";
+         pragma Annotate
+           (GNATprove, Intentional, "exception might be raised",
+            "An exception should be raised on a singular matrix");
       end if;
 
       Back_Substitute (MA, MB);
+      Ignore (MA);
 
       return MB;
    end Matrix_Matrix_Solution;
@@ -795,11 +1036,25 @@ package body System.Generic_Array_Operations is
       Right : Right_Vector) return Matrix
    is
    begin
-      return R : Matrix (Left'Range, Right'Range) do
+      return R : Matrix (Left'Range, Right'Range)
+        with Relaxed_Initialization
+      do
          for J in R'Range (1) loop
             for K in R'Range (2) loop
                R (J, K) := Left (J) * Right (K);
+
+               pragma Loop_Invariant
+                 (for all JJ in R'First (1) .. J when JJ /= J =>
+                    (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+               pragma Loop_Invariant
+                 (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
             end loop;
+
+            pragma Loop_Invariant
+              (for all JJ in R'First (1) .. J when JJ /= J =>
+                 (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+            pragma Loop_Invariant
+              (for all KK in R'Range (2) => R (J, KK)'Initialized);
          end loop;
       end return;
    end Outer_Product;
@@ -828,7 +1083,17 @@ package body System.Generic_Array_Operations is
          for K in R'Range (2) loop
             R (J, K) := A (K - R'First (2) + A'First (1),
                            J - R'First (1) + A'First (2));
+
+            pragma Loop_Invariant
+              (for all JJ in R'First (1) .. J when JJ /= J =>
+                (for all K in R'Range (2) => R (JJ, K)'Initialized));
+            pragma Loop_Invariant
+              (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
          end loop;
+
+         pragma Loop_Invariant
+           (for all JJ in R'First (1) .. J =>
+             (for all K in R'Range (2) => R (JJ, K)'Initialized));
       end loop;
    end Transpose;
 
diff --git a/gcc/ada/libgnat/s-gearop.ads b/gcc/ada/libgnat/s-gearop.ads
index 340cf96..a3c0239 100644
--- a/gcc/ada/libgnat/s-gearop.ads
+++ b/gcc/ada/libgnat/s-gearop.ads
@@ -29,8 +29,29 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-package System.Generic_Array_Operations is
-pragma Pure (Generic_Array_Operations);
+--  Proof of this unit is only done up to silver level, i.e. absence of runtime
+--  errors, and only regarding runtime checks that depend on the generic part,
+--  ignoring runtime checks related to formal generic subprogram parameters
+--  in instantiations. For example, contracts do not protect against scalar
+--  overflows in arithmetic operations passed on as formal generic subprogram
+--  parameters.
+
+--  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);
+
+package System.Generic_Array_Operations
+  with SPARK_Mode
+is
+
+   pragma Pure (Generic_Array_Operations);
 
    ---------------------
    -- Back_Substitute --
@@ -43,7 +64,10 @@ pragma Pure (Generic_Array_Operations);
       with function "*" (Left, Right : Scalar) return Scalar is <>;
       with function "/" (Left, Right : Scalar) return Scalar is <>;
       with function Is_Non_Zero (X : Scalar) return Boolean is <>;
-   procedure Back_Substitute (M, N : in out Matrix);
+   procedure Back_Substitute (M, N : in out Matrix)
+   with
+     Pre => M'First (1) = N'First (1)
+       and then M'Last (1) = N'Last (1);
 
    --------------
    -- Diagonal --
@@ -53,7 +77,14 @@ pragma Pure (Generic_Array_Operations);
       type Scalar is private;
       type Vector is array (Integer range <>) of Scalar;
       type Matrix is array (Integer range <>, Integer range <>) of Scalar;
-   function Diagonal (A : Matrix) return Vector;
+   function Diagonal (A : Matrix) return Vector
+   with
+     Pre => A'First (1) < A'Last (1)
+       and then A'First (2) < A'Last (2)
+       and then (if A'First (1) <= 0 then
+                   A'Last (1) < Integer'Last + A'First (1))
+       and then (if A'First (2) <= 0 then
+                   A'Last (2) < Integer'Last + A'First (2));
 
    -----------------------
    -- Forward_Eliminate --
@@ -76,7 +107,10 @@ pragma Pure (Generic_Array_Operations);
    procedure Forward_Eliminate
      (M   : in out Matrix;
       N   : in out Matrix;
-      Det : out Scalar);
+      Det : out Scalar)
+   with
+     Pre => M'First (1) = N'First (1)
+       and then M'Last (1) = N'Last (1);
 
    --------------------------
    -- Square_Matrix_Length --
@@ -85,8 +119,14 @@ pragma Pure (Generic_Array_Operations);
    generic
       type Scalar is private;
       type Matrix is array (Integer range <>, Integer range <>) of Scalar;
-   function Square_Matrix_Length (A : Matrix) return Natural;
-   --  If A is non-square, raise Constraint_Error,  else return its dimension
+   function Square_Matrix_Length (A : Matrix) return Natural
+   with
+     Pre => (if A'First (1) <= 0 then
+               A'Last (1) < Integer'Last + A'First (1))
+       and then (if A'First (2) <= 0 then
+                   A'Last (2) < Integer'Last + A'First (2))
+       and then A'Length (1) = A'Length (2);
+   --  If A is non-square, raise Constraint_Error, else return its dimension
 
    ----------------------------------
    -- Vector_Elementwise_Operation --
@@ -129,7 +169,13 @@ pragma Pure (Generic_Array_Operations);
               Right : Right_Scalar) return Result_Scalar;
    function Vector_Vector_Elementwise_Operation
      (Left  : Left_Vector;
-      Right : Right_Vector) return Result_Vector;
+      Right : Right_Vector) return Result_Vector
+   with
+     Pre => (if Left'First <= 0 then
+               Left'Last < Integer'Last + Left'First)
+       and then (if Right'First <= 0 then
+                   Right'Last < Integer'Last + Right'First)
+       and then Left'Length = Right'Length;
 
    ------------------------------------------------
    -- Vector_Vector_Scalar_Elementwise_Operation --
@@ -150,7 +196,11 @@ pragma Pure (Generic_Array_Operations);
    function Vector_Vector_Scalar_Elementwise_Operation
      (X : X_Vector;
       Y : Y_Vector;
-      Z : Z_Scalar) return Result_Vector;
+      Z : Z_Scalar) return Result_Vector
+   with
+     Pre => (if X'First <= 0 then X'Last < Integer'Last + X'First)
+       and then (if Y'First <= 0 then Y'Last < Integer'Last + Y'First)
+       and then X'Length = Y'Length;
 
    -----------------------------------------
    -- Matrix_Matrix_Elementwise_Operation --
@@ -171,7 +221,18 @@ pragma Pure (Generic_Array_Operations);
               Right : Right_Scalar) return Result_Scalar;
    function Matrix_Matrix_Elementwise_Operation
      (Left  : Left_Matrix;
-      Right : Right_Matrix) return Result_Matrix;
+      Right : Right_Matrix) return Result_Matrix
+   with
+     Pre => (if Left'First (1) <= 0 then
+               Left'Last (1) < Integer'Last + Left'First (1))
+       and then (if Right'First (1) <= 0 then
+                   Right'Last (1) < Integer'Last + Right'First (1))
+       and then Left'Length (1) = Right'Length (1)
+       and then (if Left'First (2) <= 0 then
+                   Left'Last (2) < Integer'Last + Left'First (2))
+       and then (if Right'First (2) <= 0 then
+                   Right'Last (2) < Integer'Last + Right'First (2))
+       and then Left'Length (2) = Right'Length (2);
 
    ------------------------------------------------
    -- Matrix_Matrix_Scalar_Elementwise_Operation --
@@ -193,7 +254,18 @@ pragma Pure (Generic_Array_Operations);
    function Matrix_Matrix_Scalar_Elementwise_Operation
      (X : X_Matrix;
       Y : Y_Matrix;
-      Z : Z_Scalar) return Result_Matrix;
+      Z : Z_Scalar) return Result_Matrix
+   with
+     Pre => (if X'First (1) <= 0 then
+               X'Last (1) < Integer'Last + X'First (1))
+       and then (if Y'First (1) <= 0 then
+                   Y'Last (1) < Integer'Last + Y'First (1))
+       and then X'Length (1) = Y'Length (1)
+       and then (if X'First (2) <= 0 then
+                   X'Last (2) < Integer'Last + X'First (2))
+       and then (if Y'First (2) <= 0 then
+                   Y'Last (2) < Integer'Last + Y'First (2))
+       and then X'Length (2) = Y'Length (2);
 
    -----------------------------------------
    -- Vector_Scalar_Elementwise_Operation --
@@ -286,7 +358,13 @@ pragma Pure (Generic_Array_Operations);
               Right : Result_Scalar) return Result_Scalar is <>;
    function Inner_Product
      (Left  : Left_Vector;
-      Right : Right_Vector) return Result_Scalar;
+      Right : Right_Vector) return Result_Scalar
+   with
+     Pre => (if Left'First <= 0 then
+               Left'Last < Integer'Last + Left'First)
+       and then (if Right'First <= 0 then
+                   Right'Last < Integer'Last + Right'First)
+       and then Left'Length = Right'Length;
 
    -------------
    -- L2_Norm --
@@ -340,7 +418,13 @@ pragma Pure (Generic_Array_Operations);
               Right : Result_Scalar) return Result_Scalar is <>;
    function Matrix_Vector_Product
      (Left  : Matrix;
-      Right : Right_Vector) return Result_Vector;
+      Right : Right_Vector) return Result_Vector
+   with
+     Pre => (if Left'First (2) <= 0 then
+               Left'Last (2) < Integer'Last + Left'First (2))
+       and then (if Right'First <= 0 then
+                   Right'Last < Integer'Last + Right'First)
+       and then Left'Length (2) = Right'Length;
 
    ---------------------------
    -- Vector_Matrix_Product --
@@ -363,7 +447,13 @@ pragma Pure (Generic_Array_Operations);
               Right : Result_Scalar) return Result_Scalar is <>;
    function Vector_Matrix_Product
      (Left  : Left_Vector;
-      Right : Matrix) return Result_Vector;
+      Right : Matrix) return Result_Vector
+   with
+     Pre => (if Left'First <= 0 then
+               Left'Last < Integer'Last + Left'First)
+       and then (if Right'First (1) <= 0 then
+                   Right'Last (1) < Integer'Last + Right'First (1))
+       and then Left'Length = Right'Length (1);
 
    ---------------------------
    -- Matrix_Matrix_Product --
@@ -388,7 +478,13 @@ pragma Pure (Generic_Array_Operations);
               Right : Result_Scalar) return Result_Scalar is <>;
    function Matrix_Matrix_Product
      (Left  : Left_Matrix;
-      Right : Right_Matrix) return Result_Matrix;
+      Right : Right_Matrix) return Result_Matrix
+   with
+     Pre => (if Left'First (2) <= 0 then
+               Left'Last (2) < Integer'Last + Left'First (2))
+       and then (if Right'First (1) <= 0 then
+                   Right'Last (1) < Integer'Last + Right'First (1))
+       and then Left'Length (2) = Right'Length (1);
 
    ----------------------------
    -- Matrix_Vector_Solution --
@@ -404,7 +500,16 @@ pragma Pure (Generic_Array_Operations);
              (M   : in out Matrix;
               N   : in out Matrix;
               Det : out Scalar) is <>;
-   function Matrix_Vector_Solution (A : Matrix; X : Vector) return Vector;
+   function Matrix_Vector_Solution (A : Matrix; X : Vector) return Vector
+   with
+     Pre => (if A'First (1) <= 0 then
+               A'Last (1) < Integer'Last + A'First (1))
+       and then (if A'First (2) <= 0 then
+                   A'Last (2) < Integer'Last + A'First (2))
+       and then A'Length (1) = A'Length (2)
+       and then (if X'First <= 0 then
+                   X'Last < Integer'Last + X'First)
+       and then A'Length (1) = X'Length;
 
    ----------------------------
    -- Matrix_Matrix_Solution --
@@ -419,7 +524,16 @@ pragma Pure (Generic_Array_Operations);
              (M   : in out Matrix;
               N   : in out Matrix;
               Det : out Scalar) is <>;
-   function Matrix_Matrix_Solution (A : Matrix; X : Matrix) return Matrix;
+   function Matrix_Matrix_Solution (A : Matrix; X : Matrix) return Matrix
+   with
+     Pre => (if A'First (1) <= 0 then
+               A'Last (1) < Integer'Last + A'First (1))
+       and then (if A'First (2) <= 0 then
+                   A'Last (2) < Integer'Last + A'First (2))
+       and then A'Length (1) = A'Length (2)
+       and then (if X'First (1) <= 0 then
+                   X'Last (1) < Integer'Last + X'First (1))
+       and then A'Length (1) = X'Length (1);
 
    ----------
    -- Sqrt --
@@ -436,7 +550,10 @@ pragma Pure (Generic_Array_Operations);
    generic
       type Scalar is private;
       type Matrix is array (Integer range <>, Integer range <>) of Scalar;
-   procedure Swap_Column (A : in out Matrix; Left, Right : Integer);
+   procedure Swap_Column (A : in out Matrix; Left, Right : Integer)
+   with
+     Pre => Left in A'Range (2)
+       and then Right in A'Range (2);
 
    ---------------
    -- Transpose --
@@ -445,7 +562,18 @@ pragma Pure (Generic_Array_Operations);
    generic
       type Scalar is private;
       type Matrix is array (Integer range <>, Integer range <>) of Scalar;
-   procedure Transpose (A : Matrix; R : out Matrix);
+   procedure Transpose (A : Matrix; R : out Matrix)
+   with
+     Relaxed_Initialization => R,
+     Pre  => A'First (1) = R'First (2)
+       and then A'Last (1) = R'Last (2)
+       and then A'First (2) = R'First (1)
+       and then A'Last (2) = R'Last (1)
+       and then (if A'First (1) < 0 then
+                   A'Last (1) <= Integer'Last + A'First (1))
+       and then (if A'First (2) < 0 then
+                   A'Last (2) <= Integer'Last + A'First (2)),
+     Post => R'Initialized;
 
    -------------------------------
    -- Update_Vector_With_Vector --
@@ -457,7 +585,13 @@ pragma Pure (Generic_Array_Operations);
       type X_Vector is array (Integer range <>) of X_Scalar;
       type Y_Vector is array (Integer range <>) of Y_Scalar;
       with procedure Update (X : in out X_Scalar; Y : Y_Scalar);
-   procedure Update_Vector_With_Vector (X : in out X_Vector; Y : Y_Vector);
+   procedure Update_Vector_With_Vector (X : in out X_Vector; Y : Y_Vector)
+   with
+     Pre => (if X'First <= 0 then
+               X'Last < Integer'Last + X'First)
+       and then (if Y'First <= 0 then
+                   Y'Last < Integer'Last + Y'First)
+       and then X'Length = Y'Length;
 
    -------------------------------
    -- Update_Matrix_With_Matrix --
@@ -469,7 +603,18 @@ pragma Pure (Generic_Array_Operations);
       type X_Matrix is array (Integer range <>, Integer range <>) of X_Scalar;
       type Y_Matrix is array (Integer range <>, Integer range <>) of Y_Scalar;
       with procedure Update (X : in out X_Scalar; Y : Y_Scalar);
-   procedure Update_Matrix_With_Matrix (X : in out X_Matrix; Y : Y_Matrix);
+   procedure Update_Matrix_With_Matrix (X : in out X_Matrix; Y : Y_Matrix)
+   with
+     Pre => (if X'First (1) <= 0 then
+               X'Last (1) < Integer'Last + X'First (1))
+       and then (if Y'First (1) <= 0 then
+                   Y'Last (1) < Integer'Last + Y'First (1))
+       and then X'Length (1) = Y'Length (1)
+       and then (if X'First (2) <= 0 then
+                   X'Last (2) < Integer'Last + X'First (2))
+       and then (if Y'First (2) <= 0 then
+                   Y'Last (2) < Integer'Last + Y'First (2))
+       and then X'Length (2) = Y'Length (2);
 
    -----------------
    -- Unit_Matrix --
@@ -483,7 +628,10 @@ pragma Pure (Generic_Array_Operations);
    function Unit_Matrix
      (Order   : Positive;
       First_1 : Integer := 1;
-      First_2 : Integer := 1) return Matrix;
+      First_2 : Integer := 1) return Matrix
+   with
+     Pre => First_1 <= Integer'Last - Order + 1
+       and then First_2 <= Integer'Last - Order + 1;
 
    -----------------
    -- Unit_Vector --
@@ -497,6 +645,10 @@ pragma Pure (Generic_Array_Operations);
    function Unit_Vector
      (Index : Integer;
       Order : Positive;
-      First : Integer := 1) return Vector;
+      First : Integer := 1) return Vector
+   with
+     Pre => Index >= First
+       and then First <= Integer'Last - Order + 1
+       and then Index <= First + (Order - 1);
 
 end System.Generic_Array_Operations;