[gcc r16-1154] ada: Add missing Ghost aspect to Lemma_Not_In_Range_Big2xx64 in s-aridou.adb

[Marc Poulhies via Gcc-cvs]

https://gcc.gnu.org/g:d57eddd9b211d4f7ded33e59f173bb2694afb835

commit r16-1154-gd57eddd9b211d4f7ded33e59f173bb2694afb835
Author: Aleksandra Pasek <pa...@adacore.com>
Date:   Mon Feb 3 16:29:21 2025 +0000

    ada: Add missing Ghost aspect to Lemma_Not_In_Range_Big2xx64 in s-aridou.adb
    
    gcc/ada/ChangeLog:
    
            * libgnat/s-aridou.adb: Add missing Ghost aspect to
            Lemma_Not_In_Range_Big2xx64.

Diff:
---
 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 e4140e837799..e3f83ca2aca0 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);