From a398b5479c9c928f7d9999de8b0c6580b733e6a8 Mon Sep 17 00:00:00 2001
From: Yannick Moy <moy@adacore.com>
Date: Mon, 16 Jan 2023 10:55:08 +0000
Subject: ada: Recover proof of runtime units

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

(limited to 'gcc/ada')

diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb
index a9323cf..dd7b032 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 6cf68a5..0682589 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
-- 
cgit v1.1