From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 1914) id 75C673836FA3; Tue, 12 Jul 2022 12:25:31 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 75C673836FA3 MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Pierre-Marie de Rodat To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-1624] [Ada] Annotate libraries with returning annotation X-Act-Checkin: gcc X-Git-Author: Joffrey Huguet X-Git-Refname: refs/heads/master X-Git-Oldrev: 01bf0d6cf53c8c5909f07d89a188b8b1a7a8f179 X-Git-Newrev: a31eda15463b00bad7c48d973e4e7e8a33006379 Message-Id: <20220712122531.75C673836FA3@sourceware.org> Date: Tue, 12 Jul 2022 12:25:31 +0000 (GMT) X-BeenThere: gcc-cvs@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-cvs mailing list List-Unsubscribe: , List-Archive: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 12 Jul 2022 12:25:31 -0000 https://gcc.gnu.org/g:a31eda15463b00bad7c48d973e4e7e8a33006379 commit r13-1624-ga31eda15463b00bad7c48d973e4e7e8a33006379 Author: Joffrey Huguet Date: Mon Jun 13 11:44:51 2022 +0200 [Ada] Annotate libraries with returning annotation This patch annotates SPARK-annotated libraries with returning annotations (Always_Return, Might_Not_Return) to remove the warnings raised by GNATprove about missing annotations. gcc/ada/ * libgnarl/a-reatim.ads, libgnat/a-cfdlli.ads, libgnat/a-cfhama.ads, libgnat/a-cfhase.ads, libgnat/a-cfinse.ads, libgnat/a-cfinve.ads, libgnat/a-cforma.ads, libgnat/a-cforse.ads, libgnat/a-chahan.ads, libgnat/a-cofove.ads, libgnat/a-cofuma.ads, libgnat/a-cofuse.ads, libgnat/a-cofuve.ads, libgnat/a-nbnbin.ads, libgnat/a-nbnbre.ads, libgnat/a-ngelfu.ads, libgnat/a-nlelfu.ads, libgnat/a-nllefu.ads, libgnat/a-nselfu.ads, libgnat/a-nuelfu.ads, libgnat/a-strbou.ads, libgnat/a-strfix.ads, libgnat/a-strmap.ads, libgnat/a-strunb.ads, libgnat/a-strunb__shared.ads, libgnat/a-strsea.ads, libgnat/a-textio.ads, libgnat/a-tideio.ads, libgnat/a-tienio.ads, libgnat/a-tifiio.ads, libgnat/a-tiflio.ads, libgnat/a-tiinio.ads, libgnat/a-timoio.ads, libgnat/i-c.ads, libgnat/interfac.ads, libgnat/interfac__2020.ads, libgnat/s-atacco.ads, libgnat/s-stoele.ads: Annotate packages and subprograms with returning annotations. Diff: --- gcc/ada/libgnarl/a-reatim.ads | 1 + gcc/ada/libgnat/a-cfdlli.ads | 4 +- gcc/ada/libgnat/a-cfhama.ads | 4 +- gcc/ada/libgnat/a-cfhase.ads | 4 +- gcc/ada/libgnat/a-cfinse.ads | 5 +- gcc/ada/libgnat/a-cfinve.ads | 4 +- gcc/ada/libgnat/a-cforma.ads | 4 +- gcc/ada/libgnat/a-cforse.ads | 4 +- gcc/ada/libgnat/a-chahan.ads | 2 + gcc/ada/libgnat/a-cofove.ads | 2 + gcc/ada/libgnat/a-cofuma.ads | 5 +- gcc/ada/libgnat/a-cofuse.ads | 5 +- gcc/ada/libgnat/a-cofuve.ads | 5 +- gcc/ada/libgnat/a-nbnbin.ads | 2 + gcc/ada/libgnat/a-nbnbre.ads | 2 + gcc/ada/libgnat/a-ngelfu.ads | 1 + 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 | 2 + gcc/ada/libgnat/a-strfix.ads | 138 +++++++++------ gcc/ada/libgnat/a-strmap.ads | 2 + gcc/ada/libgnat/a-strsea.ads | 1 + gcc/ada/libgnat/a-strunb.ads | 1 + gcc/ada/libgnat/a-strunb__shared.ads | 1 + gcc/ada/libgnat/a-textio.ads | 318 +++++++++++++++++++++-------------- gcc/ada/libgnat/a-tideio.ads | 28 +-- gcc/ada/libgnat/a-tienio.ads | 28 +-- gcc/ada/libgnat/a-tifiio.ads | 28 +-- gcc/ada/libgnat/a-tiflio.ads | 28 +-- gcc/ada/libgnat/a-tiinio.ads | 28 +-- gcc/ada/libgnat/a-timoio.ads | 28 +-- gcc/ada/libgnat/i-c.ads | 2 + gcc/ada/libgnat/interfac.ads | 1 + gcc/ada/libgnat/interfac__2020.ads | 1 + gcc/ada/libgnat/s-atacco.ads | 6 +- gcc/ada/libgnat/s-stoele.ads | 2 + 38 files changed, 443 insertions(+), 258 deletions(-) diff --git a/gcc/ada/libgnarl/a-reatim.ads b/gcc/ada/libgnarl/a-reatim.ads index 4b8f7aab259..dee20e99f4b 100644 --- a/gcc/ada/libgnarl/a-reatim.ads +++ b/gcc/ada/libgnarl/a-reatim.ads @@ -41,6 +41,7 @@ package Ada.Real_Time with Abstract_State => (Clock_Time with Synchronous), Initializes => Clock_Time is + pragma Annotate (GNATprove, Always_Return, Real_Time); pragma Compile_Time_Error (Duration'Size /= 64, diff --git a/gcc/ada/libgnat/a-cfdlli.ads b/gcc/ada/libgnat/a-cfdlli.ads index ff7d2d81aca..01e7db29132 100644 --- a/gcc/ada/libgnat/a-cfdlli.ads +++ b/gcc/ada/libgnat/a-cfdlli.ads @@ -37,8 +37,10 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Formal_Doubly_Linked_Lists with - SPARK_Mode + SPARK_Mode, + Annotate => (GNATprove, Always_Return) is + -- Contracts in this unit are meant for analysis only, not for run-time -- checking. diff --git a/gcc/ada/libgnat/a-cfhama.ads b/gcc/ada/libgnat/a-cfhama.ads index bf1e85f3ab8..8cb7488f183 100644 --- a/gcc/ada/libgnat/a-cfhama.ads +++ b/gcc/ada/libgnat/a-cfhama.ads @@ -62,8 +62,10 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Formal_Hashed_Maps with - SPARK_Mode + SPARK_Mode, + Annotate => (GNATprove, Always_Return) is + -- Contracts in this unit are meant for analysis only, not for run-time -- checking. diff --git a/gcc/ada/libgnat/a-cfhase.ads b/gcc/ada/libgnat/a-cfhase.ads index 80ce9485b2d..248a0ac9234 100644 --- a/gcc/ada/libgnat/a-cfhase.ads +++ b/gcc/ada/libgnat/a-cfhase.ads @@ -62,8 +62,10 @@ generic Right : Element_Type) return Boolean is "="; package Ada.Containers.Formal_Hashed_Sets with - SPARK_Mode + SPARK_Mode, + Annotate => (GNATprove, Always_Return) is + -- Contracts in this unit are meant for analysis only, not for run-time -- checking. diff --git a/gcc/ada/libgnat/a-cfinse.ads b/gcc/ada/libgnat/a-cfinse.ads index cff2900e71f..d7fdb0426cc 100644 --- a/gcc/ada/libgnat/a-cfinse.ads +++ b/gcc/ada/libgnat/a-cfinse.ads @@ -38,7 +38,10 @@ generic type Element_Type (<>) is private; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Functional_Infinite_Sequences with SPARK_Mode is +package Ada.Containers.Functional_Infinite_Sequences with + SPARK_Mode, + Annotate => (GNATprove, Always_Return) +is type Sequence is private with Default_Initial_Condition => Length (Sequence) = 0, diff --git a/gcc/ada/libgnat/a-cfinve.ads b/gcc/ada/libgnat/a-cfinve.ads index b5fa29bf7b1..f44e45b8171 100644 --- a/gcc/ada/libgnat/a-cfinve.ads +++ b/gcc/ada/libgnat/a-cfinve.ads @@ -53,8 +53,10 @@ generic -- grow via heap allocation. package Ada.Containers.Formal_Indefinite_Vectors with - SPARK_Mode => On + SPARK_Mode, + Annotate => (GNATprove, Always_Return) is + -- Contracts in this unit are meant for analysis only, not for run-time -- checking. diff --git a/gcc/ada/libgnat/a-cforma.ads b/gcc/ada/libgnat/a-cforma.ads index 1e3c57b1c9c..7be2eec4ae7 100644 --- a/gcc/ada/libgnat/a-cforma.ads +++ b/gcc/ada/libgnat/a-cforma.ads @@ -61,8 +61,10 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Formal_Ordered_Maps with - SPARK_Mode + SPARK_Mode, + Annotate => (GNATprove, Always_Return) is + -- Contracts in this unit are meant for analysis only, not for run-time -- checking. diff --git a/gcc/ada/libgnat/a-cforse.ads b/gcc/ada/libgnat/a-cforse.ads index f6a033f680f..ff96d8e7547 100644 --- a/gcc/ada/libgnat/a-cforse.ads +++ b/gcc/ada/libgnat/a-cforse.ads @@ -59,8 +59,10 @@ generic with function "<" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Formal_Ordered_Sets with - SPARK_Mode + SPARK_Mode, + Annotate => (GNATprove, Always_Return) is + -- Contracts in this unit are meant for analysis only, not for run-time -- checking. diff --git a/gcc/ada/libgnat/a-chahan.ads b/gcc/ada/libgnat/a-chahan.ads index e98cda351df..dc1a629cf2a 100644 --- a/gcc/ada/libgnat/a-chahan.ads +++ b/gcc/ada/libgnat/a-chahan.ads @@ -46,6 +46,8 @@ 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-cofove.ads b/gcc/ada/libgnat/a-cofove.ads index cba10a63746..64133750f29 100644 --- a/gcc/ada/libgnat/a-cofove.ads +++ b/gcc/ada/libgnat/a-cofove.ads @@ -45,6 +45,8 @@ generic package Ada.Containers.Formal_Vectors with SPARK_Mode is + pragma Annotate (GNATprove, Always_Return, Formal_Vectors); + -- Contracts in this unit are meant for analysis only, not for run-time -- checking. diff --git a/gcc/ada/libgnat/a-cofuma.ads b/gcc/ada/libgnat/a-cofuma.ads index d01c4b4dd22..f863cdc979f 100644 --- a/gcc/ada/libgnat/a-cofuma.ads +++ b/gcc/ada/libgnat/a-cofuma.ads @@ -49,7 +49,10 @@ generic -- of equivalence over keys is needed, that is, Equivalent_Keys defines a -- key uniquely. -package Ada.Containers.Functional_Maps with SPARK_Mode is +package Ada.Containers.Functional_Maps with + SPARK_Mode, + Annotate => (GNATprove, Always_Return) +is type Map is private with Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0, diff --git a/gcc/ada/libgnat/a-cofuse.ads b/gcc/ada/libgnat/a-cofuse.ads index 29f1e9f979f..ce52f613f07 100644 --- a/gcc/ada/libgnat/a-cofuse.ads +++ b/gcc/ada/libgnat/a-cofuse.ads @@ -47,7 +47,10 @@ generic -- of equivalence over elements is needed, that is, Equivalent_Elements -- defines an element uniquely. -package Ada.Containers.Functional_Sets with SPARK_Mode is +package Ada.Containers.Functional_Sets with + SPARK_Mode, + Annotate => (GNATprove, Always_Return) +is type Set is private with Default_Initial_Condition => Is_Empty (Set), diff --git a/gcc/ada/libgnat/a-cofuve.ads b/gcc/ada/libgnat/a-cofuve.ads index f926a963737..86222217af5 100644 --- a/gcc/ada/libgnat/a-cofuve.ads +++ b/gcc/ada/libgnat/a-cofuve.ads @@ -40,7 +40,10 @@ generic type Element_Type (<>) is private; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Functional_Vectors with SPARK_Mode is +package Ada.Containers.Functional_Vectors with + SPARK_Mode, + Annotate => (GNATprove, Always_Return) +is subtype Extended_Index is Index_Type'Base range Index_Type'Pred (Index_Type'First) .. Index_Type'Last; diff --git a/gcc/ada/libgnat/a-nbnbin.ads b/gcc/ada/libgnat/a-nbnbin.ads index 1ba10da6a0d..ffb96d4d98b 100644 --- a/gcc/ada/libgnat/a-nbnbin.ads +++ b/gcc/ada/libgnat/a-nbnbin.ads @@ -21,6 +21,8 @@ private with System; package Ada.Numerics.Big_Numbers.Big_Integers with Preelaborate is + pragma Annotate (GNATprove, Always_Return, Big_Integers); + type Big_Integer is private with Integer_Literal => From_Universal_Image, Put_Image => Put_Image; diff --git a/gcc/ada/libgnat/a-nbnbre.ads b/gcc/ada/libgnat/a-nbnbre.ads index 4118d2bb99c..350d0497ed4 100644 --- a/gcc/ada/libgnat/a-nbnbre.ads +++ b/gcc/ada/libgnat/a-nbnbre.ads @@ -20,6 +20,8 @@ with Ada.Strings.Text_Buffers; use Ada.Strings.Text_Buffers; package Ada.Numerics.Big_Numbers.Big_Reals with Preelaborate is + pragma Annotate (GNATprove, Always_Return, Big_Reals); + type Big_Real is private with Real_Literal => From_Universal_Image, Put_Image => Put_Image; diff --git a/gcc/ada/libgnat/a-ngelfu.ads b/gcc/ada/libgnat/a-ngelfu.ads index c8a31bb494d..75783ef44a4 100644 --- a/gcc/ada/libgnat/a-ngelfu.ads +++ b/gcc/ada/libgnat/a-ngelfu.ads @@ -40,6 +40,7 @@ package Ada.Numerics.Generic_Elementary_Functions with SPARK_Mode => On 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 10b33e9cb3c..b3afd1fc997 100644 --- a/gcc/ada/libgnat/a-nlelfu.ads +++ b/gcc/ada/libgnat/a-nlelfu.ads @@ -19,3 +19,4 @@ 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 7089fc3efb0..e137c67e786 100644 --- a/gcc/ada/libgnat/a-nllefu.ads +++ b/gcc/ada/libgnat/a-nllefu.ads @@ -19,3 +19,4 @@ 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 10b04acdeb9..6797efd70e9 100644 --- a/gcc/ada/libgnat/a-nselfu.ads +++ b/gcc/ada/libgnat/a-nselfu.ads @@ -19,3 +19,4 @@ 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 149939babea..d4fe74572f6 100644 --- a/gcc/ada/libgnat/a-nuelfu.ads +++ b/gcc/ada/libgnat/a-nuelfu.ads @@ -19,3 +19,4 @@ 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 839760ac26a..678c3454e4e 100644 --- a/gcc/ada/libgnat/a-strbou.ads +++ b/gcc/ada/libgnat/a-strbou.ads @@ -49,6 +49,7 @@ with Ada.Strings.Search; package Ada.Strings.Bounded with SPARK_Mode is pragma Preelaborate; + pragma Annotate (GNATprove, Always_Return, Bounded); generic Max : Positive; @@ -68,6 +69,7 @@ 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 0d6c5d07663..dee64ab9e0e 100644 --- a/gcc/ada/libgnat/a-strfix.ads +++ b/gcc/ada/libgnat/a-strfix.ads @@ -63,7 +63,8 @@ package Ada.Strings.Fixed with SPARK_Mode is -- Incomplete contract - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); -- 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: @@ -168,7 +169,8 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Index'Result = 0), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); pragma Ada_05 (Index); function Index @@ -231,7 +233,8 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Index'Result = 0), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); pragma Ada_05 (Index); -- Each Index function searches, starting from From, for a slice of @@ -300,7 +303,8 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Index'Result = 0), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); function Index (Source : String; @@ -355,7 +359,8 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Index'Result = 0), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); -- If Going = Forward, returns: -- @@ -408,7 +413,8 @@ 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; + Global => null, + Annotate => (GNATprove, Always_Return); function Index (Source : String; @@ -464,7 +470,8 @@ 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; + Global => null, + Annotate => (GNATprove, Always_Return); 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 @@ -524,7 +531,8 @@ package Ada.Strings.Fixed with SPARK_Mode is and then (J = From or else (J > From) = (Going = Forward)) then Source (J) = ' '))), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); pragma Ada_05 (Index_Non_Blank); -- Returns Index (Source, Maps.To_Set(Space), From, Outside, Going) @@ -562,7 +570,8 @@ package Ada.Strings.Fixed with SPARK_Mode is and then (J < Index_Non_Blank'Result) = (Going = Forward) then Source (J) = ' '))), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); -- Returns Index (Source, Maps.To_Set(Space), Outside, Going) function Count @@ -570,16 +579,18 @@ 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; + Pre => Pattern'Length /= 0, + Global => null, + Annotate => (GNATprove, Always_Return); function Count (Source : String; Pattern : String; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => Pattern'Length /= 0 and then Mapping /= null, - Global => null; + Pre => Pattern'Length /= 0 and then Mapping /= null, + Global => null, + Annotate => (GNATprove, Always_Return); -- Returns the maximum number of nonoverlapping slices of Source that match -- Pattern with respect to Mapping. If Pattern is the null string then @@ -589,7 +600,8 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : String; Set : Maps.Character_Set) return Natural with - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); -- Returns the number of occurrences in Source of characters that are in -- Set. @@ -647,7 +659,8 @@ package Ada.Strings.Fixed with SPARK_Mode is then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); 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 @@ -709,7 +722,8 @@ package Ada.Strings.Fixed with SPARK_Mode is then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); -- Equivalent to Find_Token (Source, Set, Source'First, Test, First, Last) ------------------------------------ @@ -738,7 +752,8 @@ 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; + Global => null, + Annotate => (GNATprove, Always_Return); function Translate (Source : String; @@ -761,7 +776,8 @@ 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; + Global => null, + Annotate => (GNATprove, Always_Return); -- 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 @@ -771,27 +787,29 @@ 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; + Global => null, + Annotate => (GNATprove, Always_Return); procedure Translate (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; + Global => null, + Annotate => (GNATprove, Always_Return); -- Equivalent to Source := Translate(Source, Mapping) @@ -884,7 +902,8 @@ package Ada.Strings.Fixed with SPARK_Mode is (Low - Source'First + By'Length + 1 .. Replace_Slice'Result'Last) = Source (Low .. Source'Last))), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); -- If Low > Source'Last + 1, or High < Source'First - 1, then Index_Error -- is propagated. Otherwise: -- @@ -904,7 +923,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 @@ -916,7 +935,8 @@ package Ada.Strings.Fixed with SPARK_Mode is -- Incomplete contract - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); -- Equivalent to: -- -- Move (Replace_Slice (Source, Low, High, By), @@ -962,7 +982,8 @@ package Ada.Strings.Fixed with SPARK_Mode is (Before - Source'First + New_Item'Length + 1 .. Insert'Result'Last) = Source (Before .. Source'Last)), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); -- Propagates Index_Error if Before is not in -- Source'First .. Source'Last + 1; otherwise, returns -- Source (Source'First .. Before - 1) @@ -974,13 +995,14 @@ 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; + Global => null, + Annotate => (GNATprove, Might_Not_Return); -- Equivalent to Move (Insert (Source, Before, New_Item), Source, Drop) function Overwrite @@ -988,13 +1010,13 @@ package Ada.Strings.Fixed with SPARK_Mode is Position : Positive; New_Item : String) return String 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), - Post => + Post => -- Lower bound of the returned string is 1 @@ -1029,7 +1051,8 @@ 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; + Global => null, + Annotate => (GNATprove, Always_Return); -- 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 @@ -1043,7 +1066,7 @@ 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 @@ -1051,7 +1074,8 @@ package Ada.Strings.Fixed with SPARK_Mode is -- Incomplete contract - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); -- Equivalent to Move(Overwrite(Source, Position, New_Item), Source, Drop) function Delete @@ -1099,7 +1123,8 @@ package Ada.Strings.Fixed with SPARK_Mode is others => Delete'Result'Length = Source'Length and then Delete'Result = Source), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); -- If From <= Through, the returned string is -- Replace_Slice(Source, From, Through, ""); otherwise, it is Source with -- lower bound 1. @@ -1111,13 +1136,14 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - Pre => (if From <= Through - then (From in Source'Range - and then Through <= Source'Last)), + Pre => (if From <= Through + then (From in Source'Range + and then Through <= Source'Last)), -- Incomplete contract - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); -- Equivalent to: -- -- Move (Delete (Source, From, Through), @@ -1131,7 +1157,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 @@ -1156,7 +1182,8 @@ package Ada.Strings.Fixed with SPARK_Mode is else Index_Non_Blank (Source, Backward)); begin Trim'Result = Source (Low .. High))), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); -- 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 @@ -1171,7 +1198,8 @@ package Ada.Strings.Fixed with SPARK_Mode is -- Incomplete contract - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); -- Equivalent to: -- -- Move (Trim (Source, Side), Source, Justify=>Justify, Pad=>Pad). @@ -1208,7 +1236,8 @@ package Ada.Strings.Fixed with SPARK_Mode is Index (Source, Right, Outside, Backward); begin Trim'Result = Source (Low .. High))), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); -- Returns the string obtained by removing from Source all leading -- characters in Left and all trailing characters in Right. @@ -1222,7 +1251,8 @@ package Ada.Strings.Fixed with SPARK_Mode is -- Incomplete contract - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); -- Equivalent to: -- -- Move (Trim (Source, Left, Right), @@ -1259,7 +1289,8 @@ package Ada.Strings.Fixed with SPARK_Mode is and then Head'Result (Source'Length + 1 .. Count) = [1 .. Count - Source'Length => Pad]), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); -- 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. @@ -1273,7 +1304,8 @@ package Ada.Strings.Fixed with SPARK_Mode is -- Incomplete contract - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); -- Equivalent to: -- -- Move (Head (Source, Count, Pad), @@ -1322,7 +1354,8 @@ package Ada.Strings.Fixed with SPARK_Mode is and then Tail'Result (Count - Source'Length + 1 .. Tail'Result'Last) = Source)), - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); -- 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. @@ -1336,7 +1369,8 @@ package Ada.Strings.Fixed with SPARK_Mode is -- Incomplete contract - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); -- Equivalent to: -- -- Move (Tail (Source, Count, Pad), @@ -1350,7 +1384,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 @@ -1363,7 +1397,8 @@ 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; + Global => null, + Annotate => (GNATprove, Always_Return); function "*" (Left : Natural; @@ -1386,7 +1421,8 @@ 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; + Global => null, + Annotate => (GNATprove, Always_Return); -- 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 476f772bad7..1f228830527 100644 --- a/gcc/ada/libgnat/a-strmap.ads +++ b/gcc/ada/libgnat/a-strmap.ads @@ -54,6 +54,8 @@ 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 157c6f3ed6d..22a049247ed 100644 --- a/gcc/ada/libgnat/a-strsea.ads +++ b/gcc/ada/libgnat/a-strsea.ads @@ -52,6 +52,7 @@ with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; package Ada.Strings.Search with SPARK_Mode 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-strunb.ads b/gcc/ada/libgnat/a-strunb.ads index 37c946620aa..6997594e7bc 100644 --- a/gcc/ada/libgnat/a-strunb.ads +++ b/gcc/ada/libgnat/a-strunb.ads @@ -57,6 +57,7 @@ package Ada.Strings.Unbounded with Initial_Condition => Length (Null_Unbounded_String) = 0 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 8d00d0bedb0..e5be4540ad4 100644 --- a/gcc/ada/libgnat/a-strunb__shared.ads +++ b/gcc/ada/libgnat/a-strunb__shared.ads @@ -86,6 +86,7 @@ package Ada.Strings.Unbounded with Initial_Condition => Length (Null_Unbounded_String) = 0 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 7c2ec10cda5..447023d0c3f 100644 --- a/gcc/ada/libgnat/a-textio.ads +++ b/gcc/ada/libgnat/a-textio.ads @@ -101,14 +101,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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Open (File : in out File_Type; @@ -116,54 +117,63 @@ 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Close (File : in out File_Type) with - Pre => Is_Open (File), - Post => not Is_Open (File), - Global => (In_Out => File_System); + Pre => Is_Open (File), + Post => not Is_Open (File), + Global => (In_Out => File_System), + Annotate => (GNATprove, Always_Return); procedure Delete (File : in out File_Type) with - Pre => Is_Open (File), - Post => not Is_Open (File), - Global => (In_Out => File_System); + Pre => Is_Open (File), + Post => not Is_Open (File), + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); function Mode (File : File_Type) return File_Mode with - Pre => Is_Open (File), - Global => null; + Pre => Is_Open (File), + Global => null, + Annotate => (GNATprove, Always_Return); function Name (File : File_Type) return String with - Pre => Is_Open (File), - Global => null; + Pre => Is_Open (File), + Global => null, + Annotate => (GNATprove, Always_Return); function Form (File : File_Type) return String with - Pre => Is_Open (File), - Global => null; + Pre => Is_Open (File), + Global => null, + Annotate => (GNATprove, Always_Return); function Is_Open (File : File_Type) return Boolean with - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); ------------------------------------------------------ -- Control of default input, output and error files -- @@ -199,120 +209,142 @@ 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Always_Return); procedure Flush with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System); + Global => (In_Out => File_System), + Annotate => (GNATprove, Always_Return); -------------------------------------------- -- 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Set_Line_Length (To : Count) with - Post => + Post => Line_Length = To and Page_Length'Old = Page_Length, - Global => (In_Out => File_System); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Set_Page_Length (To : Count) with - Post => + Post => Page_Length = To and Line_Length'Old = Line_Length, - Global => (In_Out => File_System); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); function Line_Length (File : File_Type) return Count with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Global => (Input => File_System); + Pre => Is_Open (File) and then Mode (File) /= In_File, + Global => (Input => File_System); function Line_Length return Count with - Global => (Input => File_System); + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); function Page_Length (File : File_Type) return Count with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Global => (Input => File_System); + Pre => Is_Open (File) and then Mode (File) /= In_File, + Global => (Input => File_System); function Page_Length return Count with - Global => (Input => File_System); + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); ------------------------------------ -- Column, Line, and Page Control -- ------------------------------------ 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Always_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Always_Return); 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); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); function End_Of_Line (File : File_Type) return Boolean with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (Input => File_System); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); function End_Of_Line return Boolean with - Global => (Input => File_System); + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Always_Return); procedure New_Page with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System); + Global => (In_Out => File_System), + Annotate => (GNATprove, Always_Return); procedure Skip_Page (File : File_Type) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Skip_Page with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); function End_Of_Page (File : File_Type) return Boolean with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (Input => File_System); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); function End_Of_Page return Boolean with - Global => (Input => File_System); + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); function End_Of_File (File : File_Type) return Boolean with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (Input => File_System); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); function End_Of_File return Boolean with - Global => (Input => File_System); + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); procedure Set_Col (File : File_Type; To : Positive_Count) with Pre => @@ -325,13 +357,15 @@ is Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), others => True), - Global => (In_Out => File_System); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Set_Line (File : File_Type; To : Positive_Count) with Pre => @@ -344,149 +378,173 @@ is Line_Length (File)'Old = Line_Length (File) and Page_Length (File)'Old = Page_Length (File), others => True), - Global => (In_Out => File_System); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); function Col (File : File_Type) return Positive_Count with - Pre => Is_Open (File), - Global => (Input => File_System); + Pre => Is_Open (File), + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); function Col return Positive_Count with - Global => (Input => File_System); + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); function Line (File : File_Type) return Positive_Count with - Pre => Is_Open (File), - Global => (Input => File_System); + Pre => Is_Open (File), + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); function Line return Positive_Count with - Global => (Input => File_System); + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); function Page (File : File_Type) return Positive_Count with - Pre => Is_Open (File), - Global => (Input => File_System); + Pre => Is_Open (File), + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); function Page return Positive_Count with - Global => (Input => File_System); + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); ---------------------------- -- 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); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Get (Item : out Character) with Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Always_Return); procedure Put (Item : Character) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System); + Global => (In_Out => File_System), + Annotate => (GNATprove, Always_Return); 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); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); 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); + Global => (Input => File_System), + Annotate => (GNATprove, Always_Return); 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); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); ------------------------- -- 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); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Get (Item : out String) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Always_Return); procedure Put (Item : String) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System); + Global => (In_Out => File_System), + Annotate => (GNATprove, Always_Return); 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 + 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); function Get_Line (File : File_Type) return String with SPARK_Mode => Off; pragma Ada_05 (Get_Line); @@ -498,19 +556,21 @@ 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Always_Return); procedure Put_Line (Item : String) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System); + Global => (In_Out => File_System), + Annotate => (GNATprove, Always_Return); --------------------------------------- -- Generic packages for Input-Output -- diff --git a/gcc/ada/libgnat/a-tideio.ads b/gcc/ada/libgnat/a-tideio.ads index c5be4960515..4a2536d3cb1 100644 --- a/gcc/ada/libgnat/a-tideio.ads +++ b/gcc/ada/libgnat/a-tideio.ads @@ -54,17 +54,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); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Put (File : File_Type; @@ -73,11 +75,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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Put (Item : Num; @@ -85,17 +88,19 @@ 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Get (From : String; Item : out Num; Last : out Positive) with - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); procedure Put (To : out String; @@ -103,7 +108,8 @@ package Ada.Text_IO.Decimal_IO is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-tienio.ads b/gcc/ada/libgnat/a-tienio.ads index fb80abdf8ff..aac90f767ba 100644 --- a/gcc/ada/libgnat/a-tienio.ads +++ b/gcc/ada/libgnat/a-tienio.ads @@ -29,13 +29,15 @@ package Ada.Text_IO.Enumeration_IO is 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); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Get (Item : out Enum) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Put (File : File_Type; @@ -43,34 +45,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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Get (From : String; Item : out Enum; Last : out Positive) with - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); procedure Put (To : out String; Item : Enum; Set : Type_Set := Default_Setting) with - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); end Ada.Text_IO.Enumeration_IO; diff --git a/gcc/ada/libgnat/a-tifiio.ads b/gcc/ada/libgnat/a-tifiio.ads index 8a3886d30e6..bbf8e90ffef 100644 --- a/gcc/ada/libgnat/a-tifiio.ads +++ b/gcc/ada/libgnat/a-tifiio.ads @@ -34,17 +34,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); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Put (File : File_Type; @@ -53,11 +55,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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Put (Item : Num; @@ -65,17 +68,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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Get (From : String; Item : out Num; Last : out Positive) with - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); procedure Put (To : out String; @@ -83,7 +88,8 @@ package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-tiflio.ads b/gcc/ada/libgnat/a-tiflio.ads index 2760b0f0e81..032c6b2f162 100644 --- a/gcc/ada/libgnat/a-tiflio.ads +++ b/gcc/ada/libgnat/a-tiflio.ads @@ -54,17 +54,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); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Put (File : File_Type; @@ -73,11 +75,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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Put (Item : Num; @@ -85,17 +88,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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Get (From : String; Item : out Num; Last : out Positive) with - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); procedure Put (To : out String; @@ -103,7 +108,8 @@ package Ada.Text_IO.Float_IO with SPARK_Mode => On is Aft : Field := Default_Aft; Exp : Field := Default_Exp) with - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-tiinio.ads b/gcc/ada/libgnat/a-tiinio.ads index 77efd46feb5..491bc2f32d8 100644 --- a/gcc/ada/libgnat/a-tiinio.ads +++ b/gcc/ada/libgnat/a-tiinio.ads @@ -53,17 +53,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); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Put (File : File_Type; @@ -71,35 +73,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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Get (From : String; Item : out Num; Last : out Positive) with - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); procedure Put (To : out String; Item : Num; Base : Number_Base := Default_Base) with - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-timoio.ads b/gcc/ada/libgnat/a-timoio.ads index 8c28a0a1ee7..67ff7c6ba28 100644 --- a/gcc/ada/libgnat/a-timoio.ads +++ b/gcc/ada/libgnat/a-timoio.ads @@ -53,17 +53,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); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Put (File : File_Type; @@ -71,35 +73,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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); 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); + Global => (In_Out => File_System), + Annotate => (GNATprove, Might_Not_Return); procedure Get (From : String; Item : out Num; Last : out Positive) with - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); procedure Put (To : out String; Item : Num; Base : Number_Base := Default_Base) with - Global => null; + Global => null, + Annotate => (GNATprove, Might_Not_Return); private pragma Inline (Get); diff --git a/gcc/ada/libgnat/i-c.ads b/gcc/ada/libgnat/i-c.ads index 2023b753dfd..70139023dc3 100644 --- a/gcc/ada/libgnat/i-c.ads +++ b/gcc/ada/libgnat/i-c.ads @@ -29,6 +29,8 @@ with System.Parameters; package Interfaces.C with SPARK_Mode, Pure is + pragma Annotate (GNATprove, Always_Return, C); + -- Each of the types declared in Interfaces.C is C-compatible. -- The types int, short, long, unsigned, ptrdiff_t, size_t, double, diff --git a/gcc/ada/libgnat/interfac.ads b/gcc/ada/libgnat/interfac.ads index b12ced8c764..b269869fd4e 100644 --- a/gcc/ada/libgnat/interfac.ads +++ b/gcc/ada/libgnat/interfac.ads @@ -38,6 +38,7 @@ package Interfaces 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 579e8b49ed6..becd18069eb 100644 --- a/gcc/ada/libgnat/interfac__2020.ads +++ b/gcc/ada/libgnat/interfac__2020.ads @@ -38,6 +38,7 @@ package Interfaces 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-atacco.ads b/gcc/ada/libgnat/s-atacco.ads index b3559ffed79..a928d47ef46 100644 --- a/gcc/ada/libgnat/s-atacco.ads +++ b/gcc/ada/libgnat/s-atacco.ads @@ -55,9 +55,11 @@ package System.Address_To_Access_Conversions is -- of no strict aliasing. function To_Pointer (Value : Address) return Object_Pointer with - Global => null; + Global => null, + Annotate => (GNATprove, Always_Return); function To_Address (Value : Object_Pointer) return Address with - SPARK_Mode => Off; + SPARK_Mode => Off, + Annotate => (GNATprove, Always_Return); pragma Import (Intrinsic, To_Pointer); pragma Import (Intrinsic, To_Address); diff --git a/gcc/ada/libgnat/s-stoele.ads b/gcc/ada/libgnat/s-stoele.ads index 48af71b1dde..d0473682f7e 100644 --- a/gcc/ada/libgnat/s-stoele.ads +++ b/gcc/ada/libgnat/s-stoele.ads @@ -43,6 +43,8 @@ package System.Storage_Elements is -- this unit Pure instead of Preelaborable; see RM 13.7.1(15). In Ada 2005, -- this is Pure in any case (AI-362). + pragma Annotate (GNATprove, Always_Return, Storage_Elements); + -- We also add the pragma Pure_Function to the operations in this package, -- because otherwise functions with parameters derived from Address are -- treated as non-pure by the back-end (see exp_ch6.adb). This is because