ada: Adapt proofs of light runtime to current version of SPARK

gcc/ada/ChangeLog:

	* libgnat/a-strmap.adb: Add assert to regain proofs.
	* libgnat/a-strsup.adb: Likewise.
	* libgnat/s-aridou.adb: Add assertions to regain proofs.
	* libgnat/s-arit32.adb: Use Exceptional_Cases to specify Raise.
	* libgnat/s-arit64.adb: Use Round_Quatient from Impl instead of
	redefining it.
	* libgnat/s-arit64.ads: Likewise.
	* libgnat/s-expmod.adb: Regain proof of lemma.
	* libgnat/s-exponn.adb: Likewise.
	* libgnat/s-expont.adb: Likewise.
	* libgnat/s-imgboo.adb: Add local lemma to regain proof.
	* libgnat/s-valuti.ads: Add Always_Terminates on Bad_Value.

11 files changed, 228 insertions, 93 deletions

diff --git a/gcc/ada/libgnat/a-strmap.adb b/gcc/ada/libgnat/a-strmap.adb
index 4131dbd..9285b3f 100644
--- a/gcc/ada/libgnat/a-strmap.adb
+++ b/gcc/ada/libgnat/a-strmap.adb
@@ -148,7 +148,7 @@ is
 
          pragma Loop_Invariant (if Map = Identity then J = 0);
          pragma Loop_Invariant (J <= Character'Pos (C) + 1);
-         pragma Loop_Invariant (Result (1 .. J)'Initialized);
+         pragma Loop_Invariant (for all K in 1 .. J => Result (K)'Initialized);
          pragma Loop_Invariant (for all K in 1 .. J => Result (K) <= C);
          pragma Loop_Invariant
            (SPARK_Proof_Sorted_Character_Sequence (Result (1 .. J)));
@@ -404,6 +404,7 @@ is
          pragma Loop_Invariant
            (for all K in 1 .. J => Result (K) = Map (Domain (K)));
       end loop;
+      pragma Assert (Is_Domain (Map, Domain (1 .. J)));
 
       --  Show the equality of Domain and To_Domain(Map)
 
diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb
index 8004422..3e5c0d7 100644
--- a/gcc/ada/libgnat/a-strsup.adb
+++ b/gcc/ada/libgnat/a-strsup.adb
@@ -1627,6 +1627,8 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
                        Result.Data (K) =
                          Item (Item'Last - (Max_Length - K) mod Ilen));
                end loop;
+               pragma Assert
+                 (Result.Data (1 .. Max_Length)'Initialized);
 
             when Strings.Error =>
                raise Ada.Strings.Length_Error;
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index 6f27487..41fcfed 100644
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -54,6 +54,10 @@ is
    pragma Suppress (Overflow_Check);
    pragma Suppress (Range_Check);
 
+   pragma Warnings
+     (Off, "statement has no effect",
+      Reason => "Ghost code on dead paths is used for verification only");
+
    function To_Uns is new Ada.Unchecked_Conversion (Double_Int, Double_Uns);
    function To_Int is new Ada.Unchecked_Conversion (Double_Uns, Double_Int);
 
@@ -123,7 +127,9 @@ is
    function "abs" (X : Double_Int) return Double_Uns is
      (if X = Double_Int'First
       then Double_Uns'(2 ** (Double_Size - 1))
-      else Double_Uns (Double_Int'(abs X)));
+      else Double_Uns (Double_Int'(abs X)))
+   with Post => abs (Big (X)) = Big ("abs"'Result),
+        Annotate => (GNATprove, Hide_Info, "Expression_Function_Body");
    --  Convert absolute value of X to unsigned. Note that we can't just use
    --  the expression of the Else since it overflows for X = Double_Int'First.
 
@@ -146,8 +152,7 @@ is
                     + Big_2xxSingle * Big (Double_Uns (X2))
                                     + Big (Double_Uns (X3)))
    with
-     Ghost,
-     Annotate => (GNATprove, Inline_For_Proof);
+     Ghost;
    --  X1&X2&X3 as a big integer
 
    function Le3 (X1, X2, X3, Y1, Y2, Y3 : Single_Uns) return Boolean
@@ -186,7 +191,8 @@ is
    --  0 .. 2 ** (Double_Size - 1) - 1, then the corresponding non-negative
    --  signed integer is returned, otherwise constraint error is raised.
 
-   procedure Raise_Error;
+   procedure Raise_Error with
+     Exceptional_Cases => (Constraint_Error => True);
    pragma No_Return (Raise_Error);
    --  Raise constraint error with appropriate message
 
@@ -1897,9 +1903,6 @@ is
    procedure Raise_Error is
    begin
       raise Constraint_Error with "Double arithmetic overflow";
-      pragma Annotate
-        (GNATprove, Intentional, "exception might be raised",
-         "Procedure Raise_Error is called to signal input errors");
    end Raise_Error;
 
    -------------------
@@ -2025,6 +2028,15 @@ is
       --  Proves correctness of the multiplication of divisor by quotient to
       --  compute amount to subtract.
 
+      procedure Prove_Mult_Decomposition_Split2
+        (D1, D2, D2_Hi, D2_Lo, D3, D4 : Big_Integer)
+      with
+        Ghost,
+        Pre  => Is_Mult_Decomposition (D1, D2, D3, D4)
+          and then D2 = Big_2xxSingle * D2_Hi + D2_Lo,
+        Post => Is_Mult_Decomposition (D1 + D2_Hi, D2_Lo, D3, D4);
+      --  Proves decomposition of Mult after splitting second component
+
       procedure Prove_Mult_Decomposition_Split3
         (D1, D2, D3, D3_Hi, D3_Lo, D4 : Big_Integer)
       with
@@ -2327,9 +2339,11 @@ is
               Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2)))
                             + Big_2xxSingle * Big (T3)
                                             + Big (Double_Uns (S3)),
-              Big_2xxSingle * Big (Double_Uns (Lo (T2)))
-            + Big_2xxSingle * Big (Double_Uns (Hi (T1)))
-            = Big_2xxSingle * Big (T3)));
+              By (Big_2xxSingle * Big (Double_Uns (Lo (T2)))
+               + Big_2xxSingle * Big (Double_Uns (Hi (T1)))
+               = Big_2xxSingle * Big (T3),
+               Double_Uns (Lo (T2))
+               + Double_Uns (Hi (T1)) = T3)));
          pragma Assert (Double_Uns (Hi (T3)) + Hi (T2) = Double_Uns (S1));
          Lemma_Add_Commutation (Double_Uns (Hi (T3)), Hi (T2));
          pragma Assert
@@ -2341,6 +2355,14 @@ is
       end Prove_Multiplication;
 
       -------------------------------------
+      -- Prove_Mult_Decomposition_Split2 --
+      -------------------------------------
+
+      procedure Prove_Mult_Decomposition_Split2
+        (D1, D2, D2_Hi, D2_Lo, D3, D4 : Big_Integer)
+      is null;
+
+      -------------------------------------
       -- Prove_Mult_Decomposition_Split3 --
       -------------------------------------
 
@@ -2492,7 +2514,10 @@ is
          pragma Assert
            (Big (Double_Uns (D (2))) + 1 <= Big (Double_Uns (Zlo)));
          Lemma_Div_Definition (T1, Zlo, T1 / Zlo, T1 rem Zlo);
-         pragma Assert (Double_Uns (Lo (T1 rem Zlo)) = T1 rem Zlo);
+         pragma Assert
+           (By (Lo (T1 rem Zlo) = Hi (T2),
+              By (Double_Uns (Lo (T1 rem Zlo)) = T1 rem Zlo,
+                T1 rem Zlo <= Double_Uns (Zlo))));
          Lemma_Hi_Lo (T2, Lo (T1 rem Zlo), D (4));
          pragma Assert (T1 rem Zlo < Double_Uns (Zlo));
          pragma Assert (T1 rem Zlo + Double_Uns'(1) <= Double_Uns (Zlo));
@@ -2501,24 +2526,26 @@ is
          pragma Assert (Big (T1 rem Zlo) + 1 <= Big (Double_Uns (Zlo)));
          Lemma_Div_Definition (T2, Zlo, T2 / Zlo, Ru);
          pragma Assert
-           (Mult = Big (Double_Uns (Zlo)) *
-              (Big_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo)) + Big (Ru));
-         pragma Assert (Big_2xxSingle * Big (Double_Uns (D (2)))
-                                      + Big (Double_Uns (D (3)))
-                        < Big_2xxSingle * (Big (Double_Uns (D (2))) + 1));
+           (By (Big_2xxSingle * Big (Double_Uns (D (2)))
+                + Big (Double_Uns (D (3)))
+                < Big_2xxSingle * (Big (Double_Uns (D (2))) + 1),
+              Mult = Big (Double_Uns (Zlo)) *
+              (Big_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo)) + Big (Ru)));
          Lemma_Div_Lt (Big (T1), Big_2xxSingle, Big (Double_Uns (Zlo)));
          Lemma_Div_Commutation (T1, Double_Uns (Zlo));
          Lemma_Lo_Is_Ident (T1 / Zlo);
          pragma Assert
            (Big (T2) <= Big_2xxSingle * (Big (Double_Uns (Zlo)) - 1)
                                       + Big (Double_Uns (D (4))));
