From: Yannick Moy <moy@adacore.com>
Date: Mon, 29 Nov 2021 15:15:32 +0000 (+0100)
Subject: [Ada] Fix lemma in generic unit System.Arith_Double
X-Git-Tag: basepoints/gcc-13~2088
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=50d8b1066a46cc134c1accc270c9be1b1cae8bc2;p=thirdparty%2Fgcc.git

[Ada] Fix lemma in generic unit System.Arith_Double

gcc/ada/

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

diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index 0a75f08fcb98..57d427b147e5 100644
--- 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 --