From d4325877f35c8984680319c76af8274dd35c40fb Mon Sep 17 00:00:00 2001 From: Johannes Kliemann Date: Tue, 28 Jan 2025 12:13:31 +0000 Subject: [PATCH] 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. --- gcc/ada/libgnat/s-arit32.adb | 1 + 1 file changed, 1 insertion(+) 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); -- 2.47.2