diff options
| author | Claire Dross <dross@adacore.com> | 2022-05-18 15:22:39 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-06-02 09:06:43 +0000 |
| commit | 2b376b593570317195f99c65343a5856ae8c07eb (patch) | |
| tree | 8625a1abef732b0e2fbf95e048a618c7421ebd47 /gcc | |
| parent | 2a466ee093827650cd33fe877c1043441c4e9427 (diff) | |
| download | gcc-2b376b593570317195f99c65343a5856ae8c07eb.zip gcc-2b376b593570317195f99c65343a5856ae8c07eb.tar.gz gcc-2b376b593570317195f99c65343a5856ae8c07eb.tar.bz2 | |
[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.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/libgnat/s-aridou.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/libgnat/s-arit32.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/libgnat/s-spcuop.ads | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 259c0ac..880a899 100644 --- 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 3d500ac..6dac572 100644 --- 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 39a61c9..53db0ce 100644 --- 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 |