From: Aleksandra Pasek <pasek@adacore.com>
Date: Mon, 3 Feb 2025 16:29:21 +0000 (+0000)
Subject: ada: Add missing Ghost aspect to Lemma_Not_In_Range_Big2xx64 in s-aridou.adb
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=d57eddd9b211d4f7ded33e59f173bb2694afb835;p=thirdparty%2Fgcc.git

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 --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);