+         Lemma_Hi_Lo (Qu, Lo (T1 / Zlo), Lo (T2 / Zlo));
          Lemma_Div_Lt (Big (T2), Big_2xxSingle, Big (Double_Uns (Zlo)));
          Lemma_Div_Commutation (T2, Double_Uns (Zlo));
          Lemma_Lo_Is_Ident (T2 / Zlo);
-         Lemma_Hi_Lo (Qu, Lo (T1 / Zlo), Lo (T2 / Zlo));
          Lemma_Substitution (Mult, Big (Double_Uns (Zlo)),
                              Big_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo),
                              Big (Qu), Big (Ru));
+         pragma Assert
+           (By (Ru < Double_Uns (Zlo), Ru = T2 rem Zlo));
          Lemma_Lt_Commutation (Ru, Double_Uns (Zlo));
          Lemma_Rev_Div_Definition
            (Mult, Big (Double_Uns (Zlo)), Big (Qu), Big (Ru));
@@ -2606,34 +2633,51 @@ is
             T2 := Double_Uns'(Xhi * Yhi);
 
             Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
+            pragma Assert
+              (Is_Mult_Decomposition
+                 (D1 => Big (Double_Uns (Hi (T2))),
+                  D2 => Big (T3) + Big (Double_Uns (Lo (T2))),
+                  D3 => Big (Double_Uns (D (3))),
+                  D4 => Big (Double_Uns (D (4)))));
 
             T1 := T3 + Lo (T2);
             D (2) := Lo (T1);
 
             Lemma_Add_Commutation (T3, Lo (T2));
             Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
