diff mbox series

[Ada] Fix lemma in generic unit System.Arith_Double

Message ID 20220105113323.GA2712524@adacore.com
State New
Headers show
Series [Ada] Fix lemma in generic unit System.Arith_Double | expand

Commit Message

Pierre-Marie de Rodat Jan. 5, 2022, 11:33 a.m. UTC 
This system unit is instanciated with values of Single_Size either 32
or 64 currently. A lemma was only valid for value of 32, which became
visible when proving the instance with value of 64.

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

gcc/ada/

	* libgnat/s-aridou.adb (Lemma_Word_Commutation): Fix for
	instances with other values of Single_Size.
diff mbox series

Patch

diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -541,7 +541,8 @@  is
    procedure Lemma_Word_Commutation (X : Single_Uns)
    with
      Ghost,
-     Post => Big_2xx32 * Big (Double_Uns (X)) = Big (2**32 * Double_Uns (X));
+     Post => Big_2xx32 * Big (Double_Uns (X))
+       = Big (2**Single_Size * Double_Uns (X));
 
    -----------------------------
    -- Local lemma null bodies --