diff options
| author | Yannick Moy <moy@adacore.com> | 2021-11-29 16:15:32 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-01-05 11:32:34 +0000 |
| commit | 50d8b1066a46cc134c1accc270c9be1b1cae8bc2 (patch) | |
| tree | fc4782859f911c411db2f6973365699f071414cf /gcc | |
| parent | acdf2f079b3dcc053129b973fc3e94c596589286 (diff) | |
| download | gcc-50d8b1066a46cc134c1accc270c9be1b1cae8bc2.zip gcc-50d8b1066a46cc134c1accc270c9be1b1cae8bc2.tar.gz gcc-50d8b1066a46cc134c1accc270c9be1b1cae8bc2.tar.bz2 | |
[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.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/libgnat/s-aridou.adb | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 0a75f08..57d427b 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 -- |