From: Johannes Kliemann <kliemann@adacore.com>
Date: Tue, 28 Jan 2025 12:13:31 +0000 (+0000)
Subject: ada: Add missing Ghost aspect to Lemma_Not_In_Range_Big2xx32 in s-arit32.adb
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=d4325877f35c8984680319c76af8274dd35c40fb;p=thirdparty%2Fgcc.git

ada: Add missing Ghost aspect to Lemma_Not_In_Range_Big2xx32 in s-arit32.adb

gcc/ada/ChangeLog:

	* libgnat/s-arit32.adb (Lemma_Not_In_Range_Big2xx32): Add missing
	Ghost aspect.
---

diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb
index 91082e7692a..5172d1dba0e 100644
--- a/gcc/ada/libgnat/s-arit32.adb
+++ b/gcc/ada/libgnat/s-arit32.adb
@@ -203,6 +203,7 @@ is
 
    procedure Lemma_Not_In_Range_Big2xx32
    with
+     Ghost,
      Post => not In_Int32_Range (Big_2xx32)
        and then not In_Int32_Range (-Big_2xx32);