public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-1624] [Ada] Annotate libraries with returning annotation
@ 2022-07-12 12:25 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-07-12 12:25 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:a31eda15463b00bad7c48d973e4e7e8a33006379
commit r13-1624-ga31eda15463b00bad7c48d973e4e7e8a33006379
Author: Joffrey Huguet <huguet@adacore.com>
Date: Mon Jun 13 11:44:51 2022 +0200
[Ada] Annotate libraries with returning annotation
This patch annotates SPARK-annotated libraries with returning
annotations (Always_Return, Might_Not_Return) to remove the warnings
raised by GNATprove about missing annotations.
gcc/ada/
* libgnarl/a-reatim.ads, libgnat/a-cfdlli.ads,
libgnat/a-cfhama.ads, libgnat/a-cfhase.ads,
libgnat/a-cfinse.ads, libgnat/a-cfinve.ads,
libgnat/a-cforma.ads, libgnat/a-cforse.ads,
libgnat/a-chahan.ads, libgnat/a-cofove.ads,
libgnat/a-cofuma.ads, libgnat/a-cofuse.ads,
libgnat/a-cofuve.ads, libgnat/a-nbnbin.ads,
libgnat/a-nbnbre.ads, libgnat/a-ngelfu.ads,
libgnat/a-nlelfu.ads, libgnat/a-nllefu.ads,
libgnat/a-nselfu.ads, libgnat/a-nuelfu.ads,
libgnat/a-strbou.ads, libgnat/a-strfix.ads,
libgnat/a-strmap.ads, libgnat/a-strunb.ads,
libgnat/a-strunb__shared.ads, libgnat/a-strsea.ads,
libgnat/a-textio.ads, libgnat/a-tideio.ads,
libgnat/a-tienio.ads, libgnat/a-tifiio.ads,
libgnat/a-tiflio.ads, libgnat/a-tiinio.ads,
libgnat/a-timoio.ads, libgnat/i-c.ads, libgnat/interfac.ads,
libgnat/interfac__2020.ads, libgnat/s-atacco.ads,
libgnat/s-stoele.ads: Annotate packages and subprograms with
returning annotations.
Diff:
---
gcc/ada/libgnarl/a-reatim.ads | 1 +
gcc/ada/libgnat/a-cfdlli.ads | 4 +-
gcc/ada/libgnat/a-cfhama.ads | 4 +-
gcc/ada/libgnat/a-cfhase.ads | 4 +-
gcc/ada/libgnat/a-cfinse.ads | 5 +-
gcc/ada/libgnat/a-cfinve.ads | 4 +-
gcc/ada/libgnat/a-cforma.ads | 4 +-
gcc/ada/libgnat/a-cforse.ads | 4 +-
gcc/ada/libgnat/a-chahan.ads | 2 +
gcc/ada/libgnat/a-cofove.ads | 2 +
gcc/ada/libgnat/a-cofuma.ads | 5 +-
gcc/ada/libgnat/a-cofuse.ads | 5 +-
gcc/ada/libgnat/a-cofuve.ads | 5 +-
gcc/ada/libgnat/a-nbnbin.ads | 2 +
gcc/ada/libgnat/a-nbnbre.ads | 2 +
gcc/ada/libgnat/a-ngelfu.ads | 1 +
gcc/ada/libgnat/a-nlelfu.ads | 1 +
gcc/ada/libgnat/a-nllefu.ads | 1 +
gcc/ada/libgnat/a-nselfu.ads | 1 +
gcc/ada/libgnat/a-nuelfu.ads | 1 +
gcc/ada/libgnat/a-strbou.ads | 2 +
gcc/ada/libgnat/a-strfix.ads | 138 +++++++++------
gcc/ada/libgnat/a-strmap.ads | 2 +
gcc/ada/libgnat/a-strsea.ads | 1 +
gcc/ada/libgnat/a-strunb.ads | 1 +
gcc/ada/libgnat/a-strunb__shared.ads | 1 +
gcc/ada/libgnat/a-textio.ads | 318 +++++++++++++++++++++--------------
gcc/ada/libgnat/a-tideio.ads | 28 +--
gcc/ada/libgnat/a-tienio.ads | 28 +--
gcc/ada/libgnat/a-tifiio.ads | 28 +--
gcc/ada/libgnat/a-tiflio.ads | 28 +--
gcc/ada/libgnat/a-tiinio.ads | 28 +--
gcc/ada/libgnat/a-timoio.ads | 28 +--
gcc/ada/libgnat/i-c.ads | 2 +
gcc/ada/libgnat/interfac.ads | 1 +
gcc/ada/libgnat/interfac__2020.ads | 1 +
gcc/ada/libgnat/s-atacco.ads | 6 +-
gcc/ada/libgnat/s-stoele.ads | 2 +
38 files changed, 443 insertions(+), 258 deletions(-)
diff --git a/gcc/ada/libgnarl/a-reatim.ads b/gcc/ada/libgnarl/a-reatim.ads
index 4b8f7aab259..dee20e99f4b 100644
--- a/gcc/ada/libgnarl/a-reatim.ads
+++ b/gcc/ada/libgnarl/a-reatim.ads
@@ -41,6 +41,7 @@ package Ada.Real_Time with
Abstract_State => (Clock_Time with Synchronous),
Initializes => Clock_Time
is
+ pragma Annotate (GNATprove, Always_Return, Real_Time);
pragma Compile_Time_Error
(Duration'Size /= 64,
diff --git a/gcc/ada/libgnat/a-cfdlli.ads b/gcc/ada/libgnat/a-cfdlli.ads
index ff7d2d81aca..01e7db29132 100644
--- a/gcc/ada/libgnat/a-cfdlli.ads
+++ b/gcc/ada/libgnat/a-cfdlli.ads
@@ -37,8 +37,10 @@ generic
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Doubly_Linked_Lists with
- SPARK_Mode
+ SPARK_Mode,
+ Annotate => (GNATprove, Always_Return)
is
+
-- Contracts in this unit are meant for analysis only, not for run-time
-- checking.
diff --git a/gcc/ada/libgnat/a-cfhama.ads b/gcc/ada/libgnat/a-cfhama.ads
index bf1e85f3ab8..8cb7488f183 100644
--- a/gcc/ada/libgnat/a-cfhama.ads
+++ b/gcc/ada/libgnat/a-cfhama.ads
@@ -62,8 +62,10 @@ generic
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Hashed_Maps with
- SPARK_Mode
+ SPARK_Mode,
+ Annotate => (GNATprove, Always_Return)
is
+
-- Contracts in this unit are meant for analysis only, not for run-time
-- checking.
diff --git a/gcc/ada/libgnat/a-cfhase.ads b/gcc/ada/libgnat/a-cfhase.ads
index 80ce9485b2d..248a0ac9234 100644
--- a/gcc/ada/libgnat/a-cfhase.ads
+++ b/gcc/ada/libgnat/a-cfhase.ads
@@ -62,8 +62,10 @@ generic
Right : Element_Type) return Boolean is "=";
package Ada.Containers.Formal_Hashed_Sets with
- SPARK_Mode
+ SPARK_Mode,
+ Annotate => (GNATprove, Always_Return)
is
+
-- Contracts in this unit are meant for analysis only, not for run-time
-- checking.
diff --git a/gcc/ada/libgnat/a-cfinse.ads b/gcc/ada/libgnat/a-cfinse.ads
index cff2900e71f..d7fdb0426cc 100644
--- a/gcc/ada/libgnat/a-cfinse.ads
+++ b/gcc/ada/libgnat/a-cfinse.ads
@@ -38,7 +38,10 @@ generic
type Element_Type (<>) is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
-package Ada.Containers.Functional_Infinite_Sequences with SPARK_Mode is
+package Ada.Containers.Functional_Infinite_Sequences with
+ SPARK_Mode,
+ Annotate => (GNATprove, Always_Return)
+is
type Sequence is private
with Default_Initial_Condition => Length (Sequence) = 0,
diff --git a/gcc/ada/libgnat/a-cfinve.ads b/gcc/ada/libgnat/a-cfinve.ads
index b5fa29bf7b1..f44e45b8171 100644
--- a/gcc/ada/libgnat/a-cfinve.ads
+++ b/gcc/ada/libgnat/a-cfinve.ads
@@ -53,8 +53,10 @@ generic
-- grow via heap allocation.
package Ada.Containers.Formal_Indefinite_Vectors with
- SPARK_Mode => On
+ SPARK_Mode,
+ Annotate => (GNATprove, Always_Return)
is
+
-- Contracts in this unit are meant for analysis only, not for run-time
-- checking.
diff --git a/gcc/ada/libgnat/a-cforma.ads b/gcc/ada/libgnat/a-cforma.ads
index 1e3c57b1c9c..7be2eec4ae7 100644
--- a/gcc/ada/libgnat/a-cforma.ads
+++ b/gcc/ada/libgnat/a-cforma.ads
@@ -61,8 +61,10 @@ generic
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Ordered_Maps with
- SPARK_Mode
+ SPARK_Mode,
+ Annotate => (GNATprove, Always_Return)
is
+
-- Contracts in this unit are meant for analysis only, not for run-time
-- checking.
diff --git a/gcc/ada/libgnat/a-cforse.ads b/gcc/ada/libgnat/a-cforse.ads
index f6a033f680f..ff96d8e7547 100644
--- a/gcc/ada/libgnat/a-cforse.ads
+++ b/gcc/ada/libgnat/a-cforse.ads
@@ -59,8 +59,10 @@ generic
with function "<" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Ordered_Sets with
- SPARK_Mode
+ SPARK_Mode,
+ Annotate => (GNATprove, Always_Return)
is
+
-- Contracts in this unit are meant for analysis only, not for run-time
-- checking.
diff --git a/gcc/ada/libgnat/a-chahan.ads b/gcc/ada/libgnat/a-chahan.ads
index e98cda351df..dc1a629cf2a 100644
--- a/gcc/ada/libgnat/a-chahan.ads
+++ b/gcc/ada/libgnat/a-chahan.ads
@@ -46,6 +46,8 @@ is
pragma Pure;
-- In accordance with Ada 2005 AI-362
+ pragma Annotate (GNATprove, Always_Return, Handling);
+
----------------------------------------
-- Character Classification Functions --
----------------------------------------
diff --git a/gcc/ada/libgnat/a-cofove.ads b/gcc/ada/libgnat/a-cofove.ads
index cba10a63746..64133750f29 100644
--- a/gcc/ada/libgnat/a-cofove.ads
+++ b/gcc/ada/libgnat/a-cofove.ads
@@ -45,6 +45,8 @@ generic
package Ada.Containers.Formal_Vectors with
SPARK_Mode
is
+ pragma Annotate (GNATprove, Always_Return, Formal_Vectors);
+
-- Contracts in this unit are meant for analysis only, not for run-time
-- checking.
diff --git a/gcc/ada/libgnat/a-cofuma.ads b/gcc/ada/libgnat/a-cofuma.ads
index d01c4b4dd22..f863cdc979f 100644
--- a/gcc/ada/libgnat/a-cofuma.ads
+++ b/gcc/ada/libgnat/a-cofuma.ads
@@ -49,7 +49,10 @@ generic
-- of equivalence over keys is needed, that is, Equivalent_Keys defines a
-- key uniquely.
-package Ada.Containers.Functional_Maps with SPARK_Mode is
+package Ada.Containers.Functional_Maps with
+ SPARK_Mode,
+ Annotate => (GNATprove, Always_Return)
+is
type Map is private with
Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0,
diff --git a/gcc/ada/libgnat/a-cofuse.ads b/gcc/ada/libgnat/a-cofuse.ads
index 29f1e9f979f..ce52f613f07 100644
--- a/gcc/ada/libgnat/a-cofuse.ads
+++ b/gcc/ada/libgnat/a-cofuse.ads
@@ -47,7 +47,10 @@ generic
-- of equivalence over elements is needed, that is, Equivalent_Elements
-- defines an element uniquely.
-package Ada.Containers.Functional_Sets with SPARK_Mode is
+package Ada.Containers.Functional_Sets with
+ SPARK_Mode,
+ Annotate => (GNATprove, Always_Return)
+is
type Set is private with
Default_Initial_Condition => Is_Empty (Set),
diff --git a/gcc/ada/libgnat/a-cofuve.ads b/gcc/ada/libgnat/a-cofuve.ads
index f926a963737..86222217af5 100644
--- a/gcc/ada/libgnat/a-cofuve.ads
+++ b/gcc/ada/libgnat/a-cofuve.ads
@@ -40,7 +40,10 @@ generic
type Element_Type (<>) is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
-package Ada.Containers.Functional_Vectors with SPARK_Mode is
+package Ada.Containers.Functional_Vectors with
+ SPARK_Mode,
+ Annotate => (GNATprove, Always_Return)
+is
subtype Extended_Index is Index_Type'Base range
Index_Type'Pred (Index_Type'First) .. Index_Type'Last;
diff --git a/gcc/ada/libgnat/a-nbnbin.ads b/gcc/ada/libgnat/a-nbnbin.ads
index 1ba10da6a0d..ffb96d4d98b 100644
--- a/gcc/ada/libgnat/a-nbnbin.ads
+++ b/gcc/ada/libgnat/a-nbnbin.ads
@@ -21,6 +21,8 @@ private with System;
package Ada.Numerics.Big_Numbers.Big_Integers
with Preelaborate
is
+ pragma Annotate (GNATprove, Always_Return, Big_Integers);
+
type Big_Integer is private
with Integer_Literal => From_Universal_Image,
Put_Image => Put_Image;
diff --git a/gcc/ada/libgnat/a-nbnbre.ads b/gcc/ada/libgnat/a-nbnbre.ads
index 4118d2bb99c..350d0497ed4 100644
--- a/gcc/ada/libgnat/a-nbnbre.ads
+++ b/gcc/ada/libgnat/a-nbnbre.ads
@@ -20,6 +20,8 @@ with Ada.Strings.Text_Buffers; use Ada.Strings.Text_Buffers;
package Ada.Numerics.Big_Numbers.Big_Reals
with Preelaborate
is
+ pragma Annotate (GNATprove, Always_Return, Big_Reals);
+
type Big_Real is private with
Real_Literal => From_Universal_Image,
Put_Image => Put_Image;
diff --git a/gcc/ada/libgnat/a-ngelfu.ads b/gcc/ada/libgnat/a-ngelfu.ads
index c8a31bb494d..75783ef44a4 100644
--- a/gcc/ada/libgnat/a-ngelfu.ads
+++ b/gcc/ada/libgnat/a-ngelfu.ads
@@ -40,6 +40,7 @@ package Ada.Numerics.Generic_Elementary_Functions with
SPARK_Mode => On
is
pragma Pure;
+ pragma Annotate (GNATprove, Always_Return, Generic_Elementary_Functions);
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised when calling
diff --git a/gcc/ada/libgnat/a-nlelfu.ads b/gcc/ada/libgnat/a-nlelfu.ads
index 10b33e9cb3c..b3afd1fc997 100644
--- a/gcc/ada/libgnat/a-nlelfu.ads
+++ b/gcc/ada/libgnat/a-nlelfu.ads
@@ -19,3 +19,4 @@ package Ada.Numerics.Long_Elementary_Functions is
new Ada.Numerics.Generic_Elementary_Functions (Long_Float);
pragma Pure (Long_Elementary_Functions);
+pragma Annotate (GNATprove, Always_Return, Long_Elementary_Functions);
diff --git a/gcc/ada/libgnat/a-nllefu.ads b/gcc/ada/libgnat/a-nllefu.ads
index 7089fc3efb0..e137c67e786 100644
--- a/gcc/ada/libgnat/a-nllefu.ads
+++ b/gcc/ada/libgnat/a-nllefu.ads
@@ -19,3 +19,4 @@ package Ada.Numerics.Long_Long_Elementary_Functions is
new Ada.Numerics.Generic_Elementary_Functions (Long_Long_Float);
pragma Pure (Long_Long_Elementary_Functions);
+pragma Annotate (GNATprove, Always_Return, Long_Long_Elementary_Functions);
diff --git a/gcc/ada/libgnat/a-nselfu.ads b/gcc/ada/libgnat/a-nselfu.ads
index 10b04acdeb9..6797efd70e9 100644
--- a/gcc/ada/libgnat/a-nselfu.ads
+++ b/gcc/ada/libgnat/a-nselfu.ads
@@ -19,3 +19,4 @@ package Ada.Numerics.Short_Elementary_Functions is
new Ada.Numerics.Generic_Elementary_Functions (Short_Float);
pragma Pure (Short_Elementary_Functions);
+pragma Annotate (GNATprove, Always_Return, Short_Elementary_Functions);
diff --git a/gcc/ada/libgnat/a-nuelfu.ads b/gcc/ada/libgnat/a-nuelfu.ads
index 149939babea..d4fe74572f6 100644
--- a/gcc/ada/libgnat/a-nuelfu.ads
+++ b/gcc/ada/libgnat/a-nuelfu.ads
@@ -19,3 +19,4 @@ package Ada.Numerics.Elementary_Functions is
new Ada.Numerics.Generic_Elementary_Functions (Float);
pragma Pure (Elementary_Functions);
+pragma Annotate (GNATprove, Always_Return, Elementary_Functions);
diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads
index 839760ac26a..678c3454e4e 100644
--- a/gcc/ada/libgnat/a-strbou.ads
+++ b/gcc/ada/libgnat/a-strbou.ads
@@ -49,6 +49,7 @@ with Ada.Strings.Search;
package Ada.Strings.Bounded with SPARK_Mode is
pragma Preelaborate;
+ pragma Annotate (GNATprove, Always_Return, Bounded);
generic
Max : Positive;
@@ -68,6 +69,7 @@ package Ada.Strings.Bounded with SPARK_Mode is
Post => Ignore,
Contract_Cases => Ignore,
Ghost => Ignore);
+ pragma Annotate (GNATprove, Always_Return, Generic_Bounded_Length);
Max_Length : constant Positive := Max;
diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads
index 0d6c5d07663..dee64ab9e0e 100644
--- a/gcc/ada/libgnat/a-strfix.ads
+++ b/gcc/ada/libgnat/a-strfix.ads
@@ -63,7 +63,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- The Move procedure copies characters from Source to Target. If Source
-- has the same length as Target, then the effect is to assign Source to
-- Target. If Source is shorter than Target then:
@@ -168,7 +169,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
others
=>
Index'Result = 0),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
pragma Ada_05 (Index);
function Index
@@ -231,7 +233,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
others
=>
Index'Result = 0),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
pragma Ada_05 (Index);
-- Each Index function searches, starting from From, for a slice of
@@ -300,7 +303,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
others
=>
Index'Result = 0),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
function Index
(Source : String;
@@ -355,7 +359,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
others
=>
Index'Result = 0),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- If Going = Forward, returns:
--
@@ -408,7 +413,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
and then (J < Index'Result) = (Going = Forward)
then (Test = Inside)
/= Ada.Strings.Maps.Is_In (Source (J), Set)))),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
function Index
(Source : String;
@@ -464,7 +470,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
or else (J > From) = (Going = Forward))
then (Test = Inside)
/= Ada.Strings.Maps.Is_In (Source (J), Set)))),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
pragma Ada_05 (Index);
-- Index searches for the first or last occurrence of any of a set of
-- characters (when Test=Inside), or any of the complement of a set of
@@ -524,7 +531,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
and then (J = From or else (J > From)
= (Going = Forward))
then Source (J) = ' '))),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
pragma Ada_05 (Index_Non_Blank);
-- Returns Index (Source, Maps.To_Set(Space), From, Outside, Going)
@@ -562,7 +570,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
and then (J < Index_Non_Blank'Result)
= (Going = Forward)
then Source (J) = ' '))),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- Returns Index (Source, Maps.To_Set(Space), Outside, Going)
function Count
@@ -570,16 +579,18 @@ package Ada.Strings.Fixed with SPARK_Mode is
Pattern : String;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
with
- Pre => Pattern'Length /= 0,
- Global => null;
+ Pre => Pattern'Length /= 0,
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
function Count
(Source : String;
Pattern : String;
Mapping : Maps.Character_Mapping_Function) return Natural
with
- Pre => Pattern'Length /= 0 and then Mapping /= null,
- Global => null;
+ Pre => Pattern'Length /= 0 and then Mapping /= null,
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- Returns the maximum number of nonoverlapping slices of Source that match
-- Pattern with respect to Mapping. If Pattern is the null string then
@@ -589,7 +600,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
(Source : String;
Set : Maps.Character_Set) return Natural
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- Returns the number of occurrences in Source of characters that are in
-- Set.
@@ -647,7 +659,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
then
(Test = Inside)
/= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
pragma Ada_2012 (Find_Token);
-- If Source is not the null string and From is not in Source'Range, then
-- Index_Error is raised. Otherwise, First is set to the index of the first
@@ -709,7 +722,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
then
(Test = Inside)
/= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- Equivalent to Find_Token (Source, Set, Source'First, Test, First, Last)
------------------------------------
@@ -738,7 +752,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
(for all J in Source'Range =>
Translate'Result (J - Source'First + 1)
= Mapping (Source (J))),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
function Translate
(Source : String;
@@ -761,7 +776,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
(for all J in Source'Range =>
Translate'Result (J - Source'First + 1)
= Ada.Strings.Maps.Value (Mapping, Source (J))),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- Returns the string S whose length is Source'Length and such that S (I)
-- is the character to which Mapping maps the corresponding element of
@@ -771,27 +787,29 @@ package Ada.Strings.Fixed with SPARK_Mode is
(Source : in out String;
Mapping : Maps.Character_Mapping_Function)
with
- Pre => Mapping /= null,
- Post =>
+ Pre => Mapping /= null,
+ Post =>
-- Each character in Source after the call is the translation of the
-- character at the same position before the call, through Mapping.
(for all J in Source'Range => Source (J) = Mapping (Source'Old (J))),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
procedure Translate
(Source : in out String;
Mapping : Maps.Character_Mapping)
with
- Post =>
+ Post =>
-- Each character in Source after the call is the translation of the
-- character at the same position before the call, through Mapping.
(for all J in Source'Range =>
Source (J) = Ada.Strings.Maps.Value (Mapping, Source'Old (J))),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- Equivalent to Source := Translate(Source, Mapping)
@@ -884,7 +902,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
(Low - Source'First + By'Length + 1
.. Replace_Slice'Result'Last)
= Source (Low .. Source'Last))),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- If Low > Source'Last + 1, or High < Source'First - 1, then Index_Error
-- is propagated. Otherwise:
--
@@ -904,7 +923,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
Justify : Alignment := Left;
Pad : Character := Space)
with
- Pre =>
+ Pre =>
Low - 1 <= Source'Last
and then High >= Source'First - 1
and then (if High >= Low
@@ -916,7 +935,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Replace_Slice (Source, Low, High, By),
@@ -962,7 +982,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
(Before - Source'First + New_Item'Length + 1
.. Insert'Result'Last)
= Source (Before .. Source'Last)),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- Propagates Index_Error if Before is not in
-- Source'First .. Source'Last + 1; otherwise, returns
-- Source (Source'First .. Before - 1)
@@ -974,13 +995,14 @@ package Ada.Strings.Fixed with SPARK_Mode is
New_Item : String;
Drop : Truncation := Error)
with
- Pre =>
+ Pre =>
Before - 1 in Source'First - 1 .. Source'Last
and then Source'Length <= Natural'Last - New_Item'Length,
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to Move (Insert (Source, Before, New_Item), Source, Drop)
function Overwrite
@@ -988,13 +1010,13 @@ package Ada.Strings.Fixed with SPARK_Mode is
Position : Positive;
New_Item : String) return String
with
- Pre =>
+ Pre =>
Position - 1 in Source'First - 1 .. Source'Last
and then
(if Position - Source'First >= Source'Length - New_Item'Length
then Position - Source'First <= Natural'Last - New_Item'Length),
- Post =>
+ Post =>
-- Lower bound of the returned string is 1
@@ -1029,7 +1051,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
(Position - Source'First + New_Item'Length + 1
.. Overwrite'Result'Last)
= Source (Position + New_Item'Length .. Source'Last)),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- Propagates Index_Error if Position is not in
-- Source'First .. Source'Last + 1; otherwise, returns the string obtained
-- from Source by consecutively replacing characters starting at Position
@@ -1043,7 +1066,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
New_Item : String;
Drop : Truncation := Right)
with
- Pre =>
+ Pre =>
Position - 1 in Source'First - 1 .. Source'Last
and then
(if Position - Source'First >= Source'Length - New_Item'Length
@@ -1051,7 +1074,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to Move(Overwrite(Source, Position, New_Item), Source, Drop)
function Delete
@@ -1099,7 +1123,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
others =>
Delete'Result'Length = Source'Length
and then Delete'Result = Source),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- If From <= Through, the returned string is
-- Replace_Slice(Source, From, Through, ""); otherwise, it is Source with
-- lower bound 1.
@@ -1111,13 +1136,14 @@ package Ada.Strings.Fixed with SPARK_Mode is
Justify : Alignment := Left;
Pad : Character := Space)
with
- Pre => (if From <= Through
- then (From in Source'Range
- and then Through <= Source'Last)),
+ Pre => (if From <= Through
+ then (From in Source'Range
+ and then Through <= Source'Last)),
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Delete (Source, From, Through),
@@ -1131,7 +1157,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
(Source : String;
Side : Trim_End) return String
with
- Post =>
+ Post =>
-- Lower bound of the returned string is 1
@@ -1156,7 +1182,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
else Index_Non_Blank (Source, Backward));
begin
Trim'Result = Source (Low .. High))),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- Returns the string obtained by removing from Source all leading Space
-- characters (if Side = Left), all trailing Space characters (if
-- Side = Right), or all leading and trailing Space characters (if
@@ -1171,7 +1198,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Trim (Source, Side), Source, Justify=>Justify, Pad=>Pad).
@@ -1208,7 +1236,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
Index (Source, Right, Outside, Backward);
begin
Trim'Result = Source (Low .. High))),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- Returns the string obtained by removing from Source all leading
-- characters in Left and all trailing characters in Right.
@@ -1222,7 +1251,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Trim (Source, Left, Right),
@@ -1259,7 +1289,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
and then
Head'Result (Source'Length + 1 .. Count)
= [1 .. Count - Source'Length => Pad]),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- Returns a string of length Count. If Count <= Source'Length, the string
-- comprises the first Count characters of Source. Otherwise, its contents
-- are Source concatenated with Count - Source'Length Pad characters.
@@ -1273,7 +1304,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Head (Source, Count, Pad),
@@ -1322,7 +1354,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
and then
Tail'Result (Count - Source'Length + 1 .. Tail'Result'Last)
= Source)),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- Returns a string of length Count. If Count <= Source'Length, the string
-- comprises the last Count characters of Source. Otherwise, its contents
-- are Count-Source'Length Pad characters concatenated with Source.
@@ -1336,7 +1369,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Tail (Source, Count, Pad),
@@ -1350,7 +1384,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
(Left : Natural;
Right : Character) return String
with
- Post =>
+ Post =>
-- Lower bound of the returned string is 1
@@ -1363,7 +1397,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
-- All characters of the returned string are Right
and then (for all C of "*"'Result => C = Right),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
function "*"
(Left : Natural;
@@ -1386,7 +1421,8 @@ package Ada.Strings.Fixed with SPARK_Mode is
and then
(for all K in "*"'Result'Range =>
"*"'Result (K) = Right (Right'First + (K - 1) mod Right'Length)),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- These functions replicate a character or string a specified number of
-- times. The first function returns a string whose length is Left and each
diff --git a/gcc/ada/libgnat/a-strmap.ads b/gcc/ada/libgnat/a-strmap.ads
index 476f772bad7..1f228830527 100644
--- a/gcc/ada/libgnat/a-strmap.ads
+++ b/gcc/ada/libgnat/a-strmap.ads
@@ -54,6 +54,8 @@ is
pragma Pure;
-- In accordance with Ada 2005 AI-362
+ pragma Annotate (GNATprove, Always_Return, Maps);
+
--------------------------------
-- Character Set Declarations --
--------------------------------
diff --git a/gcc/ada/libgnat/a-strsea.ads b/gcc/ada/libgnat/a-strsea.ads
index 157c6f3ed6d..22a049247ed 100644
--- a/gcc/ada/libgnat/a-strsea.ads
+++ b/gcc/ada/libgnat/a-strsea.ads
@@ -52,6 +52,7 @@ with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
package Ada.Strings.Search with SPARK_Mode is
pragma Preelaborate;
+ pragma Annotate (GNATprove, Always_Return, Search);
-- The ghost function Match tells whether the slice of Source starting at
-- From and of length Pattern'Length matches with Pattern with respect to
diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads
index 37c946620aa..6997594e7bc 100644
--- a/gcc/ada/libgnat/a-strunb.ads
+++ b/gcc/ada/libgnat/a-strunb.ads
@@ -57,6 +57,7 @@ package Ada.Strings.Unbounded with
Initial_Condition => Length (Null_Unbounded_String) = 0
is
pragma Preelaborate;
+ pragma Annotate (GNATprove, Always_Return, Unbounded);
type Unbounded_String is private with
Default_Initial_Condition => Length (Unbounded_String) = 0;
diff --git a/gcc/ada/libgnat/a-strunb__shared.ads b/gcc/ada/libgnat/a-strunb__shared.ads
index 8d00d0bedb0..e5be4540ad4 100644
--- a/gcc/ada/libgnat/a-strunb__shared.ads
+++ b/gcc/ada/libgnat/a-strunb__shared.ads
@@ -86,6 +86,7 @@ package Ada.Strings.Unbounded with
Initial_Condition => Length (Null_Unbounded_String) = 0
is
pragma Preelaborate;
+ pragma Annotate (GNATprove, Always_Return, Unbounded);
type Unbounded_String is private with
Default_Initial_Condition => Length (Unbounded_String) = 0;
diff --git a/gcc/ada/libgnat/a-textio.ads b/gcc/ada/libgnat/a-textio.ads
index 7c2ec10cda5..447023d0c3f 100644
--- a/gcc/ada/libgnat/a-textio.ads
+++ b/gcc/ada/libgnat/a-textio.ads
@@ -101,14 +101,15 @@ is
Name : String := "";
Form : String := "")
with
- Pre => not Is_Open (File),
- Post =>
+ Pre => not Is_Open (File),
+ Post =>
Is_Open (File)
and then Ada.Text_IO.Mode (File) = Mode
and then (if Mode /= In_File
then (Line_Length (File) = 0
and then Page_Length (File) = 0)),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Open
(File : in out File_Type;
@@ -116,54 +117,63 @@ is
Name : String;
Form : String := "")
with
- Pre => not Is_Open (File),
- Post =>
+ Pre => not Is_Open (File),
+ Post =>
Is_Open (File)
and then Ada.Text_IO.Mode (File) = Mode
and then (if Mode /= In_File
then (Line_Length (File) = 0
and then Page_Length (File) = 0)),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Close (File : in out File_Type) with
- Pre => Is_Open (File),
- Post => not Is_Open (File),
- Global => (In_Out => File_System);
+ Pre => Is_Open (File),
+ Post => not Is_Open (File),
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure Delete (File : in out File_Type) with
- Pre => Is_Open (File),
- Post => not Is_Open (File),
- Global => (In_Out => File_System);
+ Pre => Is_Open (File),
+ Post => not Is_Open (File),
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Reset (File : in out File_Type; Mode : File_Mode) with
- Pre => Is_Open (File),
- Post =>
+ Pre => Is_Open (File),
+ Post =>
Is_Open (File)
and then Ada.Text_IO.Mode (File) = Mode
and then (if Mode /= In_File
then (Line_Length (File) = 0
and then Page_Length (File) = 0)),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Reset (File : in out File_Type) with
- Pre => Is_Open (File),
- Post =>
+ Pre => Is_Open (File),
+ Post =>
Is_Open (File)
and Mode (File)'Old = Mode (File)
and (if Mode (File) /= In_File
then (Line_Length (File) = 0
and then Page_Length (File) = 0)),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
function Mode (File : File_Type) return File_Mode with
- Pre => Is_Open (File),
- Global => null;
+ Pre => Is_Open (File),
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
function Name (File : File_Type) return String with
- Pre => Is_Open (File),
- Global => null;
+ Pre => Is_Open (File),
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
function Form (File : File_Type) return String with
- Pre => Is_Open (File),
- Global => null;
+ Pre => Is_Open (File),
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
function Is_Open (File : File_Type) return Boolean with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
------------------------------------------------------
-- Control of default input, output and error files --
@@ -199,120 +209,142 @@ is
-- an oversight, and was intended to be IN, see AI95-00057.
procedure Flush (File : File_Type) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure Flush with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Always_Return);
--------------------------------------------
-- Specification of line and page lengths --
--------------------------------------------
procedure Set_Line_Length (File : File_Type; To : Count) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File) = To
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Set_Line_Length (To : Count) with
- Post =>
+ Post =>
Line_Length = To
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Set_Page_Length (File : File_Type; To : Count) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Page_Length (File) = To
and Line_Length (File)'Old = Line_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Set_Page_Length (To : Count) with
- Post =>
+ Post =>
Page_Length = To
and Line_Length'Old = Line_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
function Line_Length (File : File_Type) return Count with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Global => (Input => File_System);
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Global => (Input => File_System);
function Line_Length return Count with
- Global => (Input => File_System);
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
function Page_Length (File : File_Type) return Count with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Global => (Input => File_System);
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Global => (Input => File_System);
function Page_Length return Count with
- Global => (Input => File_System);
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
------------------------------------
-- Column, Line, and Page Control --
------------------------------------
procedure New_Line (File : File_Type; Spacing : Positive_Count := 1) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure New_Line (Spacing : Positive_Count := 1) with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure Skip_Line (File : File_Type; Spacing : Positive_Count := 1) with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Skip_Line (Spacing : Positive_Count := 1) with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
function End_Of_Line (File : File_Type) return Boolean with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (Input => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
function End_Of_Line return Boolean with
- Global => (Input => File_System);
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure New_Page (File : File_Type) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure New_Page with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure Skip_Page (File : File_Type) with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Skip_Page with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
function End_Of_Page (File : File_Type) return Boolean with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (Input => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
function End_Of_Page return Boolean with
- Global => (Input => File_System);
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
function End_Of_File (File : File_Type) return Boolean with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (Input => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
function End_Of_File return Boolean with
- Global => (Input => File_System);
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure Set_Col (File : File_Type; To : Positive_Count) with
Pre =>
@@ -325,13 +357,15 @@ is
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
others => True),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Set_Col (To : Positive_Count) with
- Pre => Line_Length = 0 or To <= Line_Length,
- Post =>
+ Pre => Line_Length = 0 or To <= Line_Length,
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Set_Line (File : File_Type; To : Positive_Count) with
Pre =>
@@ -344,149 +378,173 @@ is
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
others => True),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Set_Line (To : Positive_Count) with
- Pre => Page_Length = 0 or To <= Page_Length,
- Post =>
+ Pre => Page_Length = 0 or To <= Page_Length,
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
function Col (File : File_Type) return Positive_Count with
- Pre => Is_Open (File),
- Global => (Input => File_System);
+ Pre => Is_Open (File),
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
function Col return Positive_Count with
- Global => (Input => File_System);
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
function Line (File : File_Type) return Positive_Count with
- Pre => Is_Open (File),
- Global => (Input => File_System);
+ Pre => Is_Open (File),
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
function Line return Positive_Count with
- Global => (Input => File_System);
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
function Page (File : File_Type) return Positive_Count with
- Pre => Is_Open (File),
- Global => (Input => File_System);
+ Pre => Is_Open (File),
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
function Page return Positive_Count with
- Global => (Input => File_System);
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
----------------------------
-- Character Input-Output --
----------------------------
procedure Get (File : File_Type; Item : out Character) with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get (Item : out Character) with
Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put (File : File_Type; Item : Character) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure Put (Item : Character) with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure Look_Ahead
(File : File_Type;
Item : out Character;
End_Of_Line : out Boolean)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (Input => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure Look_Ahead
(Item : out Character;
End_Of_Line : out Boolean)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (Input => File_System);
+ Global => (Input => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure Get_Immediate
(File : File_Type;
Item : out Character)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get_Immediate
(Item : out Character)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get_Immediate
(File : File_Type;
Item : out Character;
Available : out Boolean)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get_Immediate
(Item : out Character;
Available : out Boolean)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
-------------------------
-- String Input-Output --
-------------------------
procedure Get (File : File_Type; Item : out String) with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get (Item : out String) with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put (File : File_Type; Item : String) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure Put (Item : String) with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure Get_Line
(File : File_Type;
Item : out String;
Last : out Natural)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Post => (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Post => (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last
else Last = Item'First - 1),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get_Line
(Item : out String;
Last : out Natural)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length
and (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last
else Last = Item'First - 1),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
function Get_Line (File : File_Type) return String with SPARK_Mode => Off;
pragma Ada_05 (Get_Line);
@@ -498,19 +556,21 @@ is
(File : File_Type;
Item : String)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Always_Return);
procedure Put_Line
(Item : String)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Always_Return);
---------------------------------------
-- Generic packages for Input-Output --
diff --git a/gcc/ada/libgnat/a-tideio.ads b/gcc/ada/libgnat/a-tideio.ads
index c5be4960515..4a2536d3cb1 100644
--- a/gcc/ada/libgnat/a-tideio.ads
+++ b/gcc/ada/libgnat/a-tideio.ads
@@ -54,17 +54,19 @@ package Ada.Text_IO.Decimal_IO is
Item : out Num;
Width : Field := 0)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get
(Item : out Num;
Width : Field := 0)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(File : File_Type;
@@ -73,11 +75,12 @@ package Ada.Text_IO.Decimal_IO is
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(Item : Num;
@@ -85,17 +88,19 @@ package Ada.Text_IO.Decimal_IO is
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get
(From : String;
Item : out Num;
Last : out Positive)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(To : out String;
@@ -103,7 +108,8 @@ package Ada.Text_IO.Decimal_IO is
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
private
pragma Inline (Get);
diff --git a/gcc/ada/libgnat/a-tienio.ads b/gcc/ada/libgnat/a-tienio.ads
index fb80abdf8ff..aac90f767ba 100644
--- a/gcc/ada/libgnat/a-tienio.ads
+++ b/gcc/ada/libgnat/a-tienio.ads
@@ -29,13 +29,15 @@ package Ada.Text_IO.Enumeration_IO is
Default_Setting : Type_Set := Upper_Case;
procedure Get (File : File_Type; Item : out Enum) with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get (Item : out Enum) with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(File : File_Type;
@@ -43,34 +45,38 @@ package Ada.Text_IO.Enumeration_IO is
Width : Field := Default_Width;
Set : Type_Set := Default_Setting)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(Item : Enum;
Width : Field := Default_Width;
Set : Type_Set := Default_Setting)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get
(From : String;
Item : out Enum;
Last : out Positive)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(To : out String;
Item : Enum;
Set : Type_Set := Default_Setting)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
end Ada.Text_IO.Enumeration_IO;
diff --git a/gcc/ada/libgnat/a-tifiio.ads b/gcc/ada/libgnat/a-tifiio.ads
index 8a3886d30e6..bbf8e90ffef 100644
--- a/gcc/ada/libgnat/a-tifiio.ads
+++ b/gcc/ada/libgnat/a-tifiio.ads
@@ -34,17 +34,19 @@ package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is
Item : out Num;
Width : Field := 0)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get
(Item : out Num;
Width : Field := 0)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(File : File_Type;
@@ -53,11 +55,12 @@ package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(Item : Num;
@@ -65,17 +68,19 @@ package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get
(From : String;
Item : out Num;
Last : out Positive)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(To : out String;
@@ -83,7 +88,8 @@ package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
private
pragma Inline (Get);
diff --git a/gcc/ada/libgnat/a-tiflio.ads b/gcc/ada/libgnat/a-tiflio.ads
index 2760b0f0e81..032c6b2f162 100644
--- a/gcc/ada/libgnat/a-tiflio.ads
+++ b/gcc/ada/libgnat/a-tiflio.ads
@@ -54,17 +54,19 @@ package Ada.Text_IO.Float_IO with SPARK_Mode => On is
Item : out Num;
Width : Field := 0)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get
(Item : out Num;
Width : Field := 0)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(File : File_Type;
@@ -73,11 +75,12 @@ package Ada.Text_IO.Float_IO with SPARK_Mode => On is
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(Item : Num;
@@ -85,17 +88,19 @@ package Ada.Text_IO.Float_IO with SPARK_Mode => On is
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get
(From : String;
Item : out Num;
Last : out Positive)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(To : out String;
@@ -103,7 +108,8 @@ package Ada.Text_IO.Float_IO with SPARK_Mode => On is
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
private
pragma Inline (Get);
diff --git a/gcc/ada/libgnat/a-tiinio.ads b/gcc/ada/libgnat/a-tiinio.ads
index 77efd46feb5..491bc2f32d8 100644
--- a/gcc/ada/libgnat/a-tiinio.ads
+++ b/gcc/ada/libgnat/a-tiinio.ads
@@ -53,17 +53,19 @@ package Ada.Text_IO.Integer_IO is
Item : out Num;
Width : Field := 0)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get
(Item : out Num;
Width : Field := 0)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(File : File_Type;
@@ -71,35 +73,39 @@ package Ada.Text_IO.Integer_IO is
Width : Field := Default_Width;
Base : Number_Base := Default_Base)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(Item : Num;
Width : Field := Default_Width;
Base : Number_Base := Default_Base)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get
(From : String;
Item : out Num;
Last : out Positive)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(To : out String;
Item : Num;
Base : Number_Base := Default_Base)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
private
pragma Inline (Get);
diff --git a/gcc/ada/libgnat/a-timoio.ads b/gcc/ada/libgnat/a-timoio.ads
index 8c28a0a1ee7..67ff7c6ba28 100644
--- a/gcc/ada/libgnat/a-timoio.ads
+++ b/gcc/ada/libgnat/a-timoio.ads
@@ -53,17 +53,19 @@ package Ada.Text_IO.Modular_IO is
Item : out Num;
Width : Field := 0)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get
(Item : out Num;
Width : Field := 0)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(File : File_Type;
@@ -71,35 +73,39 @@ package Ada.Text_IO.Modular_IO is
Width : Field := Default_Width;
Base : Number_Base := Default_Base)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(Item : Num;
Width : Field := Default_Width;
Base : Number_Base := Default_Base)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System);
+ Global => (In_Out => File_System),
+ Annotate => (GNATprove, Might_Not_Return);
procedure Get
(From : String;
Item : out Num;
Last : out Positive)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
procedure Put
(To : out String;
Item : Num;
Base : Number_Base := Default_Base)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
private
pragma Inline (Get);
diff --git a/gcc/ada/libgnat/i-c.ads b/gcc/ada/libgnat/i-c.ads
index 2023b753dfd..70139023dc3 100644
--- a/gcc/ada/libgnat/i-c.ads
+++ b/gcc/ada/libgnat/i-c.ads
@@ -29,6 +29,8 @@ with System.Parameters;
package Interfaces.C
with SPARK_Mode, Pure
is
+ pragma Annotate (GNATprove, Always_Return, C);
+
-- Each of the types declared in Interfaces.C is C-compatible.
-- The types int, short, long, unsigned, ptrdiff_t, size_t, double,
diff --git a/gcc/ada/libgnat/interfac.ads b/gcc/ada/libgnat/interfac.ads
index b12ced8c764..b269869fd4e 100644
--- a/gcc/ada/libgnat/interfac.ads
+++ b/gcc/ada/libgnat/interfac.ads
@@ -38,6 +38,7 @@
package Interfaces is
pragma No_Elaboration_Code_All;
pragma Pure;
+ pragma Annotate (GNATprove, Always_Return, Interfaces);
-- All identifiers in this unit are implementation defined
diff --git a/gcc/ada/libgnat/interfac__2020.ads b/gcc/ada/libgnat/interfac__2020.ads
index 579e8b49ed6..becd18069eb 100644
--- a/gcc/ada/libgnat/interfac__2020.ads
+++ b/gcc/ada/libgnat/interfac__2020.ads
@@ -38,6 +38,7 @@
package Interfaces is
pragma No_Elaboration_Code_All;
pragma Pure;
+ pragma Annotate (GNATprove, Always_Return, Interfaces);
-- All identifiers in this unit are implementation defined
diff --git a/gcc/ada/libgnat/s-atacco.ads b/gcc/ada/libgnat/s-atacco.ads
index b3559ffed79..a928d47ef46 100644
--- a/gcc/ada/libgnat/s-atacco.ads
+++ b/gcc/ada/libgnat/s-atacco.ads
@@ -55,9 +55,11 @@ package System.Address_To_Access_Conversions is
-- of no strict aliasing.
function To_Pointer (Value : Address) return Object_Pointer with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
function To_Address (Value : Object_Pointer) return Address with
- SPARK_Mode => Off;
+ SPARK_Mode => Off,
+ Annotate => (GNATprove, Always_Return);
pragma Import (Intrinsic, To_Pointer);
pragma Import (Intrinsic, To_Address);
diff --git a/gcc/ada/libgnat/s-stoele.ads b/gcc/ada/libgnat/s-stoele.ads
index 48af71b1dde..d0473682f7e 100644
--- a/gcc/ada/libgnat/s-stoele.ads
+++ b/gcc/ada/libgnat/s-stoele.ads
@@ -43,6 +43,8 @@ package System.Storage_Elements is
-- this unit Pure instead of Preelaborable; see RM 13.7.1(15). In Ada 2005,
-- this is Pure in any case (AI-362).
+ pragma Annotate (GNATprove, Always_Return, Storage_Elements);
+
-- We also add the pragma Pure_Function to the operations in this package,
-- because otherwise functions with parameters derived from Address are
-- treated as non-pure by the back-end (see exp_ch6.adb). This is because
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-07-12 12:25 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-07-12 12:25 [gcc r13-1624] [Ada] Annotate libraries with returning annotation Pierre-Marie de Rodat
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).