package Ada.Real_Time with
SPARK_Mode,
Abstract_State => (Clock_Time with Synchronous),
- Initializes => Clock_Time
+ Initializes => Clock_Time,
+ Always_Terminates
is
- pragma Annotate (GNATprove, Always_Return, Real_Time);
pragma Compile_Time_Error
(Duration'Size /= 64,
with Ada.Characters.Latin_1;
-package Ada.Characters.Handling
- with SPARK_Mode
+package Ada.Characters.Handling with
+ SPARK_Mode,
+ Always_Terminates
is
pragma Pure;
-- In accordance with Ada 2005 AI-362
- pragma Annotate (GNATprove, Always_Return, Handling);
-
----------------------------------------
-- Character Classification Functions --
----------------------------------------
package Ada.Numerics.Big_Numbers.Big_Integers_Ghost with
SPARK_Mode,
Ghost,
- Pure
+ Pure,
+ Always_Terminates
is
- pragma Annotate (GNATprove, Always_Return, Big_Integers_Ghost);
type Big_Integer is private
with Integer_Literal => From_Universal_Image;
private with Ada.Finalization;
private with System;
-package Ada.Numerics.Big_Numbers.Big_Integers
- with Preelaborate
+package Ada.Numerics.Big_Numbers.Big_Integers with
+ Preelaborate,
+ Always_Terminates
is
- pragma Annotate (GNATprove, Always_Return, Big_Integers);
type Big_Integer is private
with Integer_Literal => From_Universal_Image,
with Ada.Strings.Text_Buffers; use Ada.Strings.Text_Buffers;
-package Ada.Numerics.Big_Numbers.Big_Reals
- with Preelaborate
+package Ada.Numerics.Big_Numbers.Big_Reals with
+ Preelaborate,
+ Always_Terminates
is
- pragma Annotate (GNATprove, Always_Return, Big_Reals);
type Big_Real is private with
Real_Literal => From_Universal_Image,
type Float_Type is digits <>;
package Ada.Numerics.Generic_Elementary_Functions with
- SPARK_Mode => On
+ SPARK_Mode => On,
+ Always_Terminates
is
pragma Pure;
- pragma Annotate (GNATprove, Always_Return, Generic_Elementary_Functions);
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised when calling
new Ada.Numerics.Generic_Elementary_Functions (Long_Float);
pragma Pure (Long_Elementary_Functions);
-pragma Annotate (GNATprove, Always_Return, Long_Elementary_Functions);
new Ada.Numerics.Generic_Elementary_Functions (Long_Long_Float);
pragma Pure (Long_Long_Elementary_Functions);
-pragma Annotate (GNATprove, Always_Return, Long_Long_Elementary_Functions);
new Ada.Numerics.Generic_Elementary_Functions (Short_Float);
pragma Pure (Short_Elementary_Functions);
-pragma Annotate (GNATprove, Always_Return, Short_Elementary_Functions);
new Ada.Numerics.Generic_Elementary_Functions (Float);
pragma Pure (Elementary_Functions);
-pragma Annotate (GNATprove, Always_Return, Elementary_Functions);
with Ada.Strings.Superbounded;
with Ada.Strings.Search;
-package Ada.Strings.Bounded with SPARK_Mode is
+package Ada.Strings.Bounded with
+ SPARK_Mode,
+ Always_Terminates
+is
pragma Preelaborate;
- pragma Annotate (GNATprove, Always_Return, Bounded);
generic
Max : Positive;
package Generic_Bounded_Length with SPARK_Mode,
Initial_Condition => Length (Null_Bounded_String) = 0,
- Abstract_State => null
+ Abstract_State => null,
+ Always_Terminates
is
-- Preconditions in this unit are meant for analysis only, not for
-- run-time checking, so that the expected exceptions are raised. This
Post => Ignore,
Contract_Cases => Ignore,
Ghost => Ignore);
- pragma Annotate (GNATprove, Always_Return, Generic_Bounded_Length);
Max_Length : constant Positive := Max;
with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
with Ada.Strings.Search;
-package Ada.Strings.Fixed with SPARK_Mode is
+package Ada.Strings.Fixed with
+ SPARK_Mode,
+ Always_Terminates
+is
pragma Preelaborate;
--------------------------------------------------------------
Justify : Alignment := Left;
Pad : Character := Space)
with
-
- -- Incomplete contract
-
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases =>
+ (Length_Error => Target'Length'Old < Source'Length and Drop = Error);
-- The Move procedure copies characters from Source to Target. If Source
-- has the same length as Target, then the effect is to assign Source to
-- Target. If Source is shorter than Target then:
others
=>
Index'Result = 0),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
pragma Ada_05 (Index);
function Index
others
=>
Index'Result = 0),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
pragma Ada_05 (Index);
-- Each Index function searches, starting from From, for a slice of
others
=>
Index'Result = 0),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
function Index
(Source : String;
others
=>
Index'Result = 0),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- If Going = Forward, returns:
--
and then (J < Index'Result) = (Going = Forward)
then (Test = Inside)
/= Ada.Strings.Maps.Is_In (Source (J), Set)))),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
function Index
(Source : String;
or else (J > From) = (Going = Forward))
then (Test = Inside)
/= Ada.Strings.Maps.Is_In (Source (J), Set)))),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
pragma Ada_05 (Index);
-- Index searches for the first or last occurrence of any of a set of
-- characters (when Test=Inside), or any of the complement of a set of
and then (J = From or else (J > From)
= (Going = Forward))
then Source (J) = ' '))),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
pragma Ada_05 (Index_Non_Blank);
-- Returns Index (Source, Maps.To_Set(Space), From, Outside, Going)
and then (J < Index_Non_Blank'Result)
= (Going = Forward)
then Source (J) = ' '))),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- Returns Index (Source, Maps.To_Set(Space), Outside, Going)
function Count
Pattern : String;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
with
- Pre => Pattern'Length /= 0,
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Count
(Source : String;
Pattern : String;
Mapping : Maps.Character_Mapping_Function) return Natural
with
- Pre => Pattern'Length /= 0 and then Mapping /= null,
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Pre => Pattern'Length /= 0 and then Mapping /= null,
+ Global => null;
-- Returns the maximum number of nonoverlapping slices of Source that match
-- Pattern with respect to Mapping. If Pattern is the null string then
(Source : String;
Set : Maps.Character_Set) return Natural
with
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- Returns the number of occurrences in Source of characters that are in
-- Set.
then
(Test = Inside)
/= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
pragma Ada_2012 (Find_Token);
-- If Source is not the null string and From is not in Source'Range, then
-- Index_Error is raised. Otherwise, First is set to the index of the first
then
(Test = Inside)
/= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- Equivalent to Find_Token (Source, Set, Source'First, Test, First, Last)
------------------------------------
(for all J in Source'Range =>
Translate'Result (J - Source'First + 1)
= Mapping (Source (J))),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
(for all J in Source'Range =>
Translate'Result (J - Source'First + 1)
= Ada.Strings.Maps.Value (Mapping, Source (J))),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- Returns the string S whose length is Source'Length and such that S (I)
-- is the character to which Mapping maps the corresponding element of
(Source : in out String;
Mapping : Maps.Character_Mapping_Function)
with
- Pre => Mapping /= null,
- Post =>
+ Pre => Mapping /= null,
+ Post =>
-- Each character in Source after the call is the translation of the
-- character at the same position before the call, through Mapping.
(for all J in Source'Range => Source (J) = Mapping (Source'Old (J))),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
pragma Annotate (GNATprove, False_Positive,
"call via access-to-subprogram",
"function Mapping must always terminate");
(Source : in out String;
Mapping : Maps.Character_Mapping)
with
- Post =>
+ Post =>
-- Each character in Source after the call is the translation of the
-- character at the same position before the call, through Mapping.
(for all J in Source'Range =>
Source (J) = Ada.Strings.Maps.Value (Mapping, Source'Old (J))),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- Equivalent to Source := Translate(Source, Mapping)
(Low - Source'First + By'Length + 1
.. Replace_Slice'Result'Last)
= Source (Low .. Source'Last))),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- If Low > Source'Last + 1, or High < Source'First - 1, then Index_Error
-- is propagated. Otherwise:
--
Justify : Alignment := Left;
Pad : Character := Space)
with
- Pre =>
+ Pre =>
Low - 1 <= Source'Last
and then High >= Source'First - 1
and then (if High >= Low
- By'Length
- Natural'Max (Source'Last - High, 0)
else Source'Length <= Natural'Last - By'Length),
-
- -- Incomplete contract
-
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Length_Error => Drop = Error);
-- Equivalent to:
--
-- Move (Replace_Slice (Source, Low, High, By),
(Before - Source'First + New_Item'Length + 1
.. Insert'Result'Last)
= Source (Before .. Source'Last)),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- Propagates Index_Error if Before is not in
-- Source'First .. Source'Last + 1; otherwise, returns
-- Source (Source'First .. Before - 1)
New_Item : String;
Drop : Truncation := Error)
with
- Pre =>
+ Pre =>
Before - 1 in Source'First - 1 .. Source'Last
and then Source'Length <= Natural'Last - New_Item'Length,
-
- -- Incomplete contract
-
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Length_Error => Drop = Error);
-- Equivalent to Move (Insert (Source, Before, New_Item), Source, Drop)
function Overwrite
(Position - Source'First + New_Item'Length + 1
.. Overwrite'Result'Last)
= Source (Position + New_Item'Length .. Source'Last)),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- Propagates Index_Error if Position is not in
-- Source'First .. Source'Last + 1; otherwise, returns the string obtained
-- from Source by consecutively replacing characters starting at Position
New_Item : String;
Drop : Truncation := Right)
with
- Pre =>
+ Pre =>
Position - 1 in Source'First - 1 .. Source'Last
and then
(if Position - Source'First >= Source'Length - New_Item'Length
then Position - Source'First <= Natural'Last - New_Item'Length),
-
- -- Incomplete contract
-
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Length_Error => Drop = Error);
-- Equivalent to Move(Overwrite(Source, Position, New_Item), Source, Drop)
function Delete
others =>
Delete'Result'Length = Source'Length
and then Delete'Result = Source),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- If From <= Through, the returned string is
-- Replace_Slice(Source, From, Through, ""); otherwise, it is Source with
-- lower bound 1.
Justify : Alignment := Left;
Pad : Character := Space)
with
- Pre => (if From <= Through
+ Pre => (if From <= Through
then (From in Source'Range
and then Through <= Source'Last)),
-
- -- Incomplete contract
-
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null;
-- Equivalent to:
--
-- Move (Delete (Source, From, Through),
(Source : String;
Side : Trim_End) return String
with
- Post =>
+ Post =>
-- Lower bound of the returned string is 1
else Index_Non_Blank (Source, Backward));
begin
Trim'Result = Source (Low .. High))),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- Returns the string obtained by removing from Source all leading Space
-- characters (if Side = Left), all trailing Space characters (if
-- Side = Right), or all leading and trailing Space characters (if
Justify : Alignment := Left;
Pad : Character := Space)
with
-
- -- Incomplete contract
-
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null;
-- Equivalent to:
--
-- Move (Trim (Source, Side), Source, Justify=>Justify, Pad=>Pad).
Index (Source, Right, Outside, Backward);
begin
Trim'Result = Source (Low .. High))),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- Returns the string obtained by removing from Source all leading
-- characters in Left and all trailing characters in Right.
Justify : Alignment := Strings.Left;
Pad : Character := Space)
with
-
- -- Incomplete contract
-
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null;
-- Equivalent to:
--
-- Move (Trim (Source, Left, Right),
and then
Head'Result (Source'Length + 1 .. Count)
= [1 .. Count - Source'Length => Pad]),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- Returns a string of length Count. If Count <= Source'Length, the string
-- comprises the first Count characters of Source. Otherwise, its contents
-- are Source concatenated with Count - Source'Length Pad characters.
Justify : Alignment := Left;
Pad : Character := Space)
with
-
- -- Incomplete contract
-
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Length_Error => Count > Source'Length'Old);
-- Equivalent to:
--
-- Move (Head (Source, Count, Pad),
and then
Tail'Result (Count - Source'Length + 1 .. Tail'Result'Last)
= Source)),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- Returns a string of length Count. If Count <= Source'Length, the string
-- comprises the last Count characters of Source. Otherwise, its contents
-- are Count-Source'Length Pad characters concatenated with Source.
Justify : Alignment := Left;
Pad : Character := Space)
with
-
- -- Incomplete contract
-
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Length_Error => Count > Source'Length'Old);
-- Equivalent to:
--
-- Move (Tail (Source, Count, Pad),
(Left : Natural;
Right : Character) return String
with
- Post =>
+ Post =>
-- Lower bound of the returned string is 1
-- All characters of the returned string are Right
and then (for all C of "*"'Result => C = Right),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
function "*"
(Left : Natural;
and then
(for all K in "*"'Result'Range =>
"*"'Result (K) = Right (Right'First + (K - 1) mod Right'Length)),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
-- These functions replicate a character or string a specified number of
-- times. The first function returns a string whose length is Left and each
with Ada.Characters.Latin_1;
-package Ada.Strings.Maps
- with SPARK_Mode
+package Ada.Strings.Maps with
+ SPARK_Mode,
+ Always_Terminates
is
pragma Pure;
-- In accordance with Ada 2005 AI-362
- pragma Annotate (GNATprove, Always_Return, Maps);
-
--------------------------------
-- Character Set Declarations --
--------------------------------
with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
-package Ada.Strings.Search with SPARK_Mode is
+package Ada.Strings.Search with
+ SPARK_Mode,
+ Always_Terminates
+is
pragma Preelaborate;
- pragma Annotate (GNATprove, Always_Return, Search);
-- The ghost function Match tells whether the slice of Source starting at
-- From and of length Pattern'Length matches with Pattern with respect to
with Ada.Strings.Search;
with Ada.Strings.Text_Buffers;
-package Ada.Strings.Superbounded with SPARK_Mode is
+package Ada.Strings.Superbounded with
+ SPARK_Mode,
+ Always_Terminates
+is
pragma Preelaborate;
- pragma Annotate (GNATprove, Always_Return, Superbounded);
-- Type Bounded_String in Ada.Strings.Bounded.Generic_Bounded_Length is
-- derived from Super_String, with the constraint of the maximum length.
package Ada.Strings.Unbounded with
SPARK_Mode,
- Initial_Condition => Length (Null_Unbounded_String) = 0
+ Initial_Condition => Length (Null_Unbounded_String) = 0,
+ Always_Terminates
is
pragma Preelaborate;
- pragma Annotate (GNATprove, Always_Return, Unbounded);
type Unbounded_String is private with
Default_Initial_Condition => Length (Unbounded_String) = 0;
private with Ada.Strings.Text_Buffers;
package Ada.Strings.Unbounded with
- Initial_Condition => Length (Null_Unbounded_String) = 0
+ Initial_Condition => Length (Null_Unbounded_String) = 0,
+ Always_Terminates
is
pragma Preelaborate;
- pragma Annotate (GNATprove, Always_Return, Unbounded);
type Unbounded_String is private with
Default_Initial_Condition => Length (Unbounded_String) = 0;
SPARK_Mode,
Abstract_State => File_System,
Initializes => File_System,
- Initial_Condition => Line_Length = 0 and Page_Length = 0
+ Initial_Condition => Line_Length = 0 and Page_Length = 0,
+ Always_Terminates
is
pragma Elaborate_Body;
Name : String := "";
Form : String := "")
with
- Pre => not Is_Open (File),
- Post =>
+ Pre => not Is_Open (File),
+ Post =>
Is_Open (File)
and then Ada.Text_IO.Mode (File) = Mode
and then (if Mode /= In_File
then (Line_Length (File) = 0
and then Page_Length (File) = 0)),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Name_Error | Use_Error => Standard.True);
procedure Open
(File : in out File_Type;
Name : String;
Form : String := "")
with
- Pre => not Is_Open (File),
- Post =>
+ Pre => not Is_Open (File),
+ Post =>
Is_Open (File)
and then Ada.Text_IO.Mode (File) = Mode
and then (if Mode /= In_File
then (Line_Length (File) = 0
and then Page_Length (File) = 0)),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Name_Error | Use_Error => Standard.True);
procedure Close (File : in out File_Type) with
- Pre => Is_Open (File),
- Post => not Is_Open (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Always_Return);
+ Pre => Is_Open (File),
+ Post => not Is_Open (File),
+ Global => (In_Out => File_System);
procedure Delete (File : in out File_Type) with
- Pre => Is_Open (File),
- Post => not Is_Open (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File),
+ Post => not Is_Open (File),
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Use_Error => Standard.True);
procedure Reset (File : in out File_Type; Mode : File_Mode) with
- Pre => Is_Open (File),
- Post =>
+ Pre => Is_Open (File),
+ Post =>
Is_Open (File)
and then Ada.Text_IO.Mode (File) = Mode
and then (if Mode /= In_File
then (Line_Length (File) = 0
and then Page_Length (File) = 0)),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Use_Error => Standard.True);
procedure Reset (File : in out File_Type) with
- Pre => Is_Open (File),
- Post =>
+ Pre => Is_Open (File),
+ Post =>
Is_Open (File)
and Mode (File)'Old = Mode (File)
and (if Mode (File) /= In_File
then (Line_Length (File) = 0
and then Page_Length (File) = 0)),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Use_Error => Standard.True);
function Mode (File : File_Type) return File_Mode with
Pre => Is_Open (File),
Global => null;
function Name (File : File_Type) return String with
- Pre => Is_Open (File),
- Global => null;
+ Pre => Is_Open (File),
+ SPARK_Mode => Off;
function Form (File : File_Type) return String with
Pre => Is_Open (File),
-- an oversight, and was intended to be IN, see AI95-00057.
procedure Flush (File : File_Type) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (In_Out => File_System);
procedure Flush with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (In_Out => File_System);
--------------------------------------------
-- Specification of line and page lengths --
--------------------------------------------
procedure Set_Line_Length (File : File_Type; To : Count) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File) = To
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Use_Error => Standard.True);
procedure Set_Line_Length (To : Count) with
- Post =>
+ Post =>
Line_Length = To
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Use_Error => Standard.True);
procedure Set_Page_Length (File : File_Type; To : Count) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Page_Length (File) = To
and Line_Length (File)'Old = Line_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Use_Error => Standard.True);
procedure Set_Page_Length (To : Count) with
- Post =>
+ Post =>
Page_Length = To
and Line_Length'Old = Line_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Use_Error => Standard.True);
function Line_Length (File : File_Type) return Count with
Pre => Is_Open (File) and then Mode (File) /= In_File,
------------------------------------
procedure New_Line (File : File_Type; Spacing : Positive_Count := 1) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (In_Out => File_System);
procedure New_Line (Spacing : Positive_Count := 1) with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (In_Out => File_System);
procedure Skip_Line (File : File_Type; Spacing : Positive_Count := 1) with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
procedure Skip_Line (Spacing : Positive_Count := 1) with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
function End_Of_Line (File : File_Type) return Boolean with
Pre => Is_Open (File) and then Mode (File) = In_File,
Global => (Input => File_System);
procedure New_Page (File : File_Type) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (In_Out => File_System);
procedure New_Page with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (In_Out => File_System);
procedure Skip_Page (File : File_Type) with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
procedure Skip_Page with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
function End_Of_Page (File : File_Type) return Boolean with
Pre => Is_Open (File) and then Mode (File) = In_File,
Global => (Input => File_System);
procedure Set_Col (File : File_Type; To : Positive_Count) with
- Pre =>
+ Pre =>
Is_Open (File)
and then (if Mode (File) /= In_File
then (Line_Length (File) = 0
or else To <= Line_Length (File))),
- Contract_Cases =>
+ Contract_Cases =>
(Mode (File) /= In_File =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
others => True),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
procedure Set_Col (To : Positive_Count) with
- Pre => Line_Length = 0 or To <= Line_Length,
- Post =>
+ Pre => Line_Length = 0 or To <= Line_Length,
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
procedure Set_Line (File : File_Type; To : Positive_Count) with
- Pre =>
+ Pre =>
Is_Open (File)
and then (if Mode (File) /= In_File
then (Page_Length (File) = 0
or else To <= Page_Length (File))),
- Contract_Cases =>
+ Contract_Cases =>
(Mode (File) /= In_File =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
others => True),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
procedure Set_Line (To : Positive_Count) with
- Pre => Page_Length = 0 or To <= Page_Length,
- Post =>
+ Pre => Page_Length = 0 or To <= Page_Length,
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
function Col (File : File_Type) return Positive_Count with
- Pre => Is_Open (File),
- Global => (Input => File_System);
+ SPARK_Mode => Off;
function Col return Positive_Count with
- Global => (Input => File_System);
+ SPARK_Mode => Off;
function Line (File : File_Type) return Positive_Count with
- Pre => Is_Open (File),
- Global => (Input => File_System);
+ SPARK_Mode => Off;
function Line return Positive_Count with
- Global => (Input => File_System);
+ SPARK_Mode => Off;
function Page (File : File_Type) return Positive_Count with
- Pre => Is_Open (File),
- Global => (Input => File_System);
+ SPARK_Mode => Off;
function Page return Positive_Count with
- Global => (Input => File_System);
+ SPARK_Mode => Off;
----------------------------
-- Character Input-Output --
----------------------------
procedure Get (File : File_Type; Item : out Character) with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
procedure Get (Item : out Character) with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
procedure Put (File : File_Type; Item : Character) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (In_Out => File_System);
procedure Put (Item : Character) with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (In_Out => File_System);
procedure Look_Ahead
(File : File_Type;
Item : out Character;
End_Of_Line : out Boolean)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (Input => File_System),
- Annotate => (GNATprove, Always_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (Input => File_System);
procedure Look_Ahead
(Item : out Character;
End_Of_Line : out Boolean)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (Input => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (Input => File_System);
procedure Get_Immediate
(File : File_Type;
Item : out Character)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
procedure Get_Immediate
(Item : out Character)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
procedure Get_Immediate
(File : File_Type;
Item : out Character;
Available : out Boolean)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
procedure Get_Immediate
(Item : out Character;
Available : out Boolean)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Standard.True);
-------------------------
-- String Input-Output --
-------------------------
procedure Get (File : File_Type; Item : out String) with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Item'Length'Old > 0);
procedure Get (Item : out String) with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Item'Length'Old > 0);
procedure Put (File : File_Type; Item : String) with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (In_Out => File_System);
procedure Put (Item : String) with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (In_Out => File_System);
procedure Get_Line
(File : File_Type;
Item : out String;
Last : out Natural)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Post => (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last
- else Last = Item'First - 1),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Post =>
+ (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last
+ else Last = Item'First - 1),
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Item'Length'Old > 0);
procedure Get_Line
(Item : out String;
Last : out Natural)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length
and (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last
else Last = Item'First - 1),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (End_Error => Item'Length'Old > 0);
function Get_Line (File : File_Type) return String with SPARK_Mode => Off;
pragma Ada_05 (Get_Line);
(File : File_Type;
Item : String)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (In_Out => File_System);
procedure Put_Line
(Item : String)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (In_Out => File_System);
---------------------------------------
-- Generic packages for Input-Output --
private generic
type Num is delta <> digits <>;
-package Ada.Text_IO.Decimal_IO is
+package Ada.Text_IO.Decimal_IO with
+ Always_Terminates
+is
Default_Fore : Field := Num'Fore;
Default_Aft : Field := Num'Aft;
Item : out Num;
Width : Field := 0)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Data_Error | End_Error => Standard.True);
procedure Get
(Item : out Num;
Width : Field := 0)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Data_Error | End_Error => Standard.True);
procedure Put
(File : File_Type;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0);
procedure Put
(Item : Num;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Layout_Error => Ada.Text_IO.Line_Length /= 0);
procedure Get
(From : String;
Last : out Positive)
with
Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Exceptional_Cases => (Data_Error => Standard.True);
procedure Put
(To : out String;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Layout_Error => Standard.True);
private
pragma Inline (Get);
private generic
type Enum is (<>);
-package Ada.Text_IO.Enumeration_IO is
+package Ada.Text_IO.Enumeration_IO with
+ Always_Terminates
+is
Default_Width : Field := 0;
Default_Setting : Type_Set := Upper_Case;
procedure Get (File : File_Type; Item : out Enum) with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Data_Error | End_Error => Standard.True);
+
procedure Get (Item : out Enum) with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Data_Error | End_Error => Standard.True);
procedure Put
(File : File_Type;
Width : Field := Default_Width;
Set : Type_Set := Default_Setting)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0);
procedure Put
(Item : Enum;
Width : Field := Default_Width;
Set : Type_Set := Default_Setting)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Layout_Error => Ada.Text_IO.Line_Length /= 0);
procedure Get
(From : String;
Item : out Enum;
Last : out Positive)
with
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Data_Error => Standard.True);
procedure Put
(To : out String;
Item : Enum;
Set : Type_Set := Default_Setting)
with
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Layout_Error => Standard.True);
end Ada.Text_IO.Enumeration_IO;
private generic
type Num is delta <>;
-package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is
+package Ada.Text_IO.Fixed_IO with
+ SPARK_Mode => On,
+ Always_Terminates
+is
Default_Fore : Field := Num'Fore;
Default_Aft : Field := Num'Aft;
Item : out Num;
Width : Field := 0)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Data_Error | End_Error => Standard.True);
procedure Get
(Item : out Num;
Width : Field := 0)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Data_Error | End_Error => Standard.True);
procedure Put
(File : File_Type;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0);
procedure Put
(Item : Num;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Layout_Error => Ada.Text_IO.Line_Length /= 0);
procedure Get
(From : String;
Item : out Num;
Last : out Positive)
with
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Data_Error => Standard.True);
procedure Put
(To : out String;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Layout_Error => Standard.True);
private
pragma Inline (Get);
private generic
type Num is digits <>;
-package Ada.Text_IO.Float_IO with SPARK_Mode => On is
+package Ada.Text_IO.Float_IO with
+ SPARK_Mode => On,
+ Always_Terminates
+is
Default_Fore : Field := 2;
Default_Aft : Field := Num'Digits - 1;
Item : out Num;
Width : Field := 0)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Data_Error | End_Error => Standard.True);
procedure Get
(Item : out Num;
Width : Field := 0)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Data_Error | End_Error => Standard.True);
procedure Put
(File : File_Type;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0);
procedure Put
(Item : Num;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Layout_Error => Line_Length /= 0);
procedure Get
(From : String;
Item : out Num;
Last : out Positive)
with
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Data_Error => Standard.True);
procedure Put
(To : out String;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Layout_Error => Standard.True);
private
pragma Inline (Get);
private generic
type Num is range <>;
-package Ada.Text_IO.Integer_IO is
+package Ada.Text_IO.Integer_IO with
+ Always_Terminates
+is
Default_Width : Field := Num'Width;
Default_Base : Number_Base := 10;
Item : out Num;
Width : Field := 0)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Data_Error | End_Error => Standard.True);
procedure Get
(Item : out Num;
Width : Field := 0)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Data_Error | End_Error => Standard.True);
procedure Put
(File : File_Type;
Width : Field := Default_Width;
Base : Number_Base := Default_Base)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0);
procedure Put
(Item : Num;
Width : Field := Default_Width;
Base : Number_Base := Default_Base)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Layout_Error => Line_Length /= 0);
procedure Get
(From : String;
Item : out Num;
Last : out Positive)
with
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Data_Error => Standard.True);
procedure Put
(To : out String;
Item : Num;
Base : Number_Base := Default_Base)
with
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Layout_Error => Standard.True);
private
pragma Inline (Get);
private generic
type Num is mod <>;
-package Ada.Text_IO.Modular_IO is
+package Ada.Text_IO.Modular_IO with
+ Always_Terminates
+is
Default_Width : Field := Num'Width;
Default_Base : Number_Base := 10;
Item : out Num;
Width : Field := 0)
with
- Pre => Is_Open (File) and then Mode (File) = In_File,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Data_Error | End_Error => Standard.True);
procedure Get
(Item : out Num;
Width : Field := 0)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Data_Error | End_Error => Standard.True);
procedure Put
(File : File_Type;
Width : Field := Default_Width;
Base : Number_Base := Default_Base)
with
- Pre => Is_Open (File) and then Mode (File) /= In_File,
- Post =>
+ Pre => Is_Open (File) and then Mode (File) /= In_File,
+ Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0);
procedure Put
(Item : Num;
Width : Field := Default_Width;
Base : Number_Base := Default_Base)
with
- Post =>
+ Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
- Global => (In_Out => File_System),
- Annotate => (GNATprove, Might_Not_Return);
+ Global => (In_Out => File_System),
+ Exceptional_Cases => (Layout_Error => Line_Length /= 0);
procedure Get
(From : String;
Item : out Num;
Last : out Positive)
with
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Data_Error => Standard.True);
procedure Put
(To : out String;
Item : Num;
Base : Number_Base := Default_Base)
with
- Global => null,
- Annotate => (GNATprove, Might_Not_Return);
+ Global => null,
+ Exceptional_Cases => (Layout_Error => Standard.True);
private
pragma Inline (Get);
Abstract_State =>
(Source_Code_Information with
External => (Async_Writers, Async_Readers)),
- Annotate => (GNATprove, Always_Return)
+ Always_Terminates
is
pragma Preelaborate;
-- Note that this unit is Preelaborate, but not Pure, that's because the
with System;
with System.Parameters;
-package Interfaces.C
- with SPARK_Mode, Pure
+package Interfaces.C with
+ SPARK_Mode,
+ Pure,
+ Always_Terminates
is
- pragma Annotate (GNATprove, Always_Return, C);
-- Each of the types declared in Interfaces.C is C-compatible.
package Interfaces.C.Strings with
SPARK_Mode => On,
Abstract_State => (C_Memory),
- Initializes => (C_Memory)
+ Initializes => (C_Memory),
+ Always_Terminates
is
pragma Preelaborate;
Chars : char_array;
Check : Boolean := True)
with
- Pre =>
+ Pre =>
Item /= Null_Ptr
- and then
- (if Check then
- Strlen (Item) <= size_t'Last - Offset
- and then Strlen (Item) + Offset <= Chars'Length),
- Global => (In_Out => C_Memory),
- Annotate => (GNATprove, Might_Not_Return);
- -- Update may not return if Check is False and the null terminator
- -- is overwritten or skipped with Offset.
+ and then Strlen (Item) <= size_t'Last - Offset
+ and then Strlen (Item) + Offset <= Chars'Length,
+ Global => (In_Out => C_Memory);
procedure Update
(Item : chars_ptr;
Str : String;
Check : Boolean := True)
with
- Pre =>
+ Pre =>
Item /= Null_Ptr
- and then
- (if Check then
- Strlen (Item) <= size_t'Last - Offset
- and then Strlen (Item) + Offset <= Str'Length),
- Global => (In_Out => C_Memory),
- Annotate => (GNATprove, Might_Not_Return);
- -- Update may not return if Check is False and the null terminator
- -- is overwritten or skipped with Offset.
+ and then Strlen (Item) <= size_t'Last - Offset
+ and then Strlen (Item) + Offset <= Str'Length,
+ Global => (In_Out => C_Memory);
Update_Error : exception;
-- This is the compiler version of this unit
-package Interfaces is
+package Interfaces with
+ Always_Terminates
+is
pragma No_Elaboration_Code_All;
pragma Pure;
- pragma Annotate (GNATprove, Always_Return, Interfaces);
-- All identifiers in this unit are implementation defined
-- This is the runtime version of this unit (not used during GNAT build)
-package Interfaces is
+package Interfaces with
+ Always_Terminates
+is
pragma No_Elaboration_Code_All;
pragma Pure;
- pragma Annotate (GNATprove, Always_Return, Interfaces);
-- All identifiers in this unit are implementation defined
function To_Neg_Int (A : Double_Uns) return Double_Int
with
- Annotate => (GNATprove, Always_Return),
- Pre => In_Double_Int_Range (-Big (A)),
- Post => Big (To_Neg_Int'Result) = -Big (A);
+ Pre => In_Double_Int_Range (-Big (A)),
+ Post => Big (To_Neg_Int'Result) = -Big (A);
-- Convert to negative integer equivalent. If the input is in the range
-- 0 .. 2 ** (Double_Size - 1), then the corresponding nonpositive signed
-- integer (obtained by negating the given value) is returned, otherwise
function To_Pos_Int (A : Double_Uns) return Double_Int
with
- Annotate => (GNATprove, Always_Return),
- Pre => In_Double_Int_Range (Big (A)),
- Post => Big (To_Pos_Int'Result) = Big (A);
+ Pre => In_Double_Int_Range (Big (A)),
+ Post => Big (To_Pos_Int'Result) = Big (A);
-- Convert to positive integer equivalent. If the input is in the range
-- 0 .. 2 ** (Double_Size - 1) - 1, then the corresponding non-negative
-- signed integer is returned, otherwise constraint error is raised.
function To_Neg_Int (A : Uns32) return Int32
with
- Annotate => (GNATprove, Always_Return),
- Pre => In_Int32_Range (-Big (A)),
- Post => Big (To_Neg_Int'Result) = -Big (A);
+ Pre => In_Int32_Range (-Big (A)),
+ Post => Big (To_Neg_Int'Result) = -Big (A);
-- Convert to negative integer equivalent. If the input is in the range
-- 0 .. 2**31, then the corresponding nonpositive signed integer (obtained
-- by negating the given value) is returned, otherwise constraint error is
function To_Pos_Int (A : Uns32) return Int32
with
- Annotate => (GNATprove, Always_Return),
- Pre => In_Int32_Range (Big (A)),
- Post => Big (To_Pos_Int'Result) = Big (A);
+ Pre => In_Int32_Range (Big (A)),
+ Post => Big (To_Pos_Int'Result) = Big (A);
-- Convert to positive integer equivalent. If the input is in the range
-- 0 .. 2**31 - 1, then the corresponding nonnegative signed integer is
-- returned, otherwise constraint error is raised.
-- of no strict aliasing.
function To_Pointer (Value : Address) return Object_Pointer with
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
function To_Address (Value : Object_Pointer) return Address with
- SPARK_Mode => Off,
- Annotate => (GNATprove, Always_Return);
+ SPARK_Mode => Off;
pragma Import (Intrinsic, To_Pointer);
pragma Import (Intrinsic, To_Address);
package System.SPARK.Cut_Operations with
SPARK_Mode,
Pure,
- Annotate => (GNATprove, Always_Return)
+ Always_Terminates
is
function By (Consequence, Premise : Boolean) return Boolean with
-- extra declarations that can be introduced into System using Extend_System.
-- It is a good idea to avoid use clauses for this package.
-package System.Storage_Elements is
+package System.Storage_Elements with
+ Always_Terminates
+is
pragma Pure;
-- Note that we take advantage of the implementation permission to make
-- this unit Pure instead of Preelaborable; see RM 13.7.1(15). In Ada 2005,
pragma No_Elaboration_Code_All;
-- Allow the use of that restriction in units that WITH this unit
- pragma Annotate (GNATprove, Always_Return, Storage_Elements);
-
type Storage_Offset is range -Memory_Size / 2 .. Memory_Size / 2 - 1;
subtype Storage_Count is Storage_Offset range 0 .. Storage_Offset'Last;
package System.Value_I_Spec with
Ghost,
SPARK_Mode,
- Annotate => (GNATprove, Always_Return)
+ Always_Terminates
is
pragma Preelaborate;
use all type Uns_Params.Uns_Option;
package System.Value_U_Spec with
Ghost,
SPARK_Mode,
- Annotate => (GNATprove, Always_Return)
+ Always_Terminates
is
pragma Preelaborate;
projects / thirdparty / gcc.git / commitdiff
