https://gcc.gnu.org/g:f62972f5cab9708f4e4dac6ad9743ee8a68bde72
commit r15-5245-gf62972f5cab9708f4e4dac6ad9743ee8a68bde72
Author: Claire Dross <dr...@adacore.com>
Date: Fri Oct 18 11:45:29 2024 +0200
ada: Adapt proofs of light runtime to current version of SPARK
gcc/ada/ChangeLog:
* libgnat/a-strmap.adb: Add assert to regain proofs.
* libgnat/a-strsup.adb: Likewise.
* libgnat/s-aridou.adb: Add assertions to regain proofs.
* libgnat/s-arit32.adb: Use Exceptional_Cases to specify Raise.
* libgnat/s-arit64.adb: Use Round_Quatient from Impl instead of
redefining it.
* libgnat/s-arit64.ads: Likewise.
* libgnat/s-expmod.adb: Regain proof of lemma.
* libgnat/s-exponn.adb: Likewise.
* libgnat/s-expont.adb: Likewise.
* libgnat/s-imgboo.adb: Add local lemma to regain proof.
* libgnat/s-valuti.ads: Add Always_Terminates on Bad_Value.
Diff:
---
gcc/ada/libgnat/a-strmap.adb | 3 +-
gcc/ada/libgnat/a-strsup.adb | 2 +
gcc/ada/libgnat/s-aridou.adb | 218 +++++++++++++++++++++++++++++--------------
gcc/ada/libgnat/s-arit32.adb | 4 +-
gcc/ada/libgnat/s-arit64.adb | 4 +
gcc/ada/libgnat/s-arit64.ads | 16 ++--
gcc/ada/libgnat/s-expmod.adb | 21 ++++-
gcc/ada/libgnat/s-exponn.adb | 16 +++-
gcc/ada/libgnat/s-expont.adb | 16 +++-
gcc/ada/libgnat/s-imgboo.adb | 20 +++-
gcc/ada/libgnat/s-valuti.ads | 1 +
11 files changed, 228 insertions(+), 93 deletions(-)
diff --git a/gcc/ada/libgnat/a-strmap.adb b/gcc/ada/libgnat/a-strmap.adb
index 4131dbd80211..9285b3f85b7d 100644
--- a/gcc/ada/libgnat/a-strmap.adb
+++ b/gcc/ada/libgnat/a-strmap.adb
@@ -148,7 +148,7 @@ is
pragma Loop_Invariant (if Map = Identity then J = 0);
pragma Loop_Invariant (J <= Character'Pos (C) + 1);
- pragma Loop_Invariant (Result (1 .. J)'Initialized);
+ pragma Loop_Invariant (for all K in 1 .. J => Result (K)'Initialized);
pragma Loop_Invariant (for all K in 1 .. J => Result (K) <= C);
pragma Loop_Invariant
(SPARK_Proof_Sorted_Character_Sequence (Result (1 .. J)));
@@ -404,6 +404,7 @@ is
pragma Loop_Invariant
(for all K in 1 .. J => Result (K) = Map (Domain (K)));
end loop;
+ pragma Assert (Is_Domain (Map, Domain (1 .. J)));
-- Show the equality of Domain and To_Domain(Map)
diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb
index 80044225d3ca..3e5c0d7f22d1 100644
--- a/gcc/ada/libgnat/a-strsup.adb
+++ b/gcc/ada/libgnat/a-strsup.adb
@@ -1627,6 +1627,8 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
Result.Data (K) =
Item (Item'Last - (Max_Length - K) mod Ilen));
end loop;
+ pragma Assert
+ (Result.Data (1 .. Max_Length)'Initialized);
when Strings.Error =>
raise Ada.Strings.Length_Error;
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index 6f27487db371..41fcfed0e927 100644
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -54,6 +54,10 @@ is
pragma Suppress (Overflow_Check);
pragma Suppress (Range_Check);
+ pragma Warnings
+ (Off, "statement has no effect",
+ Reason => "Ghost code on dead paths is used for verification only");
+
function To_Uns is new Ada.Unchecked_Conversion (Double_Int, Double_Uns);
function To_Int is new Ada.Unchecked_Conversion (Double_Uns, Double_Int);
@@ -123,7 +127,9 @@ is
function "abs" (X : Double_Int) return Double_Uns is
(if X = Double_Int'First
then Double_Uns'(2 ** (Double_Size - 1))
- else Double_Uns (Double_Int'(abs X)));
+ else Double_Uns (Double_Int'(abs X)))
+ with Post => abs (Big (X)) = Big ("abs"'Result),
+ Annotate => (GNATprove, Hide_Info, "Expression_Function_Body");
-- Convert absolute value of X to unsigned. Note that we can't just use
-- the expression of the Else since it overflows for X = Double_Int'First.
@@ -146,8 +152,7 @@ is
+ Big_2xxSingle * Big (Double_Uns (X2))
+ Big (Double_Uns (X3)))
with
- Ghost,
- Annotate => (GNATprove, Inline_For_Proof);
+ Ghost;
-- X1&X2&X3 as a big integer
function Le3 (X1, X2, X3, Y1, Y2, Y3 : Single_Uns) return Boolean
@@ -186,7 +191,8 @@ is
-- 0 .. 2 ** (Double_Size - 1) - 1, then the corresponding non-negative
-- signed integer is returned, otherwise constraint error is raised.
- procedure Raise_Error;
+ procedure Raise_Error with
+ Exceptional_Cases => (Constraint_Error => True);
pragma No_Return (Raise_Error);
-- Raise constraint error with appropriate message
@@ -1897,9 +1903,6 @@ is
procedure Raise_Error is
begin
raise Constraint_Error with "Double arithmetic overflow";
- pragma Annotate
- (GNATprove, Intentional, "exception might be raised",
- "Procedure Raise_Error is called to signal input errors");
end Raise_Error;
-------------------
@@ -2025,6 +2028,15 @@ is
-- Proves correctness of the multiplication of divisor by quotient to
-- compute amount to subtract.
+ procedure Prove_Mult_Decomposition_Split2
+ (D1, D2, D2_Hi, D2_Lo, D3, D4 : Big_Integer)
+ with
+ Ghost,
+ Pre => Is_Mult_Decomposition (D1, D2, D3, D4)
+ and then D2 = Big_2xxSingle * D2_Hi + D2_Lo,
+ Post => Is_Mult_Decomposition (D1 + D2_Hi, D2_Lo, D3, D4);
+ -- Proves decomposition of Mult after splitting second component
+
procedure Prove_Mult_Decomposition_Split3
(D1, D2, D3, D3_Hi, D3_Lo, D4 : Big_Integer)
with
@@ -2327,9 +2339,11 @@ is
Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2)))
+ Big_2xxSingle * Big (T3)
+ Big (Double_Uns (S3)),
- Big_2xxSingle * Big (Double_Uns (Lo (T2)))
- + Big_2xxSingle * Big (Double_Uns (Hi (T1)))
- = Big_2xxSingle * Big (T3)));
+ By (Big_2xxSingle * Big (Double_Uns (Lo (T2)))
+ + Big_2xxSingle * Big (Double_Uns (Hi (T1)))
+ = Big_2xxSingle * Big (T3),
+ Double_Uns (Lo (T2))
+ + Double_Uns (Hi (T1)) = T3)));
pragma Assert (Double_Uns (Hi (T3)) + Hi (T2) = Double_Uns (S1));
Lemma_Add_Commutation (Double_Uns (Hi (T3)), Hi (T2));
pragma Assert
@@ -2340,6 +2354,14 @@ is
Big (Double_Uns (Hi (T2))));
end Prove_Multiplication;
+ -------------------------------------
+ -- Prove_Mult_Decomposition_Split2 --
+ -------------------------------------
+
+ procedure Prove_Mult_Decomposition_Split2
+ (D1, D2, D2_Hi, D2_Lo, D3, D4 : Big_Integer)
+ is null;
+
-------------------------------------
-- Prove_Mult_Decomposition_Split3 --
-------------------------------------
@@ -2492,7 +2514,10 @@ is
pragma Assert
(Big (Double_Uns (D (2))) + 1 <= Big (Double_Uns (Zlo)));
Lemma_Div_Definition (T1, Zlo, T1 / Zlo, T1 rem Zlo);
- pragma Assert (Double_Uns (Lo (T1 rem Zlo)) = T1 rem Zlo);
+ pragma Assert
+ (By (Lo (T1 rem Zlo) = Hi (T2),
+ By (Double_Uns (Lo (T1 rem Zlo)) = T1 rem Zlo,
+ T1 rem Zlo <= Double_Uns (Zlo))));
Lemma_Hi_Lo (T2, Lo (T1 rem Zlo), D (4));
pragma Assert (T1 rem Zlo < Double_Uns (Zlo));
pragma Assert (T1 rem Zlo + Double_Uns'(1) <= Double_Uns (Zlo));
@@ -2501,24 +2526,26 @@ is
pragma Assert (Big (T1 rem Zlo) + 1 <= Big (Double_Uns (Zlo)));
Lemma_Div_Definition (T2, Zlo, T2 / Zlo, Ru);
pragma Assert
- (Mult = Big (Double_Uns (Zlo)) *
- (Big_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo)) + Big (Ru));
- pragma Assert (Big_2xxSingle * Big (Double_Uns (D (2)))
- + Big (Double_Uns (D (3)))
- < Big_2xxSingle * (Big (Double_Uns (D (2))) + 1));
+ (By (Big_2xxSingle * Big (Double_Uns (D (2)))
+ + Big (Double_Uns (D (3)))
+ < Big_2xxSingle * (Big (Double_Uns (D (2))) + 1),
+ Mult = Big (Double_Uns (Zlo)) *
+ (Big_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo)) + Big (Ru)));
Lemma_Div_Lt (Big (T1), Big_2xxSingle, Big (Double_Uns (Zlo)));
Lemma_Div_Commutation (T1, Double_Uns (Zlo));
Lemma_Lo_Is_Ident (T1 / Zlo);
pragma Assert
(Big (T2) <= Big_2xxSingle * (Big (Double_Uns (Zlo)) - 1)
+ Big (Double_Uns (D (4))));
+ Lemma_Hi_Lo (Qu, Lo (T1 / Zlo), Lo (T2 / Zlo));
Lemma_Div_Lt (Big (T2), Big_2xxSingle, Big (Double_Uns (Zlo)));
Lemma_Div_Commutation (T2, Double_Uns (Zlo));
Lemma_Lo_Is_Ident (T2 / Zlo);
- Lemma_Hi_Lo (Qu, Lo (T1 / Zlo), Lo (T2 / Zlo));
Lemma_Substitution (Mult, Big (Double_Uns (Zlo)),
Big_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo),
Big (Qu), Big (Ru));
+ pragma Assert
+ (By (Ru < Double_Uns (Zlo), Ru = T2 rem Zlo));
Lemma_Lt_Commutation (Ru, Double_Uns (Zlo));
Lemma_Rev_Div_Definition
(Mult, Big (Double_Uns (Zlo)), Big (Qu), Big (Ru));
@@ -2606,34 +2633,51 @@ is
T2 := Double_Uns'(Xhi * Yhi);
Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
+ pragma Assert
+ (Is_Mult_Decomposition
+ (D1 => Big (Double_Uns (Hi (T2))),
+ D2 => Big (T3) + Big (Double_Uns (Lo (T2))),
+ D3 => Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))));
T1 := T3 + Lo (T2);
D (2) := Lo (T1);
Lemma_Add_Commutation (T3, Lo (T2));
Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
+ Prove_Mult_Decomposition_Split2
+ (D1 => Big (Double_Uns (Hi (T2))),
+ D2 => Big (T1),
+ D2_Lo => Big (Double_Uns (Lo (T1))),
+ D2_Hi => Big (Double_Uns (Hi (T1))),
+ D3 => Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4))));
D (1) := Hi (T2) + Hi (T1);
- pragma Assert
- (Double_Uns (Hi (T2)) + Hi (T1) = Double_Uns (D (1)));
- Lemma_Add_Commutation (Double_Uns (Hi (T2)), Hi (T1));
- pragma Assert
- (Big (Double_Uns (Hi (T2))) + Big (Double_Uns (Hi (T1))) =
- Big (Double_Uns (D (1))));
- pragma Assert
- (Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
- D2 => Big (Double_Uns (D (2))),
- D3 => Big (Double_Uns (D (3))),
- D4 => Big (Double_Uns (D (4)))));
+ pragma Assert_And_Cut
+ (D'Initialized
+ and Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
+ D2 => Big (Double_Uns (D (2))),
+ D3 => Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))));
else
+ pragma Assert
+ (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (Double_Uns (D (2))),
+ D3 => Big (Double_Uns (D (3)))
+ + Big (Double_Uns (Xhi)) * Big (Yu),
+ D4 => Big (Double_Uns (D (4)))));
+
D (1) := 0;
- pragma Assert
- (Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
- D2 => Big (Double_Uns (D (2))),
- D3 => Big (Double_Uns (D (3))),
- D4 => Big (Double_Uns (D (4)))));
+ pragma Assert_And_Cut
+ (D'Initialized
+ and Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
+ D2 => Big (Double_Uns (D (2))),
+ D3 => Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))));
end if;
else
@@ -2686,6 +2730,13 @@ is
end if;
D (1) := 0;
+
+ pragma Assert_And_Cut
+ (D'Initialized
+ and Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
+ D2 => Big (Double_Uns (D (2))),
+ D3 => Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))));
end if;
pragma Assert_And_Cut
@@ -2914,12 +2965,17 @@ is
(Big (Zu) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale));
end;
end loop;
+ pragma Assert_And_Cut
+ (Scale <= Single_Size - 1
+ and then (Hi (Zu) and Mask) /= 0
+ and then Mask = Shift_Left (Single_Uns'Last, Single_Size - 1)
+ and then Zu = Shift_Left (abs Z, Scale)
+ and then Big (Zu) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale)
+ and then Mult < Big_2xxDouble * Big (Double_Uns'(abs Z)));
Zhi := Hi (Zu);
Zlo := Lo (Zu);
- pragma Assert (Shift = 1);
- pragma Assert (Mask = Shift_Left (Single_Uns'Last, Single_Size - 1));
pragma Assert ((Zhi and Mask) /= 0);
pragma Assert (Zhi >= 2 ** (Single_Size - 1));
pragma Assert (Big (Zu) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale));
@@ -2949,14 +3005,11 @@ is
D (3) := Lo (T2) or Hi (T3);
D (4) := Lo (T3);
- pragma Assert (Big (Double_Uns (Hi (T1))) = Big (Double_Uns (D (1))));
- pragma Assert
- (Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
- * Big (Double_Uns (Hi (T1)))
- = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
- * Big (Double_Uns (D (1))));
+ pragma Assert (D (1) = Hi (T1) and D (2) = (Lo (T1) or Hi (T2))
+ and D (3) = (Lo (T2) or Hi (T3)) and D (4) = Lo (T3));
Lemma_Substitution (Big_2xxDouble * Big (Zu), Big_2xxDouble, Big (Zu),
Big (Double_Uns'(abs Z)) * Big_2xx (Scale), 0);
+ pragma Assert (Mult < Big_2xxDouble * Big (Double_Uns'(abs Z)));
Lemma_Lt_Mult (Mult, Big_2xxDouble * Big (Double_Uns'(abs Z)),
Big_2xx (Scale), Big_2xxDouble * Big (Zu));
pragma Assert (Mult >= Big_0);
@@ -3040,8 +3093,12 @@ is
Lemma_Concat_Definition (D (J), D (J + 1));
Lemma_Big_Of_Double_Uns_Of_Single_Uns (D (J + 2));
pragma Assert (Big_2xxSingle > Big (Double_Uns (D (J + 2))));
- pragma Assert (Big3 (D (J), D (J + 1), 0) + Big_2xxSingle
- > Big3 (D (J), D (J + 1), D (J + 2)));
+ pragma Assert
+ (By (Big3 (D (J), D (J + 1), 0) + Big_2xxSingle
+ > Big3 (D (J), D (J + 1), D (J + 2)),
+ Big3 (D (J), D (J + 1), 0) =
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (J)))
+ + Big_2xxSingle * Big (Double_Uns (D (J + 1)))));
pragma Assert (Big (Double_Uns'(0)) = 0);
pragma Assert (Big (D (J) & D (J + 1)) * Big_2xxSingle =
Big_2xxSingle * (Big_2xxSingle * Big (Double_Uns (D (J)))
@@ -3107,7 +3164,8 @@ is
while not Le3 (S1, S2, S3, D (J), D (J + 1), D (J + 2)) loop
pragma Loop_Invariant
- (for all K in 1 .. J => Qd (K)'Initialized);
+ (Qd (1)'Initialized
+ and (if J = 2 then Qd (2)'Initialized));
pragma Loop_Invariant (if J = 2 then Qd (1) = Qd1);
pragma Loop_Invariant
(Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu));
@@ -3131,39 +3189,57 @@ is
pragma Assert (Double_Uns (Qd (J)) - Double_Uns'(1)
= Double_Uns (Qd (J) - 1));
pragma Assert (Big (Double_Uns'(1)) = 1);
- Lemma_Substitution (Big3 (S1, S2, S3), Big (Zu),
- Big (Double_Uns (Qd (J))) - 1,
- Big (Double_Uns (Qd (J) - 1)), 0);
declare
- Prev : constant Single_Uns := Qd (J) - 1 with Ghost;
+ Prev : constant Single_Uns := Qd (J) with Ghost;
begin
Qd (J) := Qd (J) - 1;
-
- pragma Assert (Qd (J) = Prev);
- pragma Assert (Qd (J)'Initialized);
- if J = 2 then
- pragma Assert (Qd (J - 1)'Initialized);
- end if;
- pragma Assert (for all K in 1 .. J => Qd (K)'Initialized);
+ Lemma_Substitution (Big3 (S1, S2, S3), Big (Zu),
+ Big (Double_Uns (Prev)) - 1,
+ Big (Double_Uns (Qd (J))), 0);
end;
pragma Assert
(Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu));
end loop;
+ pragma Assert_And_Cut
+ (Qd (1)'Initialized
+ and then (if J = 2 then Qd (2)'Initialized and Qd (1) = Qd1)
+ and then D'Initialized
+ and then (if J = 2 then D234'Initialized)
+ and then Big3 (D (J), D (J + 1), D (J + 2)) =
+ (if J = 1 then D123 else D234)
+ and then (if J = 1 then D4 = Big (Double_Uns (D (4))))
+ and then Big3 (S1, S2, S3) =
+ Big (Double_Uns (Qd (J))) * Big (Zu)
+ and then Le3 (S1, S2, S3, D (J), D (J + 1), D (J + 2))
+ and then Big3 (D (J), D (J + 1), D (J + 2)) -
+ Big3 (S1, S2, S3) < Big (Zu));
+
-- Now subtract S1&S2&S3 from D1&D2&D3 ready for next step
- pragma Assert (for all K in 1 .. J => Qd (K)'Initialized);
- pragma Assert
- (Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu));
- pragma Assert (Big3 (S1, S2, S3) >
- Big3 (D (J), D (J + 1), D (J + 2)) - Big (Zu));
Inline_Le3 (S1, S2, S3, D (J), D (J + 1), D (J + 2));
- Sub3 (D (J), D (J + 1), D (J + 2), S1, S2, S3);
+ declare
+ D4_G : constant Single_Uns := D (4) with Ghost;
+ begin
+ Sub3 (D (J), D (J + 1), D (J + 2), S1, S2, S3);
+ pragma Assert (if J = 1 then D (4) = D4_G);
+ pragma Assert
+ (By
+ (D'Initialized,
+ D (1)'Initialized and D (2)'Initialized
+ and D (3)'Initialized and D (4)'Initialized));
+ pragma Assert
+ (Big3 (D (J), D (J + 1), D (J + 2)) =
+ (if J = 1 then D123 else D234)
+ - Big3 (S1, S2, S3));
+ end;
+
+ pragma Assert
+ (Big3 (D (J), D (J + 1), D (J + 2)) < Big (Zu));
- pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) < Big (Zu));
if D (J) > 0 then
Lemma_Double_Big_2xxSingle;
pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) =
@@ -3222,6 +3298,17 @@ is
end if;
end loop;
+
+ pragma Assert_And_Cut
+ (Qd (1)'Initialized and then Qd (2)'Initialized
+ and then D'Initialized
+ and then Big_2xxSingle * Big (Double_Uns (D (3)))
+ + Big (Double_Uns (D (4))) < Big (Zu)
+ and then Mult * Big_2xx (Scale) =
+ Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
+ + Big (Double_Uns (Qd (2))) * Big (Zu)
+ + Big_2xxSingle * Big (Double_Uns (D (3)))
+ + Big (Double_Uns (D (4))));
end;
-- The two quotient digits are now set, and the remainder of the
@@ -3231,16 +3318,9 @@ is
-- We rescale the divisor as well, to make the proper comparison
-- for rounding below.
- pragma Assert (for all K in 1 .. 2 => Qd (K)'Initialized);
Qu := Qd (1) & Qd (2);
Ru := D (3) & D (4);
- pragma Assert
- (Mult * Big_2xx (Scale) =
- Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
- + Big (Double_Uns (Qd (2))) * Big (Zu)
- + Big_2xxSingle * Big (Double_Uns (D (3)))
- + Big (Double_Uns (D (4))));
Lemma_Hi_Lo (Qu, Qd (1), Qd (2));
Lemma_Hi_Lo (Ru, D (3), D (4));
Lemma_Substitution
diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb
index 221ef1e635eb..0f4ce236cdf8 100644
--- a/gcc/ada/libgnat/s-arit32.adb
+++ b/gcc/ada/libgnat/s-arit32.adb
@@ -119,7 +119,9 @@ is
-- 0 .. 2**31 - 1, then the corresponding nonnegative signed integer is
-- returned, otherwise constraint error is raised.
- procedure Raise_Error;
+ procedure Raise_Error with
+ Always_Terminates,
+ Exceptional_Cases => (Constraint_Error => True);
pragma No_Return (Raise_Error);
-- Raise constraint error with appropriate message
diff --git a/gcc/ada/libgnat/s-arit64.adb b/gcc/ada/libgnat/s-arit64.adb
index 62f7f42b3759..a60e0bbd6903 100644
--- a/gcc/ada/libgnat/s-arit64.adb
+++ b/gcc/ada/libgnat/s-arit64.adb
@@ -28,6 +28,7 @@
-- Extensive contributions were provided by Ada Core Technologies Inc. --
-- --
------------------------------------------------------------------------------
+pragma Assertion_Policy (Ghost => Ignore);
with System.Arith_Double;
@@ -51,6 +52,9 @@ is
function Multiply_With_Ovflo_Check64 (X, Y : Int64) return Int64
renames Impl.Multiply_With_Ovflo_Check;
+ function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer
+ renames Impl.Round_Quotient;
+
procedure Scaled_Divide64
(X, Y, Z : Int64;
Q, R : out Int64;
diff --git a/gcc/ada/libgnat/s-arit64.ads b/gcc/ada/libgnat/s-arit64.ads
index efc1f5f877fe..09ac7dd78e51 100644
--- a/gcc/ada/libgnat/s-arit64.ads
+++ b/gcc/ada/libgnat/s-arit64.ads
@@ -125,15 +125,15 @@ is
or else (X < Big (Int64'(0))) = (Y < Big (Int64'(0))))
with Ghost;
- function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer is
- (if abs R > (abs Y - Big (Int64'(1))) / Big (Int64'(2)) then
- (if Same_Sign (X, Y) then Q + Big (Int64'(1))
- else Q - Big (Int64'(1)))
- else
- Q)
- with
+ function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer with
Ghost,
- Pre => Y /= 0 and then Q = X / Y and then R = X rem Y;
+ Pre => Y /= 0 and then Q = X / Y and then R = X rem Y,
+ Post => Round_Quotient'Result =
+ (if abs R > (abs Y - Big (Int64'(1))) / Big (Int64'(2)) then
+ (if Same_Sign (X, Y) then Q + Big (Int64'(1))
+ else Q - Big (Int64'(1)))
+ else
+ Q);
procedure Scaled_Divide64
(X, Y, Z : Int64;
diff --git a/gcc/ada/libgnat/s-expmod.adb b/gcc/ada/libgnat/s-expmod.adb
index c991bb787812..932050d463f9 100644
--- a/gcc/ada/libgnat/s-expmod.adb
+++ b/gcc/ada/libgnat/s-expmod.adb
@@ -149,14 +149,24 @@ is
----------------------
procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) is
+
+ procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) with
+ Pre => Natural'Last - Exp_2 >= Exp_1,
+ Post => A ** (Exp_1 + Exp_2) = A ** (Exp_1) * A ** (Exp_2);
+
+ ----------------------------
+ -- Lemma_Exp_Distribution --
+ ----------------------------
+
+ procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) is null;
+
begin
if Exp rem 2 = 0 then
pragma Assert (Exp = Exp / 2 + Exp / 2);
else
pragma Assert (Exp = Exp / 2 + Exp / 2 + 1);
- pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2 + 1));
- pragma Assert (A ** (Exp / 2 + 1) = A ** (Exp / 2) * A);
- pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
+ Lemma_Exp_Distribution (Exp / 2, Exp / 2 + 1);
+ Lemma_Exp_Distribution (Exp / 2, 1);
end if;
end Lemma_Exp_Expand;
@@ -253,7 +263,10 @@ is
Post => Big (Mult (X, Y)) = (Big (X) * Big (Y)) mod M
and then Big (Mult (X, Y)) < M;
- procedure Lemma_Mult (X, Y : Unsigned) is null;
+ procedure Lemma_Mult (X, Y : Unsigned) is
+ begin
+ pragma Assert (Big (Mult (X, Y)) = (Big (X) * Big (Y)) mod M);
+ end Lemma_Mult;
Rest : Big_Integer with Ghost;
-- Ghost variable to hold Factor**Exp between Exp and Factor updates
diff --git a/gcc/ada/libgnat/s-exponn.adb b/gcc/ada/libgnat/s-exponn.adb
index 8a80532b96f1..29db1dbd544d 100644
--- a/gcc/ada/libgnat/s-exponn.adb
+++ b/gcc/ada/libgnat/s-exponn.adb
@@ -185,14 +185,24 @@ is
----------------------
procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) is
+
+ procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) with
+ Pre => A /= 0 and then Natural'Last - Exp_2 >= Exp_1,
+ Post => A ** (Exp_1 + Exp_2) = A ** (Exp_1) * A ** (Exp_2);
+
+ ----------------------------
+ -- Lemma_Exp_Distribution --
+ ----------------------------
+
+ procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) is null;
+
begin
if Exp rem 2 = 0 then
pragma Assert (Exp = Exp / 2 + Exp / 2);
else
pragma Assert (Exp = Exp / 2 + Exp / 2 + 1);
- pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2 + 1));
- pragma Assert (A ** (Exp / 2 + 1) = A ** (Exp / 2) * A);
- pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
+ Lemma_Exp_Distribution (Exp / 2, Exp / 2 + 1);
+ Lemma_Exp_Distribution (Exp / 2, 1);
end if;
end Lemma_Exp_Expand;
diff --git a/gcc/ada/libgnat/s-expont.adb b/gcc/ada/libgnat/s-expont.adb
index 264cb969de4e..fa56c68d8b48 100644
--- a/gcc/ada/libgnat/s-expont.adb
+++ b/gcc/ada/libgnat/s-expont.adb
@@ -185,14 +185,24 @@ is
----------------------
procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) is
+
+ procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) with
+ Pre => A /= 0 and then Natural'Last - Exp_2 >= Exp_1,
+ Post => A ** (Exp_1 + Exp_2) = A ** (Exp_1) * A ** (Exp_2);
+
+ ----------------------------
+ -- Lemma_Exp_Distribution --
+ ----------------------------
+
+ procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) is null;
+
begin
if Exp rem 2 = 0 then
pragma Assert (Exp = Exp / 2 + Exp / 2);
else
pragma Assert (Exp = Exp / 2 + Exp / 2 + 1);
- pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2 + 1));
- pragma Assert (A ** (Exp / 2 + 1) = A ** (Exp / 2) * A);
- pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
+ Lemma_Exp_Distribution (Exp / 2, Exp / 2 + 1);
+ Lemma_Exp_Distribution (Exp / 2, 1);
end if;
end Lemma_Exp_Expand;
diff --git a/gcc/ada/libgnat/s-imgboo.adb b/gcc/ada/libgnat/s-imgboo.adb
index 1d1ec722079d..cd66a0f447df 100644
--- a/gcc/ada/libgnat/s-imgboo.adb
+++ b/gcc/ada/libgnat/s-imgboo.adb
@@ -41,6 +41,20 @@ package body System.Img_Bool
with SPARK_Mode
is
+ -- Local lemmas
+
+ procedure Lemma_Is_First_Non_Space_Ghost (S : String; R : Positive) with
+ Ghost,
+ Pre => R in S'Range and then S (R) /= ' '
+ and then System.Val_Spec.Only_Space_Ghost (S, S'First, R - 1),
+ Post => System.Val_Spec.First_Non_Space_Ghost (S, S'First, S'Last) = R;
+
+ ------------------------------------
+ -- Lemma_Is_First_Non_Space_Ghost --
+ ------------------------------------
+
+ procedure Lemma_Is_First_Non_Space_Ghost (S : String; R : Positive) is null;
+
-------------------
-- Image_Boolean --
-------------------
@@ -55,13 +69,11 @@ is
if V then
S (1 .. 4) := "TRUE";
P := 4;
- pragma Assert
- (System.Val_Spec.First_Non_Space_Ghost (S, S'First, S'Last) = 1);
+ Lemma_Is_First_Non_Space_Ghost (S, 1);
else
S (1 .. 5) := "FALSE";
P := 5;
- pragma Assert
- (System.Val_Spec.First_Non_Space_Ghost (S, S'First, S'Last) = 1);
+ Lemma_Is_First_Non_Space_Ghost (S, 1);
end if;
end Image_Boolean;
diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads
index cc804f4be550..6f91c363a43d 100644
--- a/gcc/ada/libgnat/s-valuti.ads
+++ b/gcc/ada/libgnat/s-valuti.ads
@@ -54,6 +54,7 @@ is
procedure Bad_Value (S : String)
with
+ Always_Terminates,
Depends => (null => S),
Exceptional_Cases => (others => Standard.False);
pragma No_Return (Bad_Value);
