[gcc r13-360] [Ada] Add ghost code to facilitate proof with SPARK

[gcc r13-360] [Ada] Add ghost code to facilitate proof with SPARK

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:86c7b1617f0ae0da828d1107795f57c96c848d8f

commit r13-360-g86c7b1617f0ae0da828d1107795f57c96c848d8f
Author: Yannick Moy <moy@adacore.com>
Date:   Thu Feb 10 11:54:44 2022 +0100

    [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:
---
 gcc/ada/libgnat/s-imageu.adb | 13 +++++++++++++
 gcc/ada/libgnat/s-valueu.adb |  4 ++++
 2 files changed, 17 insertions(+)

diff --git a/gcc/ada/libgnat/s-imageu.adb b/gcc/ada/libgnat/s-imageu.adb
index 87830dff740..d6d9d466091 100644
--- 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 f1456a1a5ca..461d957b1cb 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;