+            Prove_Mult_Decomposition_Split2
+              (D1    => Big (Double_Uns (Hi (T2))),
+               D2    => Big (T1),
+               D2_Lo => Big (Double_Uns (Lo (T1))),
+               D2_Hi => Big (Double_Uns (Hi (T1))),
+               D3    => Big (Double_Uns (D (3))),
+               D4    => Big (Double_Uns (D (4))));
 
             D (1) := Hi (T2) + Hi (T1);
 
-            pragma Assert
-              (Double_Uns (Hi (T2)) + Hi (T1) = Double_Uns (D (1)));
-            Lemma_Add_Commutation (Double_Uns (Hi (T2)), Hi (T1));
-            pragma Assert
-              (Big (Double_Uns (Hi (T2))) + Big (Double_Uns (Hi (T1))) =
-                   Big (Double_Uns (D (1))));
-            pragma Assert
-              (Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
-                                      D2 => Big (Double_Uns (D (2))),
-                                      D3 => Big (Double_Uns (D (3))),
-                                      D4 => Big (Double_Uns (D (4)))));
+            pragma Assert_And_Cut
+              (D'Initialized
+               and Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
+                                          D2 => Big (Double_Uns (D (2))),
+                                          D3 => Big (Double_Uns (D (3))),
+                                          D4 => Big (Double_Uns (D (4)))));
          else
