https://gcc.gnu.org/g:d4325877f35c8984680319c76af8274dd35c40fb

commit r16-1151-gd4325877f35c8984680319c76af8274dd35c40fb
Author: Johannes Kliemann <kliem...@adacore.com>
Date:   Tue Jan 28 12:13:31 2025 +0000

    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:
---
 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 91082e7692ab..5172d1dba0e6 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);

Reply via email to