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