@@ -102,16 +102,16 @@ is
function "+" (Left : Time; Right : Duration) return Time
with
- Global => null;
+ SPARK_Mode => Off;
function "+" (Left : Duration; Right : Time) return Time
with
- Global => null;
+ SPARK_Mode => Off;
function "-" (Left : Time; Right : Duration) return Time
with
- Global => null;
+ SPARK_Mode => Off;
function "-" (Left : Time; Right : Time) return Duration
with
- Global => null;
+ SPARK_Mode => Off;
-- The first three functions will raise Time_Error if the resulting time
-- value is less than the start of Ada time in UTC or greater than the
-- end of Ada time in UTC. The last function will raise Time_Error if the
@@ -116,14 +116,17 @@ is
Post => (if X = 0.0 then Tan'Result = 0.0);
function Tan (X, Cycle : Float_Type'Base) return Float_Type'Base with
+ SPARK_Mode => Off, -- Tan can overflow for some values of X and Cycle
Pre => Cycle > 0.0
and then abs Float_Type'Base'Remainder (X, Cycle) /= 0.25 * Cycle,
Post => (if X = 0.0 then Tan'Result = 0.0);
function Cot (X : Float_Type'Base) return Float_Type'Base with
+ SPARK_Mode => Off, -- Cot can overflow for some values of X
Pre => X /= 0.0;
function Cot (X, Cycle : Float_Type'Base) return Float_Type'Base with
+ SPARK_Mode => Off, -- Cot can overflow for some values of X and Cycle
Pre => Cycle > 0.0
and then X /= 0.0
and then Float_Type'Base'Remainder (X, Cycle) /= 0.0
@@ -176,9 +179,11 @@ is
Post => (if X > 0.0 and then Y = 0.0 then Arccot'Result = 0.0);
function Sinh (X : Float_Type'Base) return Float_Type'Base with
+ SPARK_Mode => Off, -- Sinh can overflow for some values of X
Post => (if X = 0.0 then Sinh'Result = 0.0);
function Cosh (X : Float_Type'Base) return Float_Type'Base with
+ SPARK_Mode => Off, -- Cosh can overflow for some values of X
Post => Cosh'Result >= 1.0
and then (if X = 0.0 then Cosh'Result = 1.0);
@@ -187,6 +192,7 @@ is
and then (if X = 0.0 then Tanh'Result = 0.0);
function Coth (X : Float_Type'Base) return Float_Type'Base with
+ SPARK_Mode => Off, -- Coth can overflow for some values of X
Pre => X /= 0.0,
Post => abs Coth'Result >= 1.0;
@@ -132,11 +132,13 @@ is
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),
Annotate => (GNATprove, Might_Not_Return);
+
procedure Reset (File : in out File_Type; Mode : File_Mode) with
Pre => Is_Open (File),
Post =>
@@ -147,6 +149,7 @@ is
and then Page_Length (File) = 0)),
Global => (In_Out => File_System),
Annotate => (GNATprove, Might_Not_Return);
+
procedure Reset (File : in out File_Type) with
Pre => Is_Open (File),
Post =>
@@ -159,21 +162,19 @@ is
Annotate => (GNATprove, Might_Not_Return);
function Mode (File : File_Type) return File_Mode with
- Pre => Is_Open (File),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Pre => Is_Open (File),
+ Global => null;
+
function Name (File : File_Type) return String with
- Pre => Is_Open (File),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Pre => Is_Open (File),
+ Global => null;
+
function Form (File : File_Type) return String with
- Pre => Is_Open (File),
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Pre => Is_Open (File),
+ Global => null;
function Is_Open (File : File_Type) return Boolean with
- Global => null,
- Annotate => (GNATprove, Always_Return);
+ Global => null;
------------------------------------------------------
-- Control of default input, output and error files --
@@ -215,6 +216,7 @@ is
and Page_Length (File)'Old = Page_Length (File),
Global => (In_Out => File_System),
Annotate => (GNATprove, Always_Return);
+
procedure Flush with
Post =>
Line_Length'Old = Line_Length
@@ -233,6 +235,7 @@ is
and Page_Length (File)'Old = Page_Length (File),
Global => (In_Out => File_System),
Annotate => (GNATprove, Might_Not_Return);
+
procedure Set_Line_Length (To : Count) with
Post =>
Line_Length = To
@@ -247,6 +250,7 @@ is
and Line_Length (File)'Old = Line_Length (File),
Global => (In_Out => File_System),
Annotate => (GNATprove, Might_Not_Return);
+
procedure Set_Page_Length (To : Count) with
Post =>
Page_Length = To
@@ -255,18 +259,18 @@ is
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),
- Annotate => (GNATprove, Always_Return);
+ Global => (Input => File_System);
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),
- Annotate => (GNATprove, Always_Return);
+ Global => (Input => File_System);
------------------------------------
-- Column, Line, and Page Control --
@@ -279,6 +283,7 @@ is
and Page_Length (File)'Old = Page_Length (File),
Global => (In_Out => File_System),
Annotate => (GNATprove, Always_Return);
+
procedure New_Line (Spacing : Positive_Count := 1) with
Post =>
Line_Length'Old = Line_Length
@@ -290,6 +295,7 @@ is
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 =>
Line_Length'Old = Line_Length
@@ -298,12 +304,11 @@ is
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),
- Annotate => (GNATprove, Always_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (Input => File_System);
+
function End_Of_Line return Boolean with
- Global => (Input => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (Input => File_System);
procedure New_Page (File : File_Type) with
Pre => Is_Open (File) and then Mode (File) /= In_File,
@@ -312,6 +317,7 @@ is
and Page_Length (File)'Old = Page_Length (File),
Global => (In_Out => File_System),
Annotate => (GNATprove, Always_Return);
+
procedure New_Page with
Post =>
Line_Length'Old = Line_Length
@@ -323,6 +329,7 @@ is
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 =>
Line_Length'Old = Line_Length
@@ -331,20 +338,18 @@ is
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),
- Annotate => (GNATprove, Always_Return);
+ Pre => Is_Open (File) and then Mode (File) = In_File,
+ Global => (Input => File_System);
+
function End_Of_Page return Boolean with
- Global => (Input => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (Input => File_System);
function End_Of_File (File : File_Type) return 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);
+
function End_Of_File return Boolean with
- Global => (Input => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (Input => File_System);
procedure Set_Col (File : File_Type; To : Positive_Count) with
Pre =>
@@ -359,6 +364,7 @@ is
others => True),
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 =>
@@ -380,6 +386,7 @@ is
others => True),
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 =>
@@ -389,28 +396,25 @@ is
Annotate => (GNATprove, Might_Not_Return);
function Col (File : File_Type) return Positive_Count with
- Pre => Is_Open (File),
- Global => (Input => File_System),
- Annotate => (GNATprove, Always_Return);
+ Pre => Is_Open (File),
+ Global => (Input => File_System);
+
function Col return Positive_Count with
- Global => (Input => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (Input => File_System);
function Line (File : File_Type) return Positive_Count with
- Pre => Is_Open (File),
- Global => (Input => File_System),
- Annotate => (GNATprove, Always_Return);
+ Pre => Is_Open (File),
+ Global => (Input => File_System);
+
function Line return Positive_Count with
- Global => (Input => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (Input => File_System);
function Page (File : File_Type) return Positive_Count with
- Pre => Is_Open (File),
- Global => (Input => File_System),
- Annotate => (GNATprove, Always_Return);
+ Pre => Is_Open (File),
+ Global => (Input => File_System);
+
function Page return Positive_Count with
- Global => (Input => File_System),
- Annotate => (GNATprove, Always_Return);
+ Global => (Input => File_System);
----------------------------
-- Character Input-Output --
@@ -420,12 +424,14 @@ is
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),
Annotate => (GNATprove, Might_Not_Return);
+
procedure Put (File : File_Type; Item : Character) with
Pre => Is_Open (File) and then Mode (File) /= In_File,
Post =>
@@ -433,6 +439,7 @@ is
and Page_Length (File)'Old = Page_Length (File),
Global => (In_Out => File_System),
Annotate => (GNATprove, Always_Return);
+
procedure Put (Item : Character) with
Post =>
Line_Length'Old = Line_Length
@@ -503,12 +510,14 @@ is
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 =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
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 =>
@@ -516,6 +525,7 @@ is
and Page_Length (File)'Old = Page_Length (File),
Global => (In_Out => File_System),
Annotate => (GNATprove, Always_Return);
+
procedure Put (Item : String) with
Post =>
Line_Length'Old = Line_Length
@@ -67,7 +67,7 @@ is
(Item : char_array_access;
Nul_Check : Boolean := False) return chars_ptr
with
- SPARK_Mode => Off;
+ SPARK_Mode => Off; -- To_Chars_Ptr'Result is aliased with Item
function New_Char_Array (Chars : char_array) return chars_ptr with
Volatile_Function,
@@ -118,13 +118,16 @@ is
Chars : char_array;
Check : Boolean := True)
with
- Pre =>
+ Pre =>
Item /= Null_Ptr
and then
(if Check then
Strlen (Item) <= size_t'Last - Offset
and then Strlen (Item) + Offset <= Chars'Length),
- Global => (In_Out => C_Memory);
+ 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.
procedure Update
(Item : chars_ptr;
@@ -132,13 +135,16 @@ is
Str : String;
Check : Boolean := True)
with
- Pre =>
+ Pre =>
Item /= Null_Ptr
and then
(if Check then
Strlen (Item) <= size_t'Last - Offset
and then Strlen (Item) + Offset <= Str'Length),
- Global => (In_Out => C_Memory);
+ 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.
Update_Error : exception;