diff mbox series

[Ada] Fix proof of runtime units

Message ID 20220518084317.GA3341771@adacore.com
State Committed
Commit 3c63f73051458b24298eb82ddd109bbc6a453464
Headers
Series [Ada] Fix proof of runtime units |

Commit Message

Pierre-Marie de Rodat May 18, 2022, 8:43 a.m. UTC 
  Update to latest version of Why3 caused some proof regressions.
Fix the proof by changing ghost code.

Tested on x86_64-pc-linux-gnu, committed on trunk

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 mbox series

Patch

diff --git a/gcc/ada/libgnat/s-imagei.adb b/gcc/ada/libgnat/s-imagei.adb
--- 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
--- 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
--- 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)));