[Ada] Add ghost code to facilitate proof with SPARK

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.

gcc/ada/

	* libgnat/s-imageu.adb (Set_Image_Unsigned): Add lemma.
	* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Add assertion.

1 files changed, 4 insertions, 0 deletions

diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb
index f1456a1..461d957 100644
--- 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;