From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 7871) id ECE3E3858C20; Tue, 20 Jun 2023 07:45:55 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org ECE3E3858C20 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1687247155; bh=gzN6pVIgPlPY9Mr32R4B0fAFdkL8VuzESq5pgdl58VM=; h=From:To:Subject:Date:From; b=De6nhsG0TviWwNHyhwvmaDMGHd+GLKIff63nGF6s1e4Ja2SHV0K8eiwuIy6bWLxK8 W8KaH98QExRXymeZnsmaJcLBQmvOv3VAzjHSOFpzcPzHmjL4bXFLU2fVQuOWagehUX 85aRK93nm9LuWZ6129nQOYDMWXW0mHB8g06rtX+k= MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Marc Poulhi?s To: gcc-cvs@gcc.gnu.org Subject: [gcc r14-1962] ada: Remove references to Might_Not_Return and Always_Return X-Act-Checkin: gcc X-Git-Author: Claire Dross X-Git-Refname: refs/heads/master X-Git-Oldrev: 862f84b4a36d6c569968d20949f54e2f427179c1 X-Git-Newrev: b1c3d01619e06e7ef49097925b81307f422ec78a Message-Id: <20230620074555.ECE3E3858C20@sourceware.org> Date: Tue, 20 Jun 2023 07:45:55 +0000 (GMT) List-Id: https://gcc.gnu.org/g:b1c3d01619e06e7ef49097925b81307f422ec78a commit r14-1962-gb1c3d01619e06e7ef49097925b81307f422ec78a Author: Claire Dross Date: Thu Mar 30 11:09:33 2023 +0200 ada: Remove references to Might_Not_Return and Always_Return The Might_Not_Return and Always_Return annotations for GNATprove should now be replaced by the two more precise aspects Exceptional_Cases and Always_Terminates. They allow to specify whether a subprogram is allowed to raise exceptions or fail to complete. gcc/ada/ * libgnat/a-strfix.ads: Replace Might_Not_Return annotations by Exceptional_Cases and Always_Terminates aspects. * libgnat/a-tideio.ads: Idem. * libgnat/a-tienio.ads: Idem. * libgnat/a-tifiio.ads: Idem. * libgnat/a-tiflio.ads: Idem. * libgnat/a-tiinio.ads: Idem. * libgnat/a-timoio.ads: Idem. * libgnat/a-textio.ads: Idem. Also mark functions Name, Col, Line, and Page as out of SPARK as they might raise Layout_Error. * libgnarl/a-reatim.ads: Replace Always_Return annotations by Always_Terminates aspects. * libgnat/a-chahan.ads: Idem. * libgnat/a-nbnbig.ads: Idem. * libgnat/a-nbnbin.ads: Idem. * libgnat/a-nbnbre.ads: Idem. * libgnat/a-ngelfu.ads: Idem. * libgnat/a-nlelfu.ads: Idem. * libgnat/a-nllefu.ads: Idem. * libgnat/a-nselfu.ads: Idem. * libgnat/a-nuelfu.ads: Idem. * libgnat/a-strbou.ads: Idem. * libgnat/a-strmap.ads: Idem. * libgnat/a-strsea.ads: Idem. * libgnat/a-strsup.ads: Idem. * libgnat/a-strunb.ads: Idem. * libgnat/a-strunb__shared.ads: Idem. * libgnat/g-souinf.ads: Idem. * libgnat/i-c.ads: Idem. * libgnat/interfac.ads: Idem. * libgnat/interfac__2020.ads: Idem. * libgnat/s-aridou.adb: Idem. * libgnat/s-arit32.adb: Idem. * libgnat/s-atacco.ads: Idem. * libgnat/s-spcuop.ads: Idem. * libgnat/s-stoele.ads: Idem. * libgnat/s-vaispe.ads: Idem. * libgnat/s-vauspe.ads: Idem. * libgnat/i-cstrin.ads: Add a precondition instead of a Might_Not_Return annotation. Diff: --- gcc/ada/libgnarl/a-reatim.ads | 4 +- gcc/ada/libgnat/a-chahan.ads | 7 +- gcc/ada/libgnat/a-nbnbig.ads | 4 +- gcc/ada/libgnat/a-nbnbin.ads | 6 +- gcc/ada/libgnat/a-nbnbre.ads | 6 +- gcc/ada/libgnat/a-ngelfu.ads | 4 +- gcc/ada/libgnat/a-nlelfu.ads | 1 - gcc/ada/libgnat/a-nllefu.ads | 1 - gcc/ada/libgnat/a-nselfu.ads | 1 - gcc/ada/libgnat/a-nuelfu.ads | 1 - gcc/ada/libgnat/a-strbou.ads | 10 +- gcc/ada/libgnat/a-strfix.ads | 169 +++++++------------- gcc/ada/libgnat/a-strmap.ads | 7 +- gcc/ada/libgnat/a-strsea.ads | 6 +- gcc/ada/libgnat/a-strsup.ads | 6 +- gcc/ada/libgnat/a-strunb.ads | 4 +- gcc/ada/libgnat/a-strunb__shared.ads | 4 +- gcc/ada/libgnat/a-textio.ads | 300 +++++++++++++++++------------------ gcc/ada/libgnat/a-tideio.ads | 36 +++-- gcc/ada/libgnat/a-tienio.ads | 39 ++--- gcc/ada/libgnat/a-tifiio.ads | 39 ++--- gcc/ada/libgnat/a-tiflio.ads | 39 ++--- gcc/ada/libgnat/a-tiinio.ads | 38 ++--- gcc/ada/libgnat/a-timoio.ads | 38 ++--- gcc/ada/libgnat/g-souinf.ads | 2 +- gcc/ada/libgnat/i-c.ads | 7 +- gcc/ada/libgnat/i-cstrin.ads | 29 ++-- gcc/ada/libgnat/interfac.ads | 5 +- gcc/ada/libgnat/interfac__2020.ads | 5 +- gcc/ada/libgnat/s-aridou.adb | 10 +- gcc/ada/libgnat/s-arit32.adb | 10 +- gcc/ada/libgnat/s-atacco.ads | 6 +- gcc/ada/libgnat/s-spcuop.ads | 2 +- gcc/ada/libgnat/s-stoele.ads | 6 +- gcc/ada/libgnat/s-vaispe.ads | 2 +- gcc/ada/libgnat/s-vauspe.ads | 2 +- 36 files changed, 395 insertions(+), 461 deletions(-) diff --git a/gcc/ada/libgnarl/a-reatim.ads b/gcc/ada/libgnarl/a-reatim.ads index c5009d25cff..a616d579633 100644 --- a/gcc/ada/libgnarl/a-reatim.ads +++ b/gcc/ada/libgnarl/a-reatim.ads @@ -39,9 +39,9 @@ pragma Elaborate_All (System.Task_Primitives.Operations); package Ada.Real_Time with SPARK_Mode, Abstract_State => (Clock_Time with Synchronous), - Initializes => Clock_Time + Initializes => Clock_Time, + Always_Terminates is - pragma Annotate (GNATprove, Always_Return, Real_Time); pragma Compile_Time_Error (Duration'Size /= 64, diff --git a/gcc/ada/libgnat/a-chahan.ads b/gcc/ada/libgnat/a-chahan.ads index 159cd70218e..89b2d68ccc2 100644 --- a/gcc/ada/libgnat/a-chahan.ads +++ b/gcc/ada/libgnat/a-chahan.ads @@ -40,14 +40,13 @@ pragma Assertion_Policy (Post => Ignore); with Ada.Characters.Latin_1; -package Ada.Characters.Handling - with SPARK_Mode +package Ada.Characters.Handling with + SPARK_Mode, + Always_Terminates is pragma Pure; -- In accordance with Ada 2005 AI-362 - pragma Annotate (GNATprove, Always_Return, Handling); - ---------------------------------------- -- Character Classification Functions -- ---------------------------------------- diff --git a/gcc/ada/libgnat/a-nbnbig.ads b/gcc/ada/libgnat/a-nbnbig.ads index f83bf5276b3..382a7b60d18 100644 --- a/gcc/ada/libgnat/a-nbnbig.ads +++ b/gcc/ada/libgnat/a-nbnbig.ads @@ -30,9 +30,9 @@ pragma Assertion_Policy (Ghost => Ignore); package Ada.Numerics.Big_Numbers.Big_Integers_Ghost with SPARK_Mode, Ghost, - Pure + Pure, + Always_Terminates is - pragma Annotate (GNATprove, Always_Return, Big_Integers_Ghost); type Big_Integer is private with Integer_Literal => From_Universal_Image; diff --git a/gcc/ada/libgnat/a-nbnbin.ads b/gcc/ada/libgnat/a-nbnbin.ads index ffb96d4d98b..c4d74ee513b 100644 --- a/gcc/ada/libgnat/a-nbnbin.ads +++ b/gcc/ada/libgnat/a-nbnbin.ads @@ -18,10 +18,10 @@ with Ada.Strings.Text_Buffers; use Ada.Strings.Text_Buffers; private with Ada.Finalization; private with System; -package Ada.Numerics.Big_Numbers.Big_Integers - with Preelaborate +package Ada.Numerics.Big_Numbers.Big_Integers with + Preelaborate, + Always_Terminates is - pragma Annotate (GNATprove, Always_Return, Big_Integers); type Big_Integer is private with Integer_Literal => From_Universal_Image, diff --git a/gcc/ada/libgnat/a-nbnbre.ads b/gcc/ada/libgnat/a-nbnbre.ads index 350d0497ed4..d342eebd6b6 100644 --- a/gcc/ada/libgnat/a-nbnbre.ads +++ b/gcc/ada/libgnat/a-nbnbre.ads @@ -17,10 +17,10 @@ with Ada.Numerics.Big_Numbers.Big_Integers; with Ada.Strings.Text_Buffers; use Ada.Strings.Text_Buffers; -package Ada.Numerics.Big_Numbers.Big_Reals - with Preelaborate +package Ada.Numerics.Big_Numbers.Big_Reals with + Preelaborate, + Always_Terminates is - pragma Annotate (GNATprove, Always_Return, Big_Reals); type Big_Real is private with Real_Literal => From_Universal_Image, diff --git a/gcc/ada/libgnat/a-ngelfu.ads b/gcc/ada/libgnat/a-ngelfu.ads index f6d6c9643af..444d1a31724 100644 --- a/gcc/ada/libgnat/a-ngelfu.ads +++ b/gcc/ada/libgnat/a-ngelfu.ads @@ -37,10 +37,10 @@ generic type Float_Type is digits <>; package Ada.Numerics.Generic_Elementary_Functions with - SPARK_Mode => On + SPARK_Mode => On, + Always_Terminates is pragma Pure; - pragma Annotate (GNATprove, Always_Return, Generic_Elementary_Functions); -- Preconditions in this unit are meant for analysis only, not for run-time -- checking, so that the expected exceptions are raised when calling diff --git a/gcc/ada/libgnat/a-nlelfu.ads b/gcc/ada/libgnat/a-nlelfu.ads index b3afd1fc997..10b33e9cb3c 100644 --- a/gcc/ada/libgnat/a-nlelfu.ads +++ b/gcc/ada/libgnat/a-nlelfu.ads @@ -19,4 +19,3 @@ package Ada.Numerics.Long_Elementary_Functions is new Ada.Numerics.Generic_Elementary_Functions (Long_Float); pragma Pure (Long_Elementary_Functions); -pragma Annotate (GNATprove, Always_Return, Long_Elementary_Functions); diff --git a/gcc/ada/libgnat/a-nllefu.ads b/gcc/ada/libgnat/a-nllefu.ads index e137c67e786..7089fc3efb0 100644 --- a/gcc/ada/libgnat/a-nllefu.ads +++ b/gcc/ada/libgnat/a-nllefu.ads @@ -19,4 +19,3 @@ package Ada.Numerics.Long_Long_Elementary_Functions is new Ada.Numerics.Generic_Elementary_Functions (Long_Long_Float); pragma Pure (Long_Long_Elementary_Functions); -pragma Annotate (GNATprove, Always_Return, Long_Long_Elementary_Functions); diff --git a/gcc/ada/libgnat/a-nselfu.ads b/gcc/ada/libgnat/a-nselfu.ads index 6797efd70e9..10b04acdeb9 100644 --- a/gcc/ada/libgnat/a-nselfu.ads +++ b/gcc/ada/libgnat/a-nselfu.ads @@ -19,4 +19,3 @@ package Ada.Numerics.Short_Elementary_Functions is new Ada.Numerics.Generic_Elementary_Functions (Short_Float); pragma Pure (Short_Elementary_Functions); -pragma Annotate (GNATprove, Always_Return, Short_Elementary_Functions); diff --git a/gcc/ada/libgnat/a-nuelfu.ads b/gcc/ada/libgnat/a-nuelfu.ads index d4fe74572f6..149939babea 100644 --- a/gcc/ada/libgnat/a-nuelfu.ads +++ b/gcc/ada/libgnat/a-nuelfu.ads @@ -19,4 +19,3 @@ package Ada.Numerics.Elementary_Functions is new Ada.Numerics.Generic_Elementary_Functions (Float); pragma Pure (Elementary_Functions); -pragma Annotate (GNATprove, Always_Return, Elementary_Functions); diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads index 1e4a366c5fe..ea0cc3f7a51 100644 --- a/gcc/ada/libgnat/a-strbou.ads +++ b/gcc/ada/libgnat/a-strbou.ads @@ -47,9 +47,11 @@ with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; with Ada.Strings.Superbounded; with Ada.Strings.Search; -package Ada.Strings.Bounded with SPARK_Mode is +package Ada.Strings.Bounded with + SPARK_Mode, + Always_Terminates +is pragma Preelaborate; - pragma Annotate (GNATprove, Always_Return, Bounded); generic Max : Positive; @@ -57,7 +59,8 @@ package Ada.Strings.Bounded with SPARK_Mode is package Generic_Bounded_Length with SPARK_Mode, Initial_Condition => Length (Null_Bounded_String) = 0, - Abstract_State => null + Abstract_State => null, + Always_Terminates is -- Preconditions in this unit are meant for analysis only, not for -- run-time checking, so that the expected exceptions are raised. This @@ -69,7 +72,6 @@ package Ada.Strings.Bounded with SPARK_Mode is Post => Ignore, Contract_Cases => Ignore, Ghost => Ignore); - pragma Annotate (GNATprove, Always_Return, Generic_Bounded_Length); Max_Length : constant Positive := Max; diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads index 0838d59d5f7..9d5e9d92341 100644 --- a/gcc/ada/libgnat/a-strfix.ads +++ b/gcc/ada/libgnat/a-strfix.ads @@ -46,7 +46,10 @@ pragma Assertion_Policy (Pre => Ignore, with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; with Ada.Strings.Search; -package Ada.Strings.Fixed with SPARK_Mode is +package Ada.Strings.Fixed with + SPARK_Mode, + Always_Terminates +is pragma Preelaborate; -------------------------------------------------------------- @@ -60,11 +63,9 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => + (Length_Error => Target'Length'Old < Source'Length and Drop = Error); -- The Move procedure copies characters from Source to Target. If Source -- has the same length as Target, then the effect is to assign Source to -- Target. If Source is shorter than Target then: @@ -169,8 +170,7 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Index'Result = 0), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; pragma Ada_05 (Index); function Index @@ -233,8 +233,7 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Index'Result = 0), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; pragma Ada_05 (Index); -- Each Index function searches, starting from From, for a slice of @@ -303,8 +302,7 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Index'Result = 0), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; function Index (Source : String; @@ -359,8 +357,7 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Index'Result = 0), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- If Going = Forward, returns: -- @@ -413,8 +410,7 @@ package Ada.Strings.Fixed with SPARK_Mode is and then (J < Index'Result) = (Going = Forward) then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (J), Set)))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; function Index (Source : String; @@ -470,8 +466,7 @@ package Ada.Strings.Fixed with SPARK_Mode is or else (J > From) = (Going = Forward)) then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (J), Set)))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; pragma Ada_05 (Index); -- Index searches for the first or last occurrence of any of a set of -- characters (when Test=Inside), or any of the complement of a set of @@ -531,8 +526,7 @@ package Ada.Strings.Fixed with SPARK_Mode is and then (J = From or else (J > From) = (Going = Forward)) then Source (J) = ' '))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; pragma Ada_05 (Index_Non_Blank); -- Returns Index (Source, Maps.To_Set(Space), From, Outside, Going) @@ -570,8 +564,7 @@ package Ada.Strings.Fixed with SPARK_Mode is and then (J < Index_Non_Blank'Result) = (Going = Forward) then Source (J) = ' '))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns Index (Source, Maps.To_Set(Space), Outside, Going) function Count @@ -579,18 +572,16 @@ package Ada.Strings.Fixed with SPARK_Mode is Pattern : String; Mapping : Maps.Character_Mapping := Maps.Identity) return Natural with - Pre => Pattern'Length /= 0, - Global => null, - Annotate => (GNATprove, Always_Return); + Pre => Pattern'Length /= 0, + Global => null; function Count (Source : String; Pattern : String; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => Pattern'Length /= 0 and then Mapping /= null, - Global => null, - Annotate => (GNATprove, Always_Return); + Pre => Pattern'Length /= 0 and then Mapping /= null, + Global => null; -- Returns the maximum number of nonoverlapping slices of Source that match -- Pattern with respect to Mapping. If Pattern is the null string then @@ -600,8 +591,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : String; Set : Maps.Character_Set) return Natural with - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns the number of occurrences in Source of characters that are in -- Set. @@ -659,8 +649,7 @@ package Ada.Strings.Fixed with SPARK_Mode is then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; pragma Ada_2012 (Find_Token); -- If Source is not the null string and From is not in Source'Range, then -- Index_Error is raised. Otherwise, First is set to the index of the first @@ -722,8 +711,7 @@ package Ada.Strings.Fixed with SPARK_Mode is then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Equivalent to Find_Token (Source, Set, Source'First, Test, First, Last) ------------------------------------ @@ -752,8 +740,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (for all J in Source'Range => Translate'Result (J - Source'First + 1) = Mapping (Source (J))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; pragma Annotate (GNATprove, False_Positive, "call via access-to-subprogram", "function Mapping must always terminate"); @@ -779,8 +766,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (for all J in Source'Range => Translate'Result (J - Source'First + 1) = Ada.Strings.Maps.Value (Mapping, Source (J))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns the string S whose length is Source'Length and such that S (I) -- is the character to which Mapping maps the corresponding element of @@ -790,15 +776,14 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : in out String; Mapping : Maps.Character_Mapping_Function) with - Pre => Mapping /= null, - Post => + Pre => Mapping /= null, + Post => -- Each character in Source after the call is the translation of the -- character at the same position before the call, through Mapping. (for all J in Source'Range => Source (J) = Mapping (Source'Old (J))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; pragma Annotate (GNATprove, False_Positive, "call via access-to-subprogram", "function Mapping must always terminate"); @@ -807,15 +792,14 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : in out String; Mapping : Maps.Character_Mapping) with - Post => + Post => -- Each character in Source after the call is the translation of the -- character at the same position before the call, through Mapping. (for all J in Source'Range => Source (J) = Ada.Strings.Maps.Value (Mapping, Source'Old (J))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Equivalent to Source := Translate(Source, Mapping) @@ -908,8 +892,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (Low - Source'First + By'Length + 1 .. Replace_Slice'Result'Last) = Source (Low .. Source'Last))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- If Low > Source'Last + 1, or High < Source'First - 1, then Index_Error -- is propagated. Otherwise: -- @@ -929,7 +912,7 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - Pre => + Pre => Low - 1 <= Source'Last and then High >= Source'First - 1 and then (if High >= Low @@ -938,11 +921,8 @@ package Ada.Strings.Fixed with SPARK_Mode is - By'Length - Natural'Max (Source'Last - High, 0) else Source'Length <= Natural'Last - By'Length), - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Length_Error => Drop = Error); -- Equivalent to: -- -- Move (Replace_Slice (Source, Low, High, By), @@ -988,8 +968,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (Before - Source'First + New_Item'Length + 1 .. Insert'Result'Last) = Source (Before .. Source'Last)), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Propagates Index_Error if Before is not in -- Source'First .. Source'Last + 1; otherwise, returns -- Source (Source'First .. Before - 1) @@ -1001,14 +980,11 @@ package Ada.Strings.Fixed with SPARK_Mode is New_Item : String; Drop : Truncation := Error) with - Pre => + Pre => Before - 1 in Source'First - 1 .. Source'Last and then Source'Length <= Natural'Last - New_Item'Length, - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Length_Error => Drop = Error); -- Equivalent to Move (Insert (Source, Before, New_Item), Source, Drop) function Overwrite @@ -1057,8 +1033,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (Position - Source'First + New_Item'Length + 1 .. Overwrite'Result'Last) = Source (Position + New_Item'Length .. Source'Last)), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Propagates Index_Error if Position is not in -- Source'First .. Source'Last + 1; otherwise, returns the string obtained -- from Source by consecutively replacing characters starting at Position @@ -1072,16 +1047,13 @@ package Ada.Strings.Fixed with SPARK_Mode is New_Item : String; Drop : Truncation := Right) with - Pre => + Pre => Position - 1 in Source'First - 1 .. Source'Last and then (if Position - Source'First >= Source'Length - New_Item'Length then Position - Source'First <= Natural'Last - New_Item'Length), - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Length_Error => Drop = Error); -- Equivalent to Move(Overwrite(Source, Position, New_Item), Source, Drop) function Delete @@ -1129,8 +1101,7 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Delete'Result'Length = Source'Length and then Delete'Result = Source), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- If From <= Through, the returned string is -- Replace_Slice(Source, From, Through, ""); otherwise, it is Source with -- lower bound 1. @@ -1142,14 +1113,10 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - Pre => (if From <= Through + Pre => (if From <= Through then (From in Source'Range and then Through <= Source'Last)), - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null; -- Equivalent to: -- -- Move (Delete (Source, From, Through), @@ -1163,7 +1130,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : String; Side : Trim_End) return String with - Post => + Post => -- Lower bound of the returned string is 1 @@ -1188,8 +1155,7 @@ package Ada.Strings.Fixed with SPARK_Mode is else Index_Non_Blank (Source, Backward)); begin Trim'Result = Source (Low .. High))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns the string obtained by removing from Source all leading Space -- characters (if Side = Left), all trailing Space characters (if -- Side = Right), or all leading and trailing Space characters (if @@ -1201,11 +1167,7 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null; -- Equivalent to: -- -- Move (Trim (Source, Side), Source, Justify=>Justify, Pad=>Pad). @@ -1242,8 +1204,7 @@ package Ada.Strings.Fixed with SPARK_Mode is Index (Source, Right, Outside, Backward); begin Trim'Result = Source (Low .. High))), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns the string obtained by removing from Source all leading -- characters in Left and all trailing characters in Right. @@ -1254,11 +1215,7 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Strings.Left; Pad : Character := Space) with - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null; -- Equivalent to: -- -- Move (Trim (Source, Left, Right), @@ -1295,8 +1252,7 @@ package Ada.Strings.Fixed with SPARK_Mode is and then Head'Result (Source'Length + 1 .. Count) = [1 .. Count - Source'Length => Pad]), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns a string of length Count. If Count <= Source'Length, the string -- comprises the first Count characters of Source. Otherwise, its contents -- are Source concatenated with Count - Source'Length Pad characters. @@ -1307,11 +1263,8 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Length_Error => Count > Source'Length'Old); -- Equivalent to: -- -- Move (Head (Source, Count, Pad), @@ -1360,8 +1313,7 @@ package Ada.Strings.Fixed with SPARK_Mode is and then Tail'Result (Count - Source'Length + 1 .. Tail'Result'Last) = Source)), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- Returns a string of length Count. If Count <= Source'Length, the string -- comprises the last Count characters of Source. Otherwise, its contents -- are Count-Source'Length Pad characters concatenated with Source. @@ -1372,11 +1324,8 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - - -- Incomplete contract - - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Length_Error => Count > Source'Length'Old); -- Equivalent to: -- -- Move (Tail (Source, Count, Pad), @@ -1390,7 +1339,7 @@ package Ada.Strings.Fixed with SPARK_Mode is (Left : Natural; Right : Character) return String with - Post => + Post => -- Lower bound of the returned string is 1 @@ -1403,8 +1352,7 @@ package Ada.Strings.Fixed with SPARK_Mode is -- All characters of the returned string are Right and then (for all C of "*"'Result => C = Right), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; function "*" (Left : Natural; @@ -1427,8 +1375,7 @@ package Ada.Strings.Fixed with SPARK_Mode is and then (for all K in "*"'Result'Range => "*"'Result (K) = Right (Right'First + (K - 1) mod Right'Length)), - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; -- These functions replicate a character or string a specified number of -- times. The first function returns a string whose length is Left and each diff --git a/gcc/ada/libgnat/a-strmap.ads b/gcc/ada/libgnat/a-strmap.ads index 73dd3d92a18..a070da016b1 100644 --- a/gcc/ada/libgnat/a-strmap.ads +++ b/gcc/ada/libgnat/a-strmap.ads @@ -48,14 +48,13 @@ pragma Assertion_Policy (Pre => Ignore, with Ada.Characters.Latin_1; -package Ada.Strings.Maps - with SPARK_Mode +package Ada.Strings.Maps with + SPARK_Mode, + Always_Terminates is pragma Pure; -- In accordance with Ada 2005 AI-362 - pragma Annotate (GNATprove, Always_Return, Maps); - -------------------------------- -- Character Set Declarations -- -------------------------------- diff --git a/gcc/ada/libgnat/a-strsea.ads b/gcc/ada/libgnat/a-strsea.ads index 5651bdcdf3c..df1b3429529 100644 --- a/gcc/ada/libgnat/a-strsea.ads +++ b/gcc/ada/libgnat/a-strsea.ads @@ -50,9 +50,11 @@ pragma Assertion_Policy (Pre => Ignore, with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; -package Ada.Strings.Search with SPARK_Mode is +package Ada.Strings.Search with + SPARK_Mode, + Always_Terminates +is pragma Preelaborate; - pragma Annotate (GNATprove, Always_Return, Search); -- The ghost function Match tells whether the slice of Source starting at -- From and of length Pattern'Length matches with Pattern with respect to diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads index 2e0cd98f8d4..339cb17f5df 100644 --- a/gcc/ada/libgnat/a-strsup.ads +++ b/gcc/ada/libgnat/a-strsup.ads @@ -51,9 +51,11 @@ with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; with Ada.Strings.Search; with Ada.Strings.Text_Buffers; -package Ada.Strings.Superbounded with SPARK_Mode is +package Ada.Strings.Superbounded with + SPARK_Mode, + Always_Terminates +is pragma Preelaborate; - pragma Annotate (GNATprove, Always_Return, Superbounded); -- Type Bounded_String in Ada.Strings.Bounded.Generic_Bounded_Length is -- derived from Super_String, with the constraint of the maximum length. diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads index d3e88d0b4b6..be76ad2bec5 100644 --- a/gcc/ada/libgnat/a-strunb.ads +++ b/gcc/ada/libgnat/a-strunb.ads @@ -54,10 +54,10 @@ private with Ada.Strings.Text_Buffers; package Ada.Strings.Unbounded with SPARK_Mode, - Initial_Condition => Length (Null_Unbounded_String) = 0 + Initial_Condition => Length (Null_Unbounded_String) = 0, + Always_Terminates is pragma Preelaborate; - pragma Annotate (GNATprove, Always_Return, Unbounded); type Unbounded_String is private with Default_Initial_Condition => Length (Unbounded_String) = 0; diff --git a/gcc/ada/libgnat/a-strunb__shared.ads b/gcc/ada/libgnat/a-strunb__shared.ads index 3f5d56e0a8c..2da9dc72b3b 100644 --- a/gcc/ada/libgnat/a-strunb__shared.ads +++ b/gcc/ada/libgnat/a-strunb__shared.ads @@ -83,10 +83,10 @@ private with System.Atomic_Counters; private with Ada.Strings.Text_Buffers; package Ada.Strings.Unbounded with - Initial_Condition => Length (Null_Unbounded_String) = 0 + Initial_Condition => Length (Null_Unbounded_String) = 0, + Always_Terminates is pragma Preelaborate; - pragma Annotate (GNATprove, Always_Return, Unbounded); type Unbounded_String is private with Default_Initial_Condition => Length (Unbounded_String) = 0; diff --git a/gcc/ada/libgnat/a-textio.ads b/gcc/ada/libgnat/a-textio.ads index 9cedab6a222..ddbbd8592cc 100644 --- a/gcc/ada/libgnat/a-textio.ads +++ b/gcc/ada/libgnat/a-textio.ads @@ -59,7 +59,8 @@ package Ada.Text_IO with SPARK_Mode, Abstract_State => File_System, Initializes => File_System, - Initial_Condition => Line_Length = 0 and Page_Length = 0 + Initial_Condition => Line_Length = 0 and Page_Length = 0, + Always_Terminates is pragma Elaborate_Body; @@ -101,15 +102,15 @@ is Name : String := ""; Form : String := "") with - Pre => not Is_Open (File), - Post => + Pre => not Is_Open (File), + Post => Is_Open (File) and then Ada.Text_IO.Mode (File) = Mode and then (if Mode /= In_File then (Line_Length (File) = 0 and then Page_Length (File) = 0)), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Name_Error | Use_Error => Standard.True); procedure Open (File : in out File_Type; @@ -117,57 +118,56 @@ is Name : String; Form : String := "") with - Pre => not Is_Open (File), - Post => + Pre => not Is_Open (File), + Post => Is_Open (File) and then Ada.Text_IO.Mode (File) = Mode and then (if Mode /= In_File then (Line_Length (File) = 0 and then Page_Length (File) = 0)), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Name_Error | Use_Error => Standard.True); procedure Close (File : in out File_Type) with - Pre => Is_Open (File), - Post => not Is_Open (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Pre => Is_Open (File), + Post => not Is_Open (File), + Global => (In_Out => File_System); procedure Delete (File : in out File_Type) with - Pre => Is_Open (File), - Post => not Is_Open (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File), + Post => not Is_Open (File), + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); procedure Reset (File : in out File_Type; Mode : File_Mode) with - Pre => Is_Open (File), - Post => + Pre => Is_Open (File), + Post => Is_Open (File) and then Ada.Text_IO.Mode (File) = Mode and then (if Mode /= In_File then (Line_Length (File) = 0 and then Page_Length (File) = 0)), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); procedure Reset (File : in out File_Type) with - Pre => Is_Open (File), - Post => + Pre => Is_Open (File), + Post => Is_Open (File) and Mode (File)'Old = Mode (File) and (if Mode (File) /= In_File then (Line_Length (File) = 0 and then Page_Length (File) = 0)), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); function Mode (File : File_Type) return File_Mode with Pre => Is_Open (File), Global => null; function Name (File : File_Type) return String with - Pre => Is_Open (File), - Global => null; + Pre => Is_Open (File), + SPARK_Mode => Off; function Form (File : File_Type) return String with Pre => Is_Open (File), @@ -210,53 +210,51 @@ is -- an oversight, and was intended to be IN, see AI95-00057. procedure Flush (File : File_Type) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Flush with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); -------------------------------------------- -- Specification of line and page lengths -- -------------------------------------------- procedure Set_Line_Length (File : File_Type; To : Count) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File) = To and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); procedure Set_Line_Length (To : Count) with - Post => + Post => Line_Length = To and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); procedure Set_Page_Length (File : File_Type; To : Count) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Page_Length (File) = To and Line_Length (File)'Old = Line_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); procedure Set_Page_Length (To : Count) with - Post => + Post => Page_Length = To and Line_Length'Old = Line_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); function Line_Length (File : File_Type) return Count with Pre => Is_Open (File) and then Mode (File) /= In_File, @@ -277,31 +275,29 @@ is ------------------------------------ procedure New_Line (File : File_Type; Spacing : Positive_Count := 1) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure New_Line (Spacing : Positive_Count := 1) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Skip_Line (File : File_Type; Spacing : Positive_Count := 1) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Skip_Line (Spacing : Positive_Count := 1) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); function End_Of_Line (File : File_Type) return Boolean with Pre => Is_Open (File) and then Mode (File) = In_File, @@ -311,31 +307,29 @@ is Global => (Input => File_System); procedure New_Page (File : File_Type) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure New_Page with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Skip_Page (File : File_Type) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Skip_Page with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); function End_Of_Page (File : File_Type) return Boolean with Pre => Is_Open (File) and then Mode (File) = In_File, @@ -352,209 +346,201 @@ is Global => (Input => File_System); procedure Set_Col (File : File_Type; To : Positive_Count) with - Pre => + Pre => Is_Open (File) and then (if Mode (File) /= In_File then (Line_Length (File) = 0 or else To <= Line_Length (File))), - Contract_Cases => + Contract_Cases => (Mode (File) /= In_File => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), others => True), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Set_Col (To : Positive_Count) with - Pre => Line_Length = 0 or To <= Line_Length, - Post => + Pre => Line_Length = 0 or To <= Line_Length, + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Set_Line (File : File_Type; To : Positive_Count) with - Pre => + Pre => Is_Open (File) and then (if Mode (File) /= In_File then (Page_Length (File) = 0 or else To <= Page_Length (File))), - Contract_Cases => + Contract_Cases => (Mode (File) /= In_File => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), others => True), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Set_Line (To : Positive_Count) with - Pre => Page_Length = 0 or To <= Page_Length, - Post => + Pre => Page_Length = 0 or To <= Page_Length, + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); function Col (File : File_Type) return Positive_Count with - Pre => Is_Open (File), - Global => (Input => File_System); + SPARK_Mode => Off; function Col return Positive_Count with - Global => (Input => File_System); + SPARK_Mode => Off; function Line (File : File_Type) return Positive_Count with - Pre => Is_Open (File), - Global => (Input => File_System); + SPARK_Mode => Off; function Line return Positive_Count with - Global => (Input => File_System); + SPARK_Mode => Off; function Page (File : File_Type) return Positive_Count with - Pre => Is_Open (File), - Global => (Input => File_System); + SPARK_Mode => Off; function Page return Positive_Count with - Global => (Input => File_System); + SPARK_Mode => Off; ---------------------------- -- Character Input-Output -- ---------------------------- procedure Get (File : File_Type; Item : out Character) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Get (Item : out Character) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Put (File : File_Type; Item : Character) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Put (Item : Character) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Look_Ahead (File : File_Type; Item : out Character; End_Of_Line : out Boolean) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System); procedure Look_Ahead (Item : out Character; End_Of_Line : out Boolean) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + Global => (Input => File_System); procedure Get_Immediate (File : File_Type; Item : out Character) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Get_Immediate (Item : out Character) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Get_Immediate (File : File_Type; Item : out Character; Available : out Boolean) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Get_Immediate (Item : out Character; Available : out Boolean) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); ------------------------- -- String Input-Output -- ------------------------- procedure Get (File : File_Type; Item : out String) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Item'Length'Old > 0); procedure Get (Item : out String) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Item'Length'Old > 0); procedure Put (File : File_Type; Item : String) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Put (Item : String) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Get_Line (File : File_Type; Item : out String; Last : out Natural) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Post => (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last - else Last = Item'First - 1), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Post => + (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last + else Last = Item'First - 1), + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Item'Length'Old > 0); procedure Get_Line (Item : out String; Last : out Natural) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length and (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last else Last = Item'First - 1), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Item'Length'Old > 0); function Get_Line (File : File_Type) return String with SPARK_Mode => Off; pragma Ada_05 (Get_Line); @@ -566,21 +552,19 @@ is (File : File_Type; Item : String) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Put_Line (Item : String) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); --------------------------------------- -- Generic packages for Input-Output -- diff --git a/gcc/ada/libgnat/a-tideio.ads b/gcc/ada/libgnat/a-tideio.ads index b62d251201a..7f8fa191575 100644 --- a/gcc/ada/libgnat/a-tideio.ads +++ b/gcc/ada/libgnat/a-tideio.ads @@ -43,7 +43,9 @@ private generic type Num is delta <> digits <>; -package Ada.Text_IO.Decimal_IO is +package Ada.Text_IO.Decimal_IO with + Always_Terminates +is Default_Fore : Field := Num'Fore; Default_Aft : Field := Num'Aft; @@ -54,19 +56,19 @@ package Ada.Text_IO.Decimal_IO is Item : out Num; Width : Field := 0) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Get (Item : out Num; Width : Field := 0) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Put (File : File_Type; @@ -75,12 +77,12 @@ package Ada.Text_IO.Decimal_IO is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0); procedure Put (Item : Num; @@ -88,11 +90,11 @@ package Ada.Text_IO.Decimal_IO is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Ada.Text_IO.Line_Length /= 0); procedure Get (From : String; @@ -100,7 +102,7 @@ package Ada.Text_IO.Decimal_IO is Last : out Positive) with Global => null, - Annotate => (GNATprove, Might_Not_Return); + Exceptional_Cases => (Data_Error => Standard.True); procedure Put (To : out String; @@ -108,8 +110,8 @@ package Ada.Text_IO.Decimal_IO is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Layout_Error => Standard.True); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-tienio.ads b/gcc/ada/libgnat/a-tienio.ads index aac90f767ba..e4cdaeec514 100644 --- a/gcc/ada/libgnat/a-tienio.ads +++ b/gcc/ada/libgnat/a-tienio.ads @@ -23,21 +23,24 @@ private generic type Enum is (<>); -package Ada.Text_IO.Enumeration_IO is +package Ada.Text_IO.Enumeration_IO with + Always_Terminates +is Default_Width : Field := 0; Default_Setting : Type_Set := Upper_Case; procedure Get (File : File_Type; Item : out Enum) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); + procedure Get (Item : out Enum) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Put (File : File_Type; @@ -45,38 +48,38 @@ package Ada.Text_IO.Enumeration_IO is Width : Field := Default_Width; Set : Type_Set := Default_Setting) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0); procedure Put (Item : Enum; Width : Field := Default_Width; Set : Type_Set := Default_Setting) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Ada.Text_IO.Line_Length /= 0); procedure Get (From : String; Item : out Enum; Last : out Positive) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Data_Error => Standard.True); procedure Put (To : out String; Item : Enum; Set : Type_Set := Default_Setting) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Layout_Error => Standard.True); end Ada.Text_IO.Enumeration_IO; diff --git a/gcc/ada/libgnat/a-tifiio.ads b/gcc/ada/libgnat/a-tifiio.ads index bbf8e90ffef..0e3e71c82f0 100644 --- a/gcc/ada/libgnat/a-tifiio.ads +++ b/gcc/ada/libgnat/a-tifiio.ads @@ -23,7 +23,10 @@ private generic type Num is delta <>; -package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is +package Ada.Text_IO.Fixed_IO with + SPARK_Mode => On, + Always_Terminates +is Default_Fore : Field := Num'Fore; Default_Aft : Field := Num'Aft; @@ -34,19 +37,19 @@ package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is Item : out Num; Width : Field := 0) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Get (Item : out Num; Width : Field := 0) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Put (File : File_Type; @@ -55,12 +58,12 @@ package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0); procedure Put (Item : Num; @@ -68,19 +71,19 @@ package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Ada.Text_IO.Line_Length /= 0); procedure Get (From : String; Item : out Num; Last : out Positive) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Data_Error => Standard.True); procedure Put (To : out String; @@ -88,8 +91,8 @@ package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Layout_Error => Standard.True); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-tiflio.ads b/gcc/ada/libgnat/a-tiflio.ads index 82ff84bf345..fcfa76a963e 100644 --- a/gcc/ada/libgnat/a-tiflio.ads +++ b/gcc/ada/libgnat/a-tiflio.ads @@ -43,7 +43,10 @@ private generic type Num is digits <>; -package Ada.Text_IO.Float_IO with SPARK_Mode => On is +package Ada.Text_IO.Float_IO with + SPARK_Mode => On, + Always_Terminates +is Default_Fore : Field := 2; Default_Aft : Field := Num'Digits - 1; @@ -54,19 +57,19 @@ package Ada.Text_IO.Float_IO with SPARK_Mode => On is Item : out Num; Width : Field := 0) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Get (Item : out Num; Width : Field := 0) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Put (File : File_Type; @@ -75,12 +78,12 @@ package Ada.Text_IO.Float_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0); procedure Put (Item : Num; @@ -88,19 +91,19 @@ package Ada.Text_IO.Float_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length /= 0); procedure Get (From : String; Item : out Num; Last : out Positive) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Data_Error => Standard.True); procedure Put (To : out String; @@ -108,8 +111,8 @@ package Ada.Text_IO.Float_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Layout_Error => Standard.True); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-tiinio.ads b/gcc/ada/libgnat/a-tiinio.ads index 0299cc0eed1..60f21cc19b6 100644 --- a/gcc/ada/libgnat/a-tiinio.ads +++ b/gcc/ada/libgnat/a-tiinio.ads @@ -43,7 +43,9 @@ private generic type Num is range <>; -package Ada.Text_IO.Integer_IO is +package Ada.Text_IO.Integer_IO with + Always_Terminates +is Default_Width : Field := Num'Width; Default_Base : Number_Base := 10; @@ -53,19 +55,19 @@ package Ada.Text_IO.Integer_IO is Item : out Num; Width : Field := 0) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Get (Item : out Num; Width : Field := 0) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Put (File : File_Type; @@ -73,39 +75,39 @@ package Ada.Text_IO.Integer_IO is Width : Field := Default_Width; Base : Number_Base := Default_Base) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0); procedure Put (Item : Num; Width : Field := Default_Width; Base : Number_Base := Default_Base) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length /= 0); procedure Get (From : String; Item : out Num; Last : out Positive) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Data_Error => Standard.True); procedure Put (To : out String; Item : Num; Base : Number_Base := Default_Base) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Layout_Error => Standard.True); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-timoio.ads b/gcc/ada/libgnat/a-timoio.ads index c8554b8f0aa..40d91ed5eab 100644 --- a/gcc/ada/libgnat/a-timoio.ads +++ b/gcc/ada/libgnat/a-timoio.ads @@ -43,7 +43,9 @@ private generic type Num is mod <>; -package Ada.Text_IO.Modular_IO is +package Ada.Text_IO.Modular_IO with + Always_Terminates +is Default_Width : Field := Num'Width; Default_Base : Number_Base := 10; @@ -53,19 +55,19 @@ package Ada.Text_IO.Modular_IO is Item : out Num; Width : Field := 0) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Get (Item : out Num; Width : Field := 0) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Data_Error | End_Error => Standard.True); procedure Put (File : File_Type; @@ -73,39 +75,39 @@ package Ada.Text_IO.Modular_IO is Width : Field := Default_Width; Base : Number_Base := Default_Base) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0); procedure Put (Item : Num; Width : Field := Default_Width; Base : Number_Base := Default_Base) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Layout_Error => Line_Length /= 0); procedure Get (From : String; Item : out Num; Last : out Positive) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Data_Error => Standard.True); procedure Put (To : out String; Item : Num; Base : Number_Base := Default_Base) with - Global => null, - Annotate => (GNATprove, Might_Not_Return); + Global => null, + Exceptional_Cases => (Layout_Error => Standard.True); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/g-souinf.ads b/gcc/ada/libgnat/g-souinf.ads index b6598b503d5..ea65c73e935 100644 --- a/gcc/ada/libgnat/g-souinf.ads +++ b/gcc/ada/libgnat/g-souinf.ads @@ -41,7 +41,7 @@ package GNAT.Source_Info with Abstract_State => (Source_Code_Information with External => (Async_Writers, Async_Readers)), - Annotate => (GNATprove, Always_Return) + Always_Terminates is pragma Preelaborate; -- Note that this unit is Preelaborate, but not Pure, that's because the diff --git a/gcc/ada/libgnat/i-c.ads b/gcc/ada/libgnat/i-c.ads index 70af56a7836..fe87fba32b6 100644 --- a/gcc/ada/libgnat/i-c.ads +++ b/gcc/ada/libgnat/i-c.ads @@ -27,10 +27,11 @@ pragma Assertion_Policy (Pre => Ignore, with System; with System.Parameters; -package Interfaces.C - with SPARK_Mode, Pure +package Interfaces.C with + SPARK_Mode, + Pure, + Always_Terminates is - pragma Annotate (GNATprove, Always_Return, C); -- Each of the types declared in Interfaces.C is C-compatible. diff --git a/gcc/ada/libgnat/i-cstrin.ads b/gcc/ada/libgnat/i-cstrin.ads index 49b1f137270..e486f03a585 100644 --- a/gcc/ada/libgnat/i-cstrin.ads +++ b/gcc/ada/libgnat/i-cstrin.ads @@ -44,7 +44,8 @@ pragma Assertion_Policy (Pre => Ignore); package Interfaces.C.Strings with SPARK_Mode => On, Abstract_State => (C_Memory), - Initializes => (C_Memory) + Initializes => (C_Memory), + Always_Terminates is pragma Preelaborate; @@ -118,16 +119,11 @@ is Chars : char_array; Check : Boolean := True) with - Pre => + Pre => Item /= Null_Ptr - and then - (if Check then - Strlen (Item) <= size_t'Last - Offset - and then Strlen (Item) + Offset <= Chars'Length), - Global => (In_Out => C_Memory), - Annotate => (GNATprove, Might_Not_Return); - -- Update may not return if Check is False and the null terminator - -- is overwritten or skipped with Offset. + and then Strlen (Item) <= size_t'Last - Offset + and then Strlen (Item) + Offset <= Chars'Length, + Global => (In_Out => C_Memory); procedure Update (Item : chars_ptr; @@ -135,16 +131,11 @@ is Str : String; Check : Boolean := True) with - Pre => + Pre => Item /= Null_Ptr - and then - (if Check then - Strlen (Item) <= size_t'Last - Offset - and then Strlen (Item) + Offset <= Str'Length), - Global => (In_Out => C_Memory), - Annotate => (GNATprove, Might_Not_Return); - -- Update may not return if Check is False and the null terminator - -- is overwritten or skipped with Offset. + and then Strlen (Item) <= size_t'Last - Offset + and then Strlen (Item) + Offset <= Str'Length, + Global => (In_Out => C_Memory); Update_Error : exception; diff --git a/gcc/ada/libgnat/interfac.ads b/gcc/ada/libgnat/interfac.ads index edd3f36207b..bc37a8e339e 100644 --- a/gcc/ada/libgnat/interfac.ads +++ b/gcc/ada/libgnat/interfac.ads @@ -35,10 +35,11 @@ -- This is the compiler version of this unit -package Interfaces is +package Interfaces with + Always_Terminates +is pragma No_Elaboration_Code_All; pragma Pure; - pragma Annotate (GNATprove, Always_Return, Interfaces); -- All identifiers in this unit are implementation defined diff --git a/gcc/ada/libgnat/interfac__2020.ads b/gcc/ada/libgnat/interfac__2020.ads index 89557bf5ea6..70d82be5759 100644 --- a/gcc/ada/libgnat/interfac__2020.ads +++ b/gcc/ada/libgnat/interfac__2020.ads @@ -35,10 +35,11 @@ -- This is the runtime version of this unit (not used during GNAT build) -package Interfaces is +package Interfaces with + Always_Terminates +is pragma No_Elaboration_Code_All; pragma Pure; - pragma Annotate (GNATprove, Always_Return, Interfaces); -- All identifiers in this unit are implementation defined diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 041478538a7..66ace8071ff 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -165,9 +165,8 @@ is function To_Neg_Int (A : Double_Uns) return Double_Int with - Annotate => (GNATprove, Always_Return), - Pre => In_Double_Int_Range (-Big (A)), - Post => Big (To_Neg_Int'Result) = -Big (A); + 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 -- 0 .. 2 ** (Double_Size - 1), then the corresponding nonpositive signed -- integer (obtained by negating the given value) is returned, otherwise @@ -175,9 +174,8 @@ is function To_Pos_Int (A : Double_Uns) return Double_Int with - Annotate => (GNATprove, Always_Return), - Pre => In_Double_Int_Range (Big (A)), - Post => Big (To_Pos_Int'Result) = Big (A); + 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 -- 0 .. 2 ** (Double_Size - 1) - 1, then the corresponding non-negative -- signed integer is returned, otherwise constraint error is raised. diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb index 219523b00f2..d19b9e182fd 100644 --- a/gcc/ada/libgnat/s-arit32.adb +++ b/gcc/ada/libgnat/s-arit32.adb @@ -104,9 +104,8 @@ is function To_Neg_Int (A : Uns32) return Int32 with - Annotate => (GNATprove, Always_Return), - Pre => In_Int32_Range (-Big (A)), - Post => Big (To_Neg_Int'Result) = -Big (A); + 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 -- 0 .. 2**31, then the corresponding nonpositive signed integer (obtained -- by negating the given value) is returned, otherwise constraint error is @@ -114,9 +113,8 @@ is function To_Pos_Int (A : Uns32) return Int32 with - Annotate => (GNATprove, Always_Return), - Pre => In_Int32_Range (Big (A)), - Post => Big (To_Pos_Int'Result) = Big (A); + 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 -- 0 .. 2**31 - 1, then the corresponding nonnegative signed integer is -- returned, otherwise constraint error is raised. diff --git a/gcc/ada/libgnat/s-atacco.ads b/gcc/ada/libgnat/s-atacco.ads index bd920cc905c..157ca52a4f2 100644 --- a/gcc/ada/libgnat/s-atacco.ads +++ b/gcc/ada/libgnat/s-atacco.ads @@ -55,11 +55,9 @@ package System.Address_To_Access_Conversions is -- of no strict aliasing. function To_Pointer (Value : Address) return Object_Pointer with - Global => null, - Annotate => (GNATprove, Always_Return); + Global => null; function To_Address (Value : Object_Pointer) return Address with - SPARK_Mode => Off, - Annotate => (GNATprove, Always_Return); + SPARK_Mode => Off; pragma Import (Intrinsic, To_Pointer); pragma Import (Intrinsic, To_Address); diff --git a/gcc/ada/libgnat/s-spcuop.ads b/gcc/ada/libgnat/s-spcuop.ads index daf550b69d8..642ded7daac 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, Always_Return) + Always_Terminates is function By (Consequence, Premise : Boolean) return Boolean with diff --git a/gcc/ada/libgnat/s-stoele.ads b/gcc/ada/libgnat/s-stoele.ads index 7de150dab59..d5d70428a5d 100644 --- a/gcc/ada/libgnat/s-stoele.ads +++ b/gcc/ada/libgnat/s-stoele.ads @@ -37,7 +37,9 @@ -- extra declarations that can be introduced into System using Extend_System. -- It is a good idea to avoid use clauses for this package. -package System.Storage_Elements is +package System.Storage_Elements with + Always_Terminates +is pragma Pure; -- Note that we take advantage of the implementation permission to make -- this unit Pure instead of Preelaborable; see RM 13.7.1(15). In Ada 2005, @@ -46,8 +48,6 @@ package System.Storage_Elements is pragma No_Elaboration_Code_All; -- Allow the use of that restriction in units that WITH this unit - pragma Annotate (GNATprove, Always_Return, Storage_Elements); - type Storage_Offset is range -Memory_Size / 2 .. Memory_Size / 2 - 1; subtype Storage_Count is Storage_Offset range 0 .. Storage_Offset'Last; diff --git a/gcc/ada/libgnat/s-vaispe.ads b/gcc/ada/libgnat/s-vaispe.ads index 28efcede4c7..e74202d736e 100644 --- a/gcc/ada/libgnat/s-vaispe.ads +++ b/gcc/ada/libgnat/s-vaispe.ads @@ -62,7 +62,7 @@ generic package System.Value_I_Spec with Ghost, SPARK_Mode, - Annotate => (GNATprove, Always_Return) + Always_Terminates is pragma Preelaborate; use all type Uns_Params.Uns_Option; diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads index 960ad8ec486..bdd97b52e07 100644 --- a/gcc/ada/libgnat/s-vauspe.ads +++ b/gcc/ada/libgnat/s-vauspe.ads @@ -53,7 +53,7 @@ generic package System.Value_U_Spec with Ghost, SPARK_Mode, - Annotate => (GNATprove, Always_Return) + Always_Terminates is pragma Preelaborate;