Proof of generic units for Long_Long_Long_Unsigned instantiations is
harder for provers, as they have to deal with larger values. Add ghost
code to make the proof easier.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/s-imageu.adb (Set_Image_Unsigned): Add lemma.
* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Add assertion.
diff --git a/gcc/ada/libgnat/s-imageu.adb b/gcc/ada/libgnat/s-imageu.adb
--- a/gcc/ada/libgnat/s-imageu.adb
+++ b/gcc/ada/libgnat/s-imageu.adb
@@ -210,6 +210,15 @@ package body System.Image_U is
-- Ghost lemma to prove the value of a character corresponding to the
-- next figure.
+ procedure Prove_Euclidian (Val, Quot, Rest : Uns)
+ with
+ Ghost,
+ Pre => Quot = Val / 10
+ and then Rest = Val rem 10,
+ Post => Val = 10 * Quot + Rest;
+ -- Ghost lemma to prove the relation between the quotient/remainder of
+ -- division by 10 and the initial value.
+
procedure Prove_Hexa_To_Unsigned_Ghost (R : Uns)
with
Ghost,
@@ -256,6 +265,7 @@ package body System.Image_U is
-----------------------------
procedure Prove_Character_Val (R : Uns) is null;
+ procedure Prove_Euclidian (Val, Quot, Rest : Uns) is null;
procedure Prove_Hexa_To_Unsigned_Ghost (R : Uns) is null;
procedure Prove_Unchanged is null;
@@ -347,6 +357,9 @@ package body System.Image_U is
Acc => Value);
if J /= Nb_Digits then
+ Prove_Euclidian (Val => Prev_Value,
+ Quot => Value,
+ Rest => Hexa_To_Unsigned_Ghost (S (P + J)));
pragma Assert
(Prev_Value = 10 * Value + Hexa_To_Unsigned_Ghost (S (P + J)));
Prove_Iter_Scan
diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb
--- a/gcc/ada/libgnat/s-valueu.adb
+++ b/gcc/ada/libgnat/s-valueu.adb
@@ -590,6 +590,10 @@ package body System.Value_U is
if Str (P) = Base_Char then
Ptr.all := P + 1;
pragma Assert (Ptr.all = Last_Num_Based + 2);
+ pragma Assert
+ (if not Overflow then
+ Based_Val = Scan_Based_Number_Ghost
+ (Str, P, Last_Num_Based, Base, Uval));
Lemma_End_Of_Scan (Str, P, Last_Num_Based, Base, Uval);
pragma Assert (if not Overflow then Uval = Based_Val.Value);
exit;