From: Yannick Moy <m...@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