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 --git a/gcc/ada/libgnat/g-crc32.ads b/gcc/ada/libgnat/g-crc32.ads
index d02b5ad15b764c56daa504e2aab3aaa9569ba9ec..568d65593c3a208949587ca50202a4c10754eed6 100644 (file)
--- 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 a0c92bc7f156a1313e9799c103b2c7e45f9c9ef6..94b0ce196e8d9dbfc4a12aaa8d20c054a4e210e0 100644 (file)
--- 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