[Ada] Rename GNATprove annotate pragma for termination to Always_Return

GNATprove changed the name of the pragma Annotate used to verify that
a subprogram always returns normally. It is now called Always_Return
instead of Terminating.

gcc/ada/

	* libgnat/s-aridou.adb: Use Always_Return instead of Terminating
	to annotate termination for GNATprove.
	* libgnat/s-arit32.adb: Idem.
	* libgnat/s-spcuop.ads: Idem.

diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index 259c0ac0da208b0f6583455e0e696b9dc439bc6c..880a8995d5c968af772eca5f417e639e13ea931c 100644 (file)
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -162,7 +162,7 @@ is
 
    function To_Neg_Int (A : Double_Uns) return Double_Int
    with
-     Annotate => (GNATprove, Terminating),
+     Annotate => (GNATprove, Always_Return),
      Pre      => In_Double_Int_Range (-Big (A)),
      Post     => Big (To_Neg_Int'Result) = -Big (A);
    --  Convert to negative integer equivalent. If the input is in the range
@@ -172,7 +172,7 @@ is
 
    function To_Pos_Int (A : Double_Uns) return Double_Int
    with
-     Annotate => (GNATprove, Terminating),
+     Annotate => (GNATprove, Always_Return),
      Pre      => In_Double_Int_Range (Big (A)),
      Post     => Big (To_Pos_Int'Result) = Big (A);
    --  Convert to positive integer equivalent. If the input is in the range

diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb
index 3d500ac8fad157052ef57a865f0a7b314db99594..6dac5725a59e4bca7948c3d33bb40138d9b53756 100644 (file)
--- a/gcc/ada/libgnat/s-arit32.adb
+++ b/gcc/ada/libgnat/s-arit32.adb
@@ -104,7 +104,7 @@ is
 
    function To_Neg_Int (A : Uns32) return Int32
    with
-     Annotate => (GNATprove, Terminating),
+     Annotate => (GNATprove, Always_Return),
      Pre      => In_Int32_Range (-Big (A)),
      Post     => Big (To_Neg_Int'Result) = -Big (A);
    --  Convert to negative integer equivalent. If the input is in the range
@@ -114,7 +114,7 @@ is
 
    function To_Pos_Int (A : Uns32) return Int32
    with
-     Annotate => (GNATprove, Terminating),
+     Annotate => (GNATprove, Always_Return),
      Pre      => In_Int32_Range (Big (A)),
      Post     => Big (To_Pos_Int'Result) = Big (A);
    --  Convert to positive integer equivalent. If the input is in the range

diff --git a/gcc/ada/libgnat/s-spcuop.ads b/gcc/ada/libgnat/s-spcuop.ads
index 39a61c96af136368602d7489a245e98ed9c3fded..53db0ce381214e731bc4424fc680d0739a36e16f 100644 (file)
--- a/gcc/ada/libgnat/s-spcuop.ads
+++ b/gcc/ada/libgnat/s-spcuop.ads
@@ -45,7 +45,7 @@
 package System.SPARK.Cut_Operations with
   SPARK_Mode,
   Pure,
-  Annotate => (GNATprove, Terminating)
+  Annotate => (GNATprove, Always_Return)
 is
 
    function By (Consequence, Premise : Boolean) return Boolean with