diff options
author | Yannick Moy <moy@adacore.com> | 2023-01-16 10:55:08 +0000 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-15 11:36:43 +0200 |
commit | a398b5479c9c928f7d9999de8b0c6580b733e6a8 (patch) | |
tree | ec9ebb5ba8a8db3dc01a4b6cd7bb21a40a7597d3 /gcc | |
parent | 75fb45f0692270efa1a89590e0d7dd0688101e8b (diff) | |
download | gcc-a398b5479c9c928f7d9999de8b0c6580b733e6a8.zip gcc-a398b5479c9c928f7d9999de8b0c6580b733e6a8.tar.gz gcc-a398b5479c9c928f7d9999de8b0c6580b733e6a8.tar.bz2 |
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.
Diffstat (limited to 'gcc')
-rw-r--r-- | gcc/ada/libgnat/a-strsup.adb | 11 | ||||
-rw-r--r-- | 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 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 |