+            pragma Assert
+              (Is_Mult_Decomposition
+                 (D1 => 0,
+                  D2 => Big (Double_Uns (D (2))),
+                  D3 => Big (Double_Uns (D (3)))
+                  + Big (Double_Uns (Xhi)) * Big (Yu),
+                  D4 => Big (Double_Uns (D (4)))));
+
             D (1) := 0;
 
-            pragma Assert
-              (Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
-                                      D2 => Big (Double_Uns (D (2))),
-                                      D3 => Big (Double_Uns (D (3))),
-                                      D4 => Big (Double_Uns (D (4)))));
+            pragma Assert_And_Cut
+              (D'Initialized
+               and Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
+                                          D2 => Big (Double_Uns (D (2))),
+                                          D3 => Big (Double_Uns (D (3))),
+                                          D4 => Big (Double_Uns (D (4)))));
          end if;
 
       else
@@ -2686,6 +2730,13 @@ is
          end if;
 
          D (1) := 0;
+
+         pragma Assert_And_Cut
+           (D'Initialized
+            and Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
+                                       D2 => Big (Double_Uns (D (2))),
+                                       D3 => Big (Double_Uns (D (3))),
+                                       D4 => Big (Double_Uns (D (4)))));
       end if;
 
       pragma Assert_And_Cut
@@ -2914,12 +2965,17 @@ is
                  (Big (Zu) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale));
             end;
          end loop;
