From: Aleksandra Pasek <pa...@adacore.com> gcc/ada/ChangeLog:
* libgnat/s-aridou.adb: Add missing Ghost aspect to Lemma_Not_In_Range_Big2xx64. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/s-aridou.adb | 1 + 1 file changed, 1 insertion(+) diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index e4140e83779..e3f83ca2aca 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -508,6 +508,7 @@ is procedure Lemma_Not_In_Range_Big2xx64 with + Ghost, Post => not In_Double_Int_Range (Big_2xxDouble) and then not In_Double_Int_Range (-Big_2xxDouble); -- 2.43.0