OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Fix lemma in generic unit System.Arith_Double

Browse Source 
gcc/ada/

	* libgnat/s-aridou.adb (Lemma_Word_Commutation): Fix for
	instances with other values of Single_Size.
This commit is contained in:
Yannick Moy 2021-11-29 16:15:32 +01:00 committed by Pierre-Marie de Rodat
parent acdf2f079b
commit 50d8b1066a
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
gcc/ada/libgnat/s-aridou.adb
View File

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