]> git.ipfire.org Git - thirdparty/gcc.git/commitdiff
ada: Add missing Ghost aspect to Lemma_Not_In_Range_Big2xx32 in s-arit32.adb
authorJohannes Kliemann <kliemann@adacore.com>
Tue, 28 Jan 2025 12:13:31 +0000 (12:13 +0000)
committerMarc Poulhiès <dkm@gcc.gnu.org>
Thu, 5 Jun 2025 08:18:36 +0000 (10:18 +0200)
gcc/ada/ChangeLog:

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

gcc/ada/libgnat/s-arit32.adb

index 91082e7692abb2b2ad3b4c03cb88502d8816069a..5172d1dba0e6f00bf7b45ad0c13b65b6c82ed362 100644 (file)
@@ -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);