https://gcc.gnu.org/g:4980b619fc2ce7f0acfc72a44f6af39cf922ffc0
commit r16-5231-g4980b619fc2ce7f0acfc72a44f6af39cf922ffc0 Author: Piotr Trojanek <[email protected]> Date: Thu Aug 7 16:11:09 2025 +0200 ada: Annotate CRC32 runtime packages as Pure and Always_Terminates Packages that implement CRC32 algorithm are pure and always terminate. This avoids spurious warnings when using them from GNATprove. gcc/ada/ChangeLog: * libgnat/g-crc32.ads (CRC32): Annotate as pure and always terminating. * libgnat/s-crc32.ads (CRC32): Annotate as pure and always terminating. Diff: --- gcc/ada/libgnat/g-crc32.ads | 2 +- gcc/ada/libgnat/s-crc32.ads | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/gcc/ada/libgnat/g-crc32.ads b/gcc/ada/libgnat/g-crc32.ads index d02b5ad15b76..568d65593c3a 100644 --- a/gcc/ada/libgnat/g-crc32.ads +++ b/gcc/ada/libgnat/g-crc32.ads @@ -58,7 +58,7 @@ with Ada.Streams; with Interfaces; with System.CRC32; -package GNAT.CRC32 is +package GNAT.CRC32 with Pure, Always_Terminates is subtype CRC32 is System.CRC32.CRC32; -- Used to represent CRC32 values, which are 32 bit bit-strings diff --git a/gcc/ada/libgnat/s-crc32.ads b/gcc/ada/libgnat/s-crc32.ads index a0c92bc7f156..94b0ce196e8d 100644 --- a/gcc/ada/libgnat/s-crc32.ads +++ b/gcc/ada/libgnat/s-crc32.ads @@ -56,7 +56,7 @@ with Interfaces; -package System.CRC32 is +package System.CRC32 with Pure, Always_Terminates is type CRC32 is new Interfaces.Unsigned_32; -- Used to represent CRC32 values, which are 32 bit bit-strings
