yggdrasil/gcc
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

[Ada] Annotate libraries with returning annotation

Browse Source 
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.
This commit is contained in:
Joffrey Huguet
2022-06-13 11:44:51 +02:00
committed by Pierre-Marie de Rodat
parent 01bf0d6cf5
commit a31eda1546
38 changed files with 443 additions and 258 deletions
Download Patch File Download Diff File Expand all files Collapse all files
gcc/ada/libgnarl/a-reatim.ads
+1
View File
@@ -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,
gcc/ada/libgnat/a-cfdlli.ads
+3 -1
View File
@@ -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.
gcc/ada/libgnat/a-cfhama.ads
+3 -1
View File
@@ -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.
gcc/ada/libgnat/a-cfhase.ads
+3 -1
View File
@@ -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.
gcc/ada/libgnat/a-cfinse.ads
+4 -1
View File
@@ -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,
gcc/ada/libgnat/a-cfinve.ads
+3 -1
View File
@@ -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.
gcc/ada/libgnat/a-cforma.ads
+3 -1
View File
@@ -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.
gcc/ada/libgnat/a-cforse.ads
+3 -1
View File
@@ -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.
gcc/ada/libgnat/a-chahan.ads
+2
View File
@@ -46,6 +46,8 @@ is
pragma Pure;
-- In accordance with Ada 2005 AI-362
pragma Annotate (GNATprove, Always_Return, Handling);
----------------------------------------
-- Character Classification Functions --
----------------------------------------
gcc/ada/libgnat/a-cofove.ads
+2
View File
@@ -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.
gcc/ada/libgnat/a-cofuma.ads
+4 -1
View File
@@ -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,
gcc/ada/libgnat/a-cofuse.ads
+4 -1
View File
@@ -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),
gcc/ada/libgnat/a-cofuve.ads
+4 -1
View File
@@ -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;
gcc/ada/libgnat/a-nbnbin.ads
+2
View File
@@ -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;
gcc/ada/libgnat/a-nbnbre.ads
+2
View File
@@ -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;
gcc/ada/libgnat/a-ngelfu.ads
+1
View File
@@ -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
gcc/ada/libgnat/a-nlelfu.ads
+1
View File
@@ -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);
gcc/ada/libgnat/a-nllefu.ads
+1
View File
@@ -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);
gcc/ada/libgnat/a-nselfu.ads
+1
View File
@@ -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);
gcc/ada/libgnat/a-nuelfu.ads
+1
View File
@@ -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);
gcc/ada/libgnat/a-strbou.ads
+2
View File
@@ -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;
gcc/ada/libgnat/a-strfix.ads
+87 -51
View File
@@ -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
gcc/ada/libgnat/a-strmap.ads
+2
View File
@@ -54,6 +54,8 @@ is
pragma Pure;
-- In accordance with Ada 2005 AI-362
pragma Annotate (GNATprove, Always_Return, Maps);
--------------------------------
-- Character Set Declarations --
--------------------------------
gcc/ada/libgnat/a-strsea.ads
+1
View File
@@ -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
gcc/ada/libgnat/a-strunb.ads
+1
View File
@@ -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;
gcc/ada/libgnat/a-strunb__shared.ads
+1
View File
@@ -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;
gcc/ada/libgnat/a-textio.ads
+189 -129
View File
@@ -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 --
gcc/ada/libgnat/a-tideio.ads
+17 -11
View File
@@ -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);
gcc/ada/libgnat/a-tienio.ads
+17 -11
View File
@@ -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;
gcc/ada/libgnat/a-tifiio.ads
+17 -11
View File
@@ -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);
gcc/ada/libgnat/a-tiflio.ads
+17 -11
View File
@@ -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);
gcc/ada/libgnat/a-tiinio.ads
+17 -11
View File
@@ -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);
gcc/ada/libgnat/a-timoio.ads
+17 -11
View File
@@ -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);
gcc/ada/libgnat/i-c.ads
+2
View File
@@ -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,
gcc/ada/libgnat/interfac.ads
+1
View File
@@ -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
gcc/ada/libgnat/interfac__2020.ads
+1
View File
@@ -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
gcc/ada/libgnat/s-atacco.ads
+4 -2
View File
@@ -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);
gcc/ada/libgnat/s-stoele.ads
+2
View File
@@ -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