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