mirrors/gcc
1
0
Fork 0
mirror of https://gcc.gnu.org/git/gcc.git synced 2024-11-25 03:44:04 +08:00
Code Issues Actions Packages Projects Releases Wiki Activity

[Ada] Rename GNATprove annotate pragma for termination to Always_Return

Browse Source 
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.
This commit is contained in:
Claire Dross 2022-05-18 15:22:39 +02:00 committed by Pierre-Marie de Rodat
parent 2a466ee093
commit 2b376b5935
3 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
gcc/ada/libgnat/s-aridou.adb
View File

@ -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

4
gcc/ada/libgnat/s-arit32.adb
View File

@ -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

2
gcc/ada/libgnat/s-spcuop.ads
View File

@ -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