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.
(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
(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;
(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;
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;
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;
------------------------------
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;
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;
-- 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
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)));