https://gcc.gnu.org/g:1955a35a46e4667cccf8d22116edc29b88e3e729
commit r15-252-g1955a35a46e4667cccf8d22116edc29b88e3e729
Author: Yannick Moy <m...@adacore.com>
Date: Fri Jan 12 11:30:38 2024 +0000
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.
Diff:
---
gcc/ada/libgnat/a-strsea.adb | 2 ++
gcc/ada/libgnat/a-strsup.ads | 1 -
gcc/ada/libgnat/s-aridou.adb | 9 +++++++--
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 1dad3be4f4a..54f12199fcc 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 cb1dcc9a076..6c360f1982b 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 ac25e6a9183..6f27487db37 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 59a6db08199..221ef1e635e 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)));
