From: Yannick Moy <moy@adacore.com>
Date: Thu, 10 Feb 2022 10:54:44 +0000 (+0100)
Subject: [Ada] Add ghost code to facilitate proof with SPARK
X-Git-Tag: basepoints/gcc-14~6847
X-Git-Url: http://git.ipfire.org/?a=commitdiff_plain;h=86c7b1617f0ae0da828d1107795f57c96c848d8f;p=thirdparty%2Fgcc.git

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