[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 f340d139e26e8be8fb388d1af945a268290518a1..ff853d3ac6b851a19f7766c70dcb4cfa9d9c8985 100644 (file)
--- 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 221c0c6c87f38719666f574af311dabc55e7417e..eb2cc96a638d08d1d95f326a54be73bb09107bfc 100644 (file)
--- 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 461d957b1cb7bdf57dddef1b369e324d791157c8..b8bfd447237bb05cb262a7264f42d522a9d77931 100644 (file)
--- 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)));