diff options
author | Yannick Moy <moy@adacore.com> | 2024-01-12 11:30:38 +0000 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2024-05-07 09:55:54 +0200 |
commit | 1955a35a46e4667cccf8d22116edc29b88e3e729 (patch) | |
tree | e4634c485f70b5b79557ab5946c4212815dbacee | |
parent | 711326014d078f330085127a200edb810191856d (diff) | |
download | gcc-1955a35a46e4667cccf8d22116edc29b88e3e729.zip gcc-1955a35a46e4667cccf8d22116edc29b88e3e729.tar.gz gcc-1955a35a46e4667cccf8d22116edc29b88e3e729.tar.bz2 |
ada: Adapt proof of runtime units
Restore proof of runtime units after changes in SPARK.
gcc/ada/
* libgnat/a-strsea.adb (Index): Add assertions.
* libgnat/a-strsup.ads ("="): Remove useless precondition.
* libgnat/s-aridou.adb (Prove_Rounding_Case): Add assertions.
(Lemma_Shift_Right): Add call to lemma.
* libgnat/s-arit32.adb (Prove_Rounding_Case): Add assertion.
(Prove_ Signs): Add assertions.
(Scaled_Divide32): Add assertions.
-rw-r--r-- | gcc/ada/libgnat/a-strsea.adb | 2 | ||||
-rw-r--r-- | gcc/ada/libgnat/a-strsup.ads | 1 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-aridou.adb | 9 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-arit32.adb | 17 |
4 files changed, 24 insertions, 5 deletions
diff --git a/gcc/ada/libgnat/a-strsea.adb b/gcc/ada/libgnat/a-strsea.adb index 1dad3be..54f1219 100644 --- a/gcc/ada/libgnat/a-strsea.adb +++ b/gcc/ada/libgnat/a-strsea.adb @@ -623,6 +623,7 @@ package body Ada.Strings.Search with SPARK_Mode is (if (for some J in From .. Source'Last - PL1 => Match (Source, Pattern, Mapping, J)) then Result in From .. Source'Last - PL1 + and then Match (Source, Pattern, Mapping, Result) else Result = 0); else @@ -636,6 +637,7 @@ package body Ada.Strings.Search with SPARK_Mode is (if (for some J in Source'First .. From - PL1 => Match (Source, Pattern, Mapping, J)) then Result in Source'First .. From - PL1 + and then Match (Source, Pattern, Mapping, Result) else Result = 0); end if; diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads index cb1dcc9..6c360f1 100644 --- a/gcc/ada/libgnat/a-strsup.ads +++ b/gcc/ada/libgnat/a-strsup.ads @@ -689,7 +689,6 @@ is (Left : Super_String; Right : Super_String) return Boolean with - Pre => Left.Max_Length = Right.Max_Length, Post => "="'Result = (Super_To_String (Left) = Super_To_String (Right)), Global => null; diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index ac25e6a..6f27487 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -971,7 +971,7 @@ is procedure Prove_Rounding_Case is begin if Same_Sign (Big (X), Big (Y) * Big (Z)) then - null; + pragma Assert (abs Big_Q = Big (Qu)); end if; end Prove_Rounding_Case; @@ -1603,6 +1603,7 @@ is pragma Loop_Invariant (XX = Shift_Right (X, J)); pragma Loop_Invariant (XX = X / Double_Uns'(2) ** J); end loop; + Lemma_Div_Commutation (X, Double_Uns'(2) ** Shift); end Lemma_Shift_Right; ------------------------------ @@ -2441,7 +2442,11 @@ is procedure Prove_Rounding_Case is begin if Same_Sign (Big (X) * Big (Y), Big (Z)) then - null; + pragma Assert + (abs Big_Q = + (if Ru > (Zu - Double_Uns'(1)) / Double_Uns'(2) + then abs Quot + 1 + else abs Quot)); end if; end Prove_Rounding_Case; diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb index 59a6db0..221ef1e 100644 --- a/gcc/ada/libgnat/s-arit32.adb +++ b/gcc/ada/libgnat/s-arit32.adb @@ -415,7 +415,11 @@ is procedure Prove_Rounding_Case is begin if Same_Sign (Big (X) * Big (Y), Big (Z)) then - null; + pragma Assert + (abs Big_Q = + (if Ru > (Zu - Uns32'(1)) / Uns32'(2) + then abs Quot + 1 + else abs Quot)); end if; end Prove_Rounding_Case; @@ -432,7 +436,14 @@ is -- Prove_Signs -- ----------------- - procedure Prove_Signs is null; + procedure Prove_Signs is + begin + if (X >= 0) = (Y >= 0) then + pragma Assert (Big (R) = Big_R and then Big (Q) = Big_Q); + else + pragma Assert (Big (R) = Big_R and then Big (Q) = Big_Q); + end if; + end Prove_Signs; -- Start of processing for Scaled_Divide32 @@ -483,6 +494,8 @@ is Lemma_Div_Commutation (D, Uns64 (Zu)); Lemma_Rem_Commutation (D, Uns64 (Zu)); + pragma Assert (Uns64 (Qu) = D / Uns64 (Zu)); + pragma Assert (Uns64 (Ru) = D rem Uns64 (Zu)); pragma Assert (Big (Ru) = abs Big_R); pragma Assert (Big (Qu) = abs Quot); pragma Assert (Big (Zu) = Big (Uns32'(abs Z))); |