[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.

diff --git a/gcc/ada/libgnat/s-imageu.adb b/gcc/ada/libgnat/s-imageu.adb
index 87830dff74052825cd25a57e5db864cbce7242d3..d6d9d466091c492856aa919b201a96655c1824c5 100644 (file)
--- 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
index f1456a1a5ca42b550b2d107481410324c67b9303..461d957b1cb7bdf57dddef1b369e324d791157c8 100644 (file)
--- 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;