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.

36 files changed, 395 insertions, 461 deletions

diff --git a/gcc/ada/libgnarl/a-reatim.ads b/gcc/ada/libgnarl/a-reatim.ads
index c5009d2..a616d57 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 159cd70..89b2d68 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 f83bf52..382a7b6 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 ffb96d4..c4d74ee 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 350d049..d342eeb 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 f6d6c96..444d1a3 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 b3afd1f..10b33e9 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 e137c67..7089fc3 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 6797efd..10b04ac 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 d4fe745..149939b 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 1e4a366..ea0cc3f 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 0838d59..9d5e9d9 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 73dd3d9..a070da0 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 5651bdc..df1b342 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 2e0cd98..339cb17 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 d3e88d0..be76ad2 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 3f5d56e..2da9dc7 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 9cedab6..ddbbd85 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 b62d251..7f8fa19 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 aac90f7..e4cdaee 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 bbf8e90..0e3e71c 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 82ff84b..fcfa76a 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 0299cc0..60f21cc 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 c8554b8..40d91ed 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 b6598b5..ea65c73 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 70af56a..fe87fba 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 49b1f13..e486f03 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 edd3f36..bc37a8e 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 89557bf..70d82be 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 0414785..66ace80 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 219523b..d19b9e1 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 bd920cc..157ca52 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 daf550b6..642ded7 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 7de150d..d5d7042 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 28efced..e74202d7 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 960ad8e..bdd97b5 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;