[gcc r13-599] [Ada] Fix proof of runtime units

[Pierre-Marie de Rodat <pmderodat@gcc.gnu.org>]

https://gcc.gnu.org/g:3c63f73051458b24298eb82ddd109bbc6a453464

commit r13-599-g3c63f73051458b24298eb82ddd109bbc6a453464
Author: Yannick Moy <moy@adacore.com>
Date:   Mon Apr 4 17:38:57 2022 +0200

    [Ada] Fix proof of runtime units
    
    Update to latest version of Why3 caused some proof regressions.
    Fix the proof by changing ghost code.
    
    gcc/ada/
    
            * libgnat/s-imagei.adb (Set_Digits): Add assertion.
            * libgnat/s-imgboo.adb (Image_Boolean): Add assertions.
            * libgnat/s-valueu.adb (Scan_Raw_Unsigned): Add assertion.

Diff:
---
 gcc/ada/libgnat/s-imagei.adb | 2 ++
 gcc/ada/libgnat/s-imgboo.adb | 6 ++++++
 gcc/ada/libgnat/s-valueu.adb | 1 +
 3 files changed, 9 insertions(+)

diff --git a/gcc/ada/libgnat/s-imagei.adb b/gcc/ada/libgnat/s-imagei.adb
index f340d139e26..ff853d3ac6b 100644
--- a/gcc/ada/libgnat/s-imagei.adb
+++ b/gcc/ada/libgnat/s-imagei.adb
@@ -388,6 +388,8 @@ package body System.Image_I is
          Prove_Uns_Of_Non_Positive_Value;
          pragma Assert (Uns_Value rem 10 = Uns_Of_Non_Positive (Value rem 10));
          pragma Assert (Uns_Value rem 10 = Uns (-(Value rem 10)));
+         pragma Assert
+           (Uns_Value = From_Big (Big (Uns_T) / Big_10 ** (Nb_Digits - J)));
 
          Prev_Value := Uns_Value;
          Prev_S := S;
diff --git a/gcc/ada/libgnat/s-imgboo.adb b/gcc/ada/libgnat/s-imgboo.adb
index 221c0c6c87f..eb2cc96a638 100644
--- a/gcc/ada/libgnat/s-imgboo.adb
+++ b/gcc/ada/libgnat/s-imgboo.adb
@@ -37,6 +37,8 @@ pragma Assertion_Policy (Ghost          => Ignore,
                          Loop_Invariant => Ignore,
                          Assert         => Ignore);
 
+with System.Val_Util;
+
 package body System.Img_Bool
   with SPARK_Mode
 is
@@ -55,9 +57,13 @@ is
       if V then
          S (1 .. 4) := "TRUE";
          P := 4;
+         pragma Assert
+           (System.Val_Util.First_Non_Space_Ghost (S, S'First, S'Last) = 1);
       else
          S (1 .. 5) := "FALSE";
          P := 5;
+         pragma Assert
+           (System.Val_Util.First_Non_Space_Ghost (S, S'First, S'Last) = 1);
       end if;
    end Image_Boolean;
 
diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb
index 461d957b1cb..b8bfd447237 100644
--- a/gcc/ada/libgnat/s-valueu.adb
+++ b/gcc/ada/libgnat/s-valueu.adb
@@ -645,6 +645,7 @@ package body System.Value_U is
 
       Scan_Exponent (Str, Ptr, Max, Expon);
 
+      pragma Assert (Ptr.all = Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max));
       pragma Assert
         (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max))
          then Expon = Scan_Exponent_Ghost (Str (First_Exp .. Max)));