+         pragma Assert_And_Cut
+           (Scale <= Single_Size - 1
+            and then (Hi (Zu) and Mask) /= 0
+            and then Mask = Shift_Left (Single_Uns'Last, Single_Size - 1)
+            and then Zu = Shift_Left (abs Z, Scale)
+            and then Big (Zu) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale)
+            and then Mult < Big_2xxDouble * Big (Double_Uns'(abs Z)));
 
          Zhi := Hi (Zu);
          Zlo := Lo (Zu);
 
-         pragma Assert (Shift = 1);
-         pragma Assert (Mask = Shift_Left (Single_Uns'Last, Single_Size - 1));
          pragma Assert ((Zhi and Mask) /= 0);
          pragma Assert (Zhi >= 2 ** (Single_Size - 1));
          pragma Assert (Big (Zu) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale));
@@ -2949,14 +3005,11 @@ is
          D (3) := Lo (T2) or Hi (T3);
          D (4) := Lo (T3);
 
-         pragma Assert (Big (Double_Uns (Hi (T1))) = Big (Double_Uns (D (1))));
-         pragma Assert
-           (Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
-            * Big (Double_Uns (Hi (T1)))
-            = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
-            * Big (Double_Uns (D (1))));
+         pragma Assert (D (1) = Hi (T1) and D (2) = (Lo (T1) or Hi (T2))
+                        and D (3) = (Lo (T2) or Hi (T3)) and D (4) = Lo (T3));
          Lemma_Substitution (Big_2xxDouble * Big (Zu), Big_2xxDouble, Big (Zu),
                              Big (Double_Uns'(abs Z)) * Big_2xx (Scale), 0);
+         pragma Assert (Mult < Big_2xxDouble * Big (Double_Uns'(abs Z)));
          Lemma_Lt_Mult (Mult, Big_2xxDouble * Big (Double_Uns'(abs Z)),
                         Big_2xx (Scale), Big_2xxDouble * Big (Zu));
          pragma Assert (Mult >= Big_0);
@@ -3040,8 +3093,12 @@ is
                   Lemma_Concat_Definition (D (J), D (J + 1));
                   Lemma_Big_Of_Double_Uns_Of_Single_Uns (D (J + 2));
                   pragma Assert (Big_2xxSingle > Big (Double_Uns (D (J + 2))));
-                  pragma Assert (Big3 (D (J), D (J + 1), 0) + Big_2xxSingle
-                                 > Big3 (D (J), D (J + 1), D (J + 2)));
+                  pragma Assert
+                    (By (Big3 (D (J), D (J + 1), 0) + Big_2xxSingle
+                        > Big3 (D (J), D (J + 1), D (J + 2)),
+                    Big3 (D (J), D (J + 1), 0) =
+                       Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (J)))
+                    + Big_2xxSingle * Big (Double_Uns (D (J + 1)))));
                   pragma Assert (Big (Double_Uns'(0)) = 0);
                   pragma Assert (Big (D (J) & D (J + 1)) * Big_2xxSingle =
                     Big_2xxSingle * (Big_2xxSingle * Big (Double_Uns (D (J)))
@@ -3107,7 +3164,8 @@ is
 
                while not Le3 (S1, S2, S3, D (J), D (J + 1), D (J + 2)) loop
                   pragma Loop_Invariant
-                    (for all K in 1 .. J => Qd (K)'Initialized);
+                    (Qd (1)'Initialized
+                     and (if J = 2 then Qd (2)'Initialized));
                   pragma Loop_Invariant (if J = 2 then Qd (1) = Qd1);
                   pragma Loop_Invariant
                     (Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu));
@@ -3131,39 +3189,57 @@ is
                   pragma Assert (Double_Uns (Qd (J)) - Double_Uns'(1)
                                  = Double_Uns (Qd (J) - 1));
                   pragma Assert (Big (Double_Uns'(1)) = 1);
-                  Lemma_Substitution (Big3 (S1, S2, S3), Big (Zu),
-                                      Big (Double_Uns (Qd (J))) - 1,
-                                      Big (Double_Uns (Qd (J) - 1)), 0);
 
                   declare
-                     Prev : constant Single_Uns := Qd (J) - 1 with Ghost;
+                     Prev : constant Single_Uns := Qd (J) with Ghost;
                   begin
                      Qd (J) := Qd (J) - 1;
-
-                     pragma Assert (Qd (J) = Prev);
-                     pragma Assert (Qd (J)'Initialized);
-                     if J = 2 then
-                        pragma Assert (Qd (J - 1)'Initialized);
-                     end if;
-                     pragma Assert (for all K in 1 .. J => Qd (K)'Initialized);
+                     Lemma_Substitution (Big3 (S1, S2, S3), Big (Zu),
+                                         Big (Double_Uns (Prev)) - 1,
+                                         Big (Double_Uns (Qd (J))), 0);
                   end;
 
                   pragma Assert
                     (Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu));
                end loop;
 
+               pragma Assert_And_Cut
+                 (Qd (1)'Initialized
+                  and then (if J = 2 then Qd (2)'Initialized and Qd (1) = Qd1)
+                  and then D'Initialized
+                  and then (if J = 2 then D234'Initialized)
+                  and then Big3 (D (J), D (J + 1), D (J + 2)) =
+                    (if J = 1 then D123 else D234)
+                  and then (if J = 1 then D4 = Big (Double_Uns (D (4))))
+                  and then Big3 (S1, S2, S3) =
+                      Big (Double_Uns (Qd (J))) * Big (Zu)
+                  and then Le3 (S1, S2, S3, D (J), D (J + 1), D (J + 2))
+                  and then Big3 (D (J), D (J + 1), D (J + 2)) -
+                    Big3 (S1, S2, S3) < Big (Zu));
+
                --  Now subtract S1&S2&S3 from D1&D2&D3 ready for next step
 
-               pragma Assert (for all K in 1 .. J => Qd (K)'Initialized);
-               pragma Assert
-                 (Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu));
-               pragma Assert (Big3 (S1, S2, S3) >
-                                Big3 (D (J), D (J + 1), D (J + 2)) - Big (Zu));
                Inline_Le3 (S1, S2, S3, D (J), D (J + 1), D (J + 2));
 
-               Sub3 (D (J), D (J + 1), D (J + 2), S1, S2, S3);
+               declare
+                  D4_G : constant Single_Uns := D (4) with Ghost;
+               begin
+                  Sub3 (D (J), D (J + 1), D (J + 2), S1, S2, S3);
+                  pragma Assert (if J = 1 then D (4) = D4_G);
+                  pragma Assert
+                    (By
+                       (D'Initialized,
+                        D (1)'Initialized and D (2)'Initialized
+                        and D (3)'Initialized and D (4)'Initialized));
+                  pragma Assert
+                    (Big3 (D (J), D (J + 1), D (J + 2)) =
+                     (if J = 1 then D123 else D234)
+                     - Big3 (S1, S2, S3));
+               end;
+
+               pragma Assert
+                 (Big3 (D (J), D (J + 1), D (J + 2)) < Big (Zu));
 
-               pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) < Big (Zu));
                if D (J) > 0 then
                   Lemma_Double_Big_2xxSingle;
                   pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) =
@@ -3222,6 +3298,17 @@ is
 
                end if;
             end loop;
+
+            pragma Assert_And_Cut
+              (Qd (1)'Initialized and then Qd (2)'Initialized
+               and then D'Initialized
+               and then Big_2xxSingle * Big (Double_Uns (D (3)))
+                   + Big (Double_Uns (D (4))) < Big (Zu)
+               and then Mult * Big_2xx (Scale) =
+                   Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
+                                 + Big (Double_Uns (Qd (2))) * Big (Zu)
+                   + Big_2xxSingle * Big (Double_Uns (D (3)))
+                                   + Big (Double_Uns (D (4))));
          end;
 
          --  The two quotient digits are now set, and the remainder of the
@@ -3231,16 +3318,9 @@ is
          --  We rescale the divisor as well, to make the proper comparison
          --  for rounding below.
 
-         pragma Assert (for all K in 1 .. 2 => Qd (K)'Initialized);
          Qu := Qd (1) & Qd (2);
          Ru := D (3) & D (4);
 
-         pragma Assert
-           (Mult * Big_2xx (Scale) =
-              Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
-                            + Big (Double_Uns (Qd (2))) * Big (Zu)
-            + Big_2xxSingle * Big (Double_Uns (D (3)))
-                            + Big (Double_Uns (D (4))));
          Lemma_Hi_Lo (Qu, Qd (1), Qd (2));
          Lemma_Hi_Lo (Ru, D (3), D (4));
          Lemma_Substitution
diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb
index 221ef1e..0f4ce23 100644
--- a/gcc/ada/libgnat/s-arit32.adb
+++ b/gcc/ada/libgnat/s-arit32.adb
@@ -119,7 +119,9 @@ is
    --  0 .. 2**31 - 1, then the corresponding nonnegative signed integer is
    --  returned, otherwise constraint error is raised.
 
-   procedure Raise_Error;
+   procedure Raise_Error with
+     Always_Terminates,
+     Exceptional_Cases => (Constraint_Error => True);
    pragma No_Return (Raise_Error);
    --  Raise constraint error with appropriate message
 
diff --git a/gcc/ada/libgnat/s-arit64.adb b/gcc/ada/libgnat/s-arit64.adb
index 62f7f42..a60e0bb 100644
--- a/gcc/ada/libgnat/s-arit64.adb
+++ b/gcc/ada/libgnat/s-arit64.adb
@@ -28,6 +28,7 @@
 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
 --                                                                          --
 ------------------------------------------------------------------------------
+pragma Assertion_Policy (Ghost => Ignore);
 
 with System.Arith_Double;
 
@@ -51,6 +52,9 @@ is
    function Multiply_With_Ovflo_Check64 (X, Y : Int64) return Int64
      renames Impl.Multiply_With_Ovflo_Check;
 
+   function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer
+     renames Impl.Round_Quotient;
+
    procedure Scaled_Divide64
      (X, Y, Z : Int64;
       Q, R    : out Int64;
diff --git a/gcc/ada/libgnat/s-arit64.ads b/gcc/ada/libgnat/s-arit64.ads
index efc1f5f..09ac7dd 100644
--- a/gcc/ada/libgnat/s-arit64.ads
+++ b/gcc/ada/libgnat/s-arit64.ads
@@ -125,15 +125,15 @@ is
         or else (X < Big (Int64'(0))) = (Y < Big (Int64'(0))))
    with Ghost;
 
-   function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer is
-     (if abs R > (abs Y - Big (Int64'(1))) / Big (Int64'(2)) then
-       (if Same_Sign (X, Y) then Q + Big (Int64'(1))
-        else Q - Big (Int64'(1)))
-      else
-        Q)
-   with
+   function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer with
      Ghost,
-     Pre => Y /= 0 and then Q = X / Y and then R = X rem Y;
+     Pre  => Y /= 0 and then Q = X / Y and then R = X rem Y,
+     Post => Round_Quotient'Result =
+       (if abs R > (abs Y - Big (Int64'(1))) / Big (Int64'(2)) then
+         (if Same_Sign (X, Y) then Q + Big (Int64'(1))
+          else Q - Big (Int64'(1)))
+        else
+          Q);
 
    procedure Scaled_Divide64
      (X, Y, Z : Int64;
diff --git a/gcc/ada/libgnat/s-expmod.adb b/gcc/ada/libgnat/s-expmod.adb
index c991bb7..932050d 100644
--- a/gcc/ada/libgnat/s-expmod.adb
+++ b/gcc/ada/libgnat/s-expmod.adb
@@ -149,14 +149,24 @@ is
    ----------------------
 
    procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) is
+
+      procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) with
+        Pre  => Natural'Last - Exp_2 >= Exp_1,
+        Post => A ** (Exp_1 + Exp_2) = A ** (Exp_1) * A ** (Exp_2);
+
+      ----------------------------
+      -- Lemma_Exp_Distribution --
+      ----------------------------
+
+      procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) is null;
+
    begin
       if Exp rem 2 = 0 then
          pragma Assert (Exp = Exp / 2 + Exp / 2);
       else
          pragma Assert (Exp = Exp / 2 + Exp / 2 + 1);
-         pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2 + 1));
-         pragma Assert (A ** (Exp / 2 + 1) = A ** (Exp / 2) * A);
-         pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
+         Lemma_Exp_Distribution (Exp / 2, Exp / 2 + 1);
+         Lemma_Exp_Distribution (Exp / 2, 1);
       end if;
    end Lemma_Exp_Expand;
 
@@ -253,7 +263,10 @@ is
         Post => Big (Mult (X, Y)) = (Big (X) * Big (Y)) mod M
           and then Big (Mult (X, Y)) < M;
 
-      procedure Lemma_Mult (X, Y : Unsigned) is null;
+      procedure Lemma_Mult (X, Y : Unsigned) is
+      begin
+         pragma Assert (Big (Mult (X, Y)) = (Big (X) * Big (Y)) mod M);
+      end Lemma_Mult;
 
       Rest : Big_Integer with Ghost;
       --  Ghost variable to hold Factor**Exp between Exp and Factor updates
diff --git a/gcc/ada/libgnat/s-exponn.adb b/gcc/ada/libgnat/s-exponn.adb
index 8a80532..29db1db 100644
--- a/gcc/ada/libgnat/s-exponn.adb
+++ b/gcc/ada/libgnat/s-exponn.adb
@@ -185,14 +185,24 @@ is
    ----------------------
 
    procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) is
+
+      procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) with
+        Pre  => A /= 0 and then Natural'Last - Exp_2 >= Exp_1,
+        Post => A ** (Exp_1 + Exp_2) = A ** (Exp_1) * A ** (Exp_2);
+
+      ----------------------------
+      -- Lemma_Exp_Distribution --
+      ----------------------------
+
+      procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) is null;
+
    begin
       if Exp rem 2 = 0 then
          pragma Assert (Exp = Exp / 2 + Exp / 2);
       else
          pragma Assert (Exp = Exp / 2 + Exp / 2 + 1);
-         pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2 + 1));
-         pragma Assert (A ** (Exp / 2 + 1) = A ** (Exp / 2) * A);
-         pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
+         Lemma_Exp_Distribution (Exp / 2, Exp / 2 + 1);
+         Lemma_Exp_Distribution (Exp / 2, 1);
       end if;
    end Lemma_Exp_Expand;
 
diff --git a/gcc/ada/libgnat/s-expont.adb b/gcc/ada/libgnat/s-expont.adb
index 264cb96..fa56c68 100644
--- a/gcc/ada/libgnat/s-expont.adb
+++ b/gcc/ada/libgnat/s-expont.adb
@@ -185,14 +185,24 @@ is
    ----------------------
 
    procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) is
+
+      procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) with
+        Pre  => A /= 0 and then Natural'Last - Exp_2 >= Exp_1,
+        Post => A ** (Exp_1 + Exp_2) = A ** (Exp_1) * A ** (Exp_2);
+
+      ----------------------------
+      -- Lemma_Exp_Distribution --
+      ----------------------------
+
+      procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) is null;
+
    begin
       if Exp rem 2 = 0 then
          pragma Assert (Exp = Exp / 2 + Exp / 2);
       else
          pragma Assert (Exp = Exp / 2 + Exp / 2 + 1);
-         pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2 + 1));
-         pragma Assert (A ** (Exp / 2 + 1) = A ** (Exp / 2) * A);
-         pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
+         Lemma_Exp_Distribution (Exp / 2, Exp / 2 + 1);
+         Lemma_Exp_Distribution (Exp / 2, 1);
       end if;
    end Lemma_Exp_Expand;
 
diff --git a/gcc/ada/libgnat/s-imgboo.adb b/gcc/ada/libgnat/s-imgboo.adb
index 1d1ec72..cd66a0f 100644
--- a/gcc/ada/libgnat/s-imgboo.adb
+++ b/gcc/ada/libgnat/s-imgboo.adb
@@ -41,6 +41,20 @@ package body System.Img_Bool
   with SPARK_Mode
 is
 
+   --  Local lemmas
+
+   procedure Lemma_Is_First_Non_Space_Ghost (S : String; R : Positive) with
+     Ghost,
+     Pre => R in S'Range and then S (R) /= ' '
+       and then System.Val_Spec.Only_Space_Ghost (S, S'First, R - 1),
+     Post => System.Val_Spec.First_Non_Space_Ghost (S, S'First, S'Last) = R;
+
+   ------------------------------------
+   -- Lemma_Is_First_Non_Space_Ghost --
+   ------------------------------------
+
+   procedure Lemma_Is_First_Non_Space_Ghost (S : String; R : Positive) is null;
+
    -------------------
    -- Image_Boolean --
    -------------------
@@ -55,13 +69,11 @@ is
       if V then
          S (1 .. 4) := "TRUE";
          P := 4;
-         pragma Assert
-           (System.Val_Spec.First_Non_Space_Ghost (S, S'First, S'Last) = 1);
+         Lemma_Is_First_Non_Space_Ghost (S, 1);
       else
          S (1 .. 5) := "FALSE";
          P := 5;
-         pragma Assert
-           (System.Val_Spec.First_Non_Space_Ghost (S, S'First, S'Last) = 1);
+         Lemma_Is_First_Non_Space_Ghost (S, 1);
       end if;
    end Image_Boolean;
 
diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads
index cc804f4..6f91c36 100644
--- a/gcc/ada/libgnat/s-valuti.ads
+++ b/gcc/ada/libgnat/s-valuti.ads
@@ -54,6 +54,7 @@ is
 
    procedure Bad_Value (S : String)
    with
+     Always_Terminates,
      Depends => (null => S),
      Exceptional_Cases => (others => Standard.False);
    pragma No_Return (Bad_Value);