[COMMITTED] ada: Recover proof of runtime units

[COMMITTED] ada: Recover proof of runtime units

[Marc Poulhiès]

From: Yannick Moy <moy@adacore.com>

Changes needed to make proof go through, after some change in
GNAT and SPARK.

gcc/ada/

	* libgnat/a-strsup.adb (Super_Slice): Reorder component assignment
	to avoid failing predicate check related to initialization.
	* libgnat/s-expmod.adb (Exp_Modular): Add intermediate assertion.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/a-strsup.adb | 11 ++++++-----
 gcc/ada/libgnat/s-expmod.adb |  1 +
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb
index a9323cf0d3e..dd7b0322b76 100644
--- a/gcc/ada/libgnat/a-strsup.adb
+++ b/gcc/ada/libgnat/a-strsup.adb
@@ -1654,6 +1654,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
       Low    : Positive;
       High   : Natural) return Super_String
    is
+      Len : constant Natural := (if Low > High then 0 else High - Low + 1);
    begin
       return Result : Super_String (Source.Max_Length) do
          if Low - 1 > Source.Current_Length
@@ -1662,9 +1663,8 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
             raise Index_Error;
          end if;
 
-         Result.Current_Length := (if Low > High then 0 else High - Low + 1);
-         Result.Data (1 .. Result.Current_Length) :=
-           Source.Data (Low .. High);
+         Result.Data (1 .. Len) := Source.Data (Low .. High);
+         Result.Current_Length := Len;
       end return;
    end Super_Slice;
 
@@ -1674,6 +1674,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
       Low    : Positive;
       High   : Natural)
    is
+      Len : constant Natural := (if Low > High then 0 else High - Low + 1);
    begin
       if Low - 1 > Source.Current_Length
         or else High > Source.Current_Length
@@ -1681,8 +1682,8 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
          raise Index_Error;
       end if;
 
-      Target.Current_Length := (if Low > High then 0 else High - Low + 1);
-      Target.Data (1 .. Target.Current_Length) := Source.Data (Low .. High);
+      Target.Data (1 .. Len) := Source.Data (Low .. High);
+      Target.Current_Length := Len;
    end Super_Slice;
 
    ----------------
diff --git a/gcc/ada/libgnat/s-expmod.adb b/gcc/ada/libgnat/s-expmod.adb
index 6cf68a5b586..0682589d352 100644
--- a/gcc/ada/libgnat/s-expmod.adb
+++ b/gcc/ada/libgnat/s-expmod.adb
@@ -309,6 +309,7 @@ is
             Lemma_Mod_Mod (Rest * Rest, Big (Modulus));
             Lemma_Mod_Ident (Big (Result), Big (Modulus));
             Lemma_Mult_Mod (Big (Result), Rest * Rest, Big (Modulus));
+            pragma Assert (Big (Factor) >= 0);
             Lemma_Mult_Mod (Big (Result), Big (Factor) ** Exp,
                                Big (Modulus));
             pragma Assert (Equal_Modulo
-- 
2.40.0