From 50d8b1066a46cc134c1accc270c9be1b1cae8bc2 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 29 Nov 2021 16:15:32 +0100 Subject: [PATCH] [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. --- gcc/ada/libgnat/s-aridou.adb | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- -- 2.47.2