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

Reply via email to