From: Yannick Moy <moy@adacore.com>
Date: Mon, 4 Apr 2022 15:38:57 +0000 (+0200)
Subject: [Ada] Fix proof of runtime units
X-Git-Tag: basepoints/gcc-14~6608
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=3c63f73051458b24298eb82ddd109bbc6a453464;p=thirdparty%2Fgcc.git

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