[gcc r16-1154] ada: Add missing Ghost aspect to Lemma_Not_In_Range_Big2xx64 in s-aridou.adb
Marc Poulhies
dkm@gcc.gnu.org
Thu Jun 5 08:22:04 GMT 2025
https://gcc.gnu.org/g:d57eddd9b211d4f7ded33e59f173bb2694afb835
commit r16-1154-gd57eddd9b211d4f7ded33e59f173bb2694afb835
Author: Aleksandra Pasek <pasek@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);
More information about the Gcc-cvs
mailing list