Abstract_State => (Clock_Time with Synchronous),
Initializes => Clock_Time
is
+ pragma Annotate (GNATprove, Always_Return, Real_Time);
pragma Compile_Time_Error
(Duration'Size /= 64,
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.
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.
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.
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,
-- 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.
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.
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.
pragma Pure;
-- In accordance with Ada 2005 AI-362
+ pragma Annotate (GNATprove, Always_Return, Handling);
+
----------------------------------------
-- Character Classification Functions --
----------------------------------------
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.
-- 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,
-- 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),
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;
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;
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;
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
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);
package Ada.Strings.Bounded with SPARK_Mode is
pragma Preelaborate;
+ pragma Annotate (GNATprove, Always_Return, Bounded);
generic
Max : Positive;
Post => Ignore,
Contract_Cases => Ignore,
Ghost => Ignore);
+ pragma Annotate (GNATprove, Always_Return, Generic_Bounded_Length);
Max_Length : constant Positive := Max;
-- 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:
others
=>
Index'Result = 0),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
pragma Ada_05 (Index);
function Index
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
others
=>
Index'Result = 0),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
function Index
(Source : String;
others
=>
Index'Result = 0),
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
-- If Going = Forward, returns:
--
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;
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
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)
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
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
(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.
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
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)
------------------------------------
(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;
(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
(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)
(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:
--
Justify : Alignment := Left;
Pad : Character := Space)
with
- Pre =>
+ Pre =>
Low - 1 <= Source'Last
and then High >= Source'First - 1
and then (if High >= Low
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- 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;
+ 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)
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
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
(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
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
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- 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;
+ 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.
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),
(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;
+ 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
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Trim (Source, Side), Source, Justify=>Justify, Pad=>Pad).
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.
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Trim (Source, Left, Right),
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.
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Head (Source, Count, Pad),
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.
-- Incomplete contract
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
-- 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;
+ Global => null,
+ Annotate => (GNATprove, Always_Return);
function "*"
(Left : Natural;
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
pragma Pure;
-- In accordance with Ada 2005 AI-362
+ pragma Annotate (GNATprove, Always_Return, Maps);
+
--------------------------------
-- Character Set Declarations --
--------------------------------
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
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;
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;
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;
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 --
-- 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 =>
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 =>
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);
(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 --
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;
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;
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;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
private
pragma Inline (Get);
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;
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;
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;
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;
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;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
private
pragma Inline (Get);
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;
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;
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;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp)
with
- Global => null;
+ Global => null,
+ Annotate => (GNATprove, Might_Not_Return);
private
pragma Inline (Get);
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;
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);
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;
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);
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,
package Interfaces is
pragma No_Elaboration_Code_All;
pragma Pure;
+ pragma Annotate (GNATprove, Always_Return, Interfaces);
-- All identifiers in this unit are implementation defined
package Interfaces is
pragma No_Elaboration_Code_All;
pragma Pure;
+ pragma Annotate (GNATprove, Always_Return, Interfaces);
-- All identifiers in this unit are implementation defined
-- 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);
-- 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
projects / thirdparty / gcc.git / commitdiff
