844 lines
31 KiB
Plaintext
844 lines
31 KiB
Plaintext
*******************************************************
|
|
Listing of SPARK Text
|
|
Examiner GPL Edition
|
|
|
|
*******************************************************
|
|
|
|
|
|
Line
|
|
----------------------------------------------------------------
|
|
-- IRONSIDES - DNS SERVER
|
|
--
|
|
-- By: Martin C. Carlisle and Barry S. Fagin
|
|
-- Department of Computer Science
|
|
-- United States Air Force Academy
|
|
--
|
|
-- This is free software; you can redistribute it and/or
|
|
-- modify without restriction. We do ask that you please keep
|
|
-- the original author information, and clearly indicate if the
|
|
-- software has been modified.
|
|
--
|
|
-- This software is distributed in the hope that it will be useful,
|
|
-- but WITHOUT ANY WARRANTY; without even the implied warranty
|
|
-- of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
|
|
----------------------------------------------------------------
|
|
|
|
with Text_IO;
|
|
^
|
|
--- Warning :391: If the identifier Text_IO represents a package
|
|
which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
with Unchecked_Deallocation;
|
|
^
|
|
--- Warning :391: If the identifier Unchecked_Deallocation
|
|
represents a package which contains a task or an interrupt handler
|
|
then the partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
|
|
|
|
package body Protected_Spark_Io_05 is
|
|
--# hide Protected_SPARK_IO_05;
|
|
|
|
type File_System is
|
|
record
|
|
Standard_Input : File_Type;
|
|
Standard_Output : File_Type;
|
|
end record;
|
|
File_System_Standard_Input : aliased File_Descriptor :=
|
|
File_Descriptor'(File_Ref => Text_IO.Standard_Input);
|
|
File_System_Standard_Output : aliased File_Descriptor :=
|
|
File_Descriptor'(File_Ref => Text_IO.Standard_Output);
|
|
|
|
File_Sys : constant File_System :=
|
|
File_System'(Standard_Input => File_System_Standard_Input'access,
|
|
Standard_Output => File_System_Standard_Output'access);
|
|
|
|
package Integer_IO is new Text_IO.Integer_IO (Integer);
|
|
package Real_IO is new Text_IO.Float_IO (Float);
|
|
|
|
|
|
procedure Dispose is new Unchecked_Deallocation
|
|
(File_Descriptor, File_Type);
|
|
|
|
|
|
-------------------------------------------------------------------------------
|
|
-- (C) Altran Praxis Limited
|
|
-------------------------------------------------------------------------------
|
|
--
|
|
-- The SPARK toolset is free software; you can redistribute it and/or modify it
|
|
-- under terms of the GNU General Public License as published by the Free
|
|
-- Software Foundation; either version 3, or (at your option) any later
|
|
-- version. The SPARK toolset is distributed in the hope that it will be
|
|
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
|
|
-- Public License for more details. You should have received a copy of the GNU
|
|
-- General Public License distributed with the SPARK toolset; see file
|
|
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
|
|
-- the license.
|
|
--
|
|
--=============================================================================
|
|
|
|
protected body SPARK_IO_05
|
|
is
|
|
--# hide SPARK_IO_05;
|
|
|
|
-- File Management
|
|
|
|
|
|
|
|
function Standard_Input return File_Type
|
|
is
|
|
begin
|
|
return File_Sys.Standard_Input;
|
|
end Standard_Input;
|
|
|
|
function Standard_Output return File_Type
|
|
is
|
|
begin
|
|
return File_Sys.Standard_Output;
|
|
end Standard_Output;
|
|
|
|
procedure Create (File : out File_Type;
|
|
Name_Of_File : in String;
|
|
Form_Of_File : in String;
|
|
Status : out File_Status)
|
|
is
|
|
begin
|
|
Create_Flex (File => File,
|
|
Name_Length => Name_Of_File'Length,
|
|
Name_Of_File => Name_Of_File,
|
|
Form_Of_File => Form_Of_File,
|
|
Status => Status);
|
|
end Create;
|
|
|
|
procedure Create_Flex (File : out File_Type;
|
|
Name_Length : in Natural;
|
|
Name_Of_File : in String;
|
|
Form_Of_File : in String;
|
|
Status : out File_Status)
|
|
is
|
|
begin
|
|
File := new File_Descriptor;
|
|
Text_IO.Create (File.File_Ref,
|
|
Text_IO.Out_File,
|
|
Name_Of_File (Name_Of_File'First .. Name_Length),
|
|
Form_Of_File);
|
|
Status := Ok;
|
|
exception
|
|
when Text_IO.Status_Error =>
|
|
Status := Status_Error;
|
|
Dispose (File);
|
|
when Text_IO.Name_Error =>
|
|
Status := Name_Error;
|
|
Dispose (File);
|
|
when Text_IO.Use_Error =>
|
|
Status := Use_Error;
|
|
Dispose (File);
|
|
when Text_IO.Device_Error =>
|
|
Status := Device_Error;
|
|
Dispose (File);
|
|
when Standard.Storage_Error =>
|
|
Status := Storage_Error;
|
|
Dispose (File);
|
|
when Standard.Program_Error =>
|
|
Status := Program_Error;
|
|
Dispose (File);
|
|
end Create_Flex;
|
|
|
|
procedure Open (File : out File_Type;
|
|
Mode_Of_File : in File_Mode;
|
|
Name_Of_File : in String;
|
|
Form_Of_File : in String;
|
|
Status : out File_Status)
|
|
is
|
|
begin
|
|
Open_Flex (File => File,
|
|
Mode_Of_File => Mode_Of_File,
|
|
Name_Length => Name_Of_File'Length,
|
|
Name_Of_File => Name_Of_File,
|
|
Form_Of_File => Form_Of_File,
|
|
Status => Status);
|
|
end Open;
|
|
|
|
procedure Open_Flex (File : out File_Type;
|
|
Mode_Of_File : in File_Mode;
|
|
Name_Length : in Natural;
|
|
Name_Of_File : in String;
|
|
Form_Of_File : in String;
|
|
Status : out File_Status)
|
|
is
|
|
F_Mode : Text_IO.File_Mode;
|
|
begin
|
|
File := new File_Descriptor;
|
|
case Mode_Of_File is
|
|
when In_File => F_Mode := Text_IO.In_File;
|
|
when Out_File => F_Mode := Text_IO.Out_File;
|
|
when Append_File => F_Mode := Text_IO.Append_File;
|
|
end case;
|
|
Text_IO.Open (File.File_Ref,
|
|
F_Mode,
|
|
Name_Of_File (Name_Of_File'First .. Name_Length),
|
|
Form_Of_File);
|
|
Status := Ok;
|
|
exception
|
|
when Text_IO.Status_Error =>
|
|
Status := Status_Error;
|
|
Dispose (File);
|
|
when Text_IO.Name_Error =>
|
|
Status := Name_Error;
|
|
Dispose (File);
|
|
when Text_IO.Use_Error =>
|
|
Status := Use_Error;
|
|
Dispose (File);
|
|
when Text_IO.Device_Error =>
|
|
Status := Device_Error;
|
|
Dispose (File);
|
|
when Standard.Storage_Error =>
|
|
Status := Storage_Error;
|
|
Dispose (File);
|
|
when Standard.Program_Error =>
|
|
Status := Program_Error;
|
|
Dispose (File);
|
|
end Open_Flex;
|
|
|
|
procedure Close (File : in out File_Type;
|
|
Status : out File_Status)
|
|
is
|
|
begin
|
|
if File = null then
|
|
Status := Status_Error;
|
|
else
|
|
Text_IO.Close (File.File_Ref);
|
|
Dispose (File);
|
|
Status := Ok;
|
|
end if;
|
|
exception
|
|
when Text_IO.Status_Error =>
|
|
Status := Status_Error;
|
|
Dispose (File);
|
|
when Text_IO.Device_Error =>
|
|
Status := Device_Error;
|
|
Dispose (File);
|
|
when Constraint_Error =>
|
|
Status := Use_Error;
|
|
Dispose (File);
|
|
when Standard.Storage_Error =>
|
|
Status := Storage_Error;
|
|
Dispose (File);
|
|
when Standard.Program_Error =>
|
|
Status := Program_Error;
|
|
Dispose (File);
|
|
end Close;
|
|
|
|
procedure Delete (File : in out File_Type;
|
|
Status : out File_Status)
|
|
is
|
|
begin
|
|
if File = null then
|
|
Status := Status_Error;
|
|
else
|
|
Text_IO.Delete (File.File_Ref);
|
|
Dispose (File);
|
|
Status := Ok;
|
|
end if;
|
|
exception
|
|
when Text_IO.Status_Error =>
|
|
Status := Status_Error;
|
|
Dispose (File);
|
|
when Text_IO.Use_Error =>
|
|
Status := Use_Error;
|
|
Dispose (File);
|
|
when Text_IO.Device_Error =>
|
|
Status := Device_Error;
|
|
Dispose (File);
|
|
when Constraint_Error =>
|
|
Status := Use_Error;
|
|
Dispose (File);
|
|
when Standard.Storage_Error =>
|
|
Status := Storage_Error;
|
|
Dispose (File);
|
|
when Standard.Program_Error =>
|
|
Status := Program_Error;
|
|
Dispose (File);
|
|
end Delete;
|
|
|
|
procedure Reset (File : in out File_Type;
|
|
Mode_Of_File : in File_Mode;
|
|
Status : out File_Status)
|
|
is
|
|
F_Mode : Text_IO.File_Mode;
|
|
begin
|
|
if File = null then
|
|
Status := Status_Error;
|
|
else
|
|
case Mode_Of_File is
|
|
when In_File => F_Mode := Text_IO.In_File;
|
|
when Out_File => F_Mode := Text_IO.Out_File;
|
|
when Append_File => F_Mode := Text_IO.Append_File;
|
|
end case;
|
|
Text_IO.Reset (File.File_Ref,
|
|
F_Mode);
|
|
Status := Ok;
|
|
end if;
|
|
exception
|
|
when Text_IO.Status_Error =>
|
|
Status := Status_Error;
|
|
Dispose (File);
|
|
when Text_IO.Use_Error =>
|
|
Status := Use_Error;
|
|
Dispose (File);
|
|
when Text_IO.Device_Error =>
|
|
Status := Device_Error;
|
|
Dispose (File);
|
|
when Standard.Storage_Error =>
|
|
Status := Storage_Error;
|
|
Dispose (File);
|
|
when Standard.Program_Error =>
|
|
Status := Program_Error;
|
|
Dispose (File);
|
|
end Reset;
|
|
|
|
function Valid_File (File : File_Type) return Boolean
|
|
is
|
|
begin
|
|
return File /= null;
|
|
end Valid_File;
|
|
|
|
function Is_Open (File : File_Type) return Boolean
|
|
is
|
|
begin
|
|
return Valid_File (File) and then
|
|
Text_IO.Is_Open (File.File_Ref);
|
|
end Is_Open;
|
|
|
|
function Mode (File : File_Type) return File_Mode
|
|
is
|
|
F_Mode : File_Mode;
|
|
begin
|
|
if Is_Open (File) and then
|
|
Text_IO.Is_Open (File.File_Ref) then
|
|
case Text_IO.Mode (File.File_Ref) is
|
|
when Text_IO.In_File =>
|
|
F_Mode := In_File;
|
|
when Text_IO.Out_File =>
|
|
F_Mode := Out_File;
|
|
when Text_IO.Append_File =>
|
|
F_Mode := Append_File;
|
|
end case;
|
|
else
|
|
F_Mode := In_File;
|
|
end if;
|
|
return F_Mode;
|
|
end Mode;
|
|
|
|
function Is_In (File : File_Type) return Boolean;
|
|
|
|
function Is_In (File : File_Type) return Boolean
|
|
is
|
|
begin
|
|
return Is_Open (File) and then Mode (File) = In_File;
|
|
end Is_In;
|
|
|
|
function Is_Out (File : File_Type) return Boolean;
|
|
|
|
function Is_Out (File : File_Type) return Boolean
|
|
is
|
|
begin
|
|
return Is_Open (File) and then (Mode (File) = Out_File or
|
|
Mode (File) = Append_File);
|
|
end Is_Out;
|
|
|
|
procedure Name (File : in File_Type;
|
|
Name_Of_File : out String;
|
|
Stop : out Natural)
|
|
is
|
|
begin
|
|
if Is_Open (File) then
|
|
declare
|
|
FN : constant String := Text_IO.Name (File.File_Ref);
|
|
begin
|
|
if Name_Of_File'Length >= FN'Length then
|
|
Name_Of_File (FN'range) := FN;
|
|
Stop := FN'Length;
|
|
else
|
|
Name_Of_File := FN (Name_Of_File'range);
|
|
Stop := Name_Of_File'Length;
|
|
end if;
|
|
end;
|
|
else
|
|
Stop := Name_Of_File'First - 1;
|
|
end if;
|
|
exception
|
|
when others => Stop := Name_Of_File'First - 1;
|
|
end Name;
|
|
|
|
procedure Form (File : in File_Type;
|
|
Form_Of_File : out String;
|
|
Stop : out Natural)
|
|
is
|
|
begin
|
|
if Is_Open (File) then
|
|
declare
|
|
FM : constant String := Text_IO.Form (File.File_Ref);
|
|
begin
|
|
if Form_Of_File'Length >= FM'Length then
|
|
Form_Of_File (FM'range) := FM;
|
|
Stop := FM'Length;
|
|
else
|
|
Form_Of_File := FM (Form_Of_File'range);
|
|
Stop := Form_Of_File'Length;
|
|
end if;
|
|
end;
|
|
else
|
|
Stop := Form_Of_File'First - 1;
|
|
end if;
|
|
exception
|
|
when others => Stop := Form_Of_File'First - 1;
|
|
end Form;
|
|
|
|
-- Line and file terminator control
|
|
|
|
function P_To_PC (P : Positive) return Text_IO.Positive_Count;
|
|
|
|
function P_To_PC (P : Positive) return Text_IO.Positive_Count
|
|
is
|
|
begin
|
|
return Text_IO.Positive_Count (P);
|
|
end P_To_PC;
|
|
|
|
function PC_To_P (PC : Text_IO.Positive_Count) return Positive;
|
|
|
|
function PC_To_P (PC : Text_IO.Positive_Count) return Positive
|
|
is
|
|
begin
|
|
return Positive (PC);
|
|
end PC_To_P;
|
|
|
|
procedure New_Line (File : in File_Type;
|
|
Spacing : in Positive)
|
|
is
|
|
Gap : Text_IO.Positive_Count;
|
|
begin
|
|
if Is_Out (File) then
|
|
Gap := P_To_PC (Spacing);
|
|
Text_IO.New_Line (File.File_Ref, Gap);
|
|
end if;
|
|
exception
|
|
when others => null;
|
|
end New_Line;
|
|
|
|
procedure Skip_Line (File : in File_Type;
|
|
Spacing : in Positive)
|
|
is
|
|
Gap : Text_IO.Positive_Count;
|
|
begin
|
|
if Is_In (File) then
|
|
Gap := P_To_PC (Spacing);
|
|
Text_IO.Skip_Line (File.File_Ref, Gap);
|
|
end if;
|
|
exception
|
|
when others => null;
|
|
end Skip_Line;
|
|
|
|
procedure New_Page (File : in File_Type)
|
|
is
|
|
begin
|
|
if Is_Out (File) then
|
|
Text_IO.New_Page (File.File_Ref);
|
|
end if;
|
|
exception
|
|
when others => null;
|
|
end New_Page;
|
|
|
|
function End_Of_Line (File : File_Type) return Boolean
|
|
is
|
|
EOLN : Boolean;
|
|
begin
|
|
if Is_In (File) then
|
|
EOLN := Text_IO.End_Of_Line (File.File_Ref);
|
|
else
|
|
EOLN := False;
|
|
end if;
|
|
return EOLN;
|
|
end End_Of_Line;
|
|
|
|
function End_Of_File (File : File_Type) return Boolean
|
|
is
|
|
EOF : Boolean;
|
|
begin
|
|
if Is_In (File) then
|
|
EOF := Text_IO.End_Of_File (File.File_Ref);
|
|
else
|
|
EOF := True;
|
|
end if;
|
|
return EOF;
|
|
end End_Of_File;
|
|
|
|
procedure Set_Col (File : in File_Type;
|
|
Posn : in Positive);
|
|
|
|
procedure Set_Col (File : in File_Type;
|
|
Posn : in Positive)
|
|
is
|
|
Col : Text_IO.Positive_Count;
|
|
begin
|
|
if Is_Open (File) then
|
|
Col := P_To_PC (Posn);
|
|
Text_IO.Set_Col (File.File_Ref, Col);
|
|
end if;
|
|
exception
|
|
when others => null;
|
|
end Set_Col;
|
|
|
|
procedure Set_In_File_Col (File : in File_Type;
|
|
Posn : in Positive)
|
|
is
|
|
begin
|
|
if Is_In (File) then
|
|
Set_Col (File, Posn);
|
|
end if;
|
|
end Set_In_File_Col;
|
|
|
|
procedure Set_Out_File_Col (File : in File_Type;
|
|
Posn : in Positive)
|
|
is
|
|
begin
|
|
if Is_Out (File) then
|
|
Set_Col (File, Posn);
|
|
end if;
|
|
end Set_Out_File_Col;
|
|
|
|
function Col (File : File_Type) return Positive;
|
|
|
|
function Col (File : File_Type) return Positive
|
|
is
|
|
Posn : Positive;
|
|
Col : Text_IO.Positive_Count;
|
|
begin
|
|
if Is_Open (File) then
|
|
Col := Text_IO.Col (File.File_Ref);
|
|
Posn := PC_To_P (Col);
|
|
else
|
|
Posn := 1;
|
|
end if;
|
|
return Posn;
|
|
exception
|
|
when Text_IO.Status_Error => return 1;
|
|
when Text_IO.Layout_Error => return PC_To_P (Text_IO.Count'Last);
|
|
when Text_IO.Device_Error => return 1;
|
|
when Standard.Storage_Error => return 1;
|
|
when Standard.Program_Error => return 1;
|
|
end Col;
|
|
|
|
function In_File_Col (File : File_Type) return Positive
|
|
is
|
|
begin
|
|
if Is_In (File) then
|
|
return Col (File);
|
|
else
|
|
return 1;
|
|
end if;
|
|
end In_File_Col;
|
|
|
|
function Out_File_Col (File : File_Type) return Positive
|
|
is
|
|
begin
|
|
if Is_Out (File) then
|
|
return Col (File);
|
|
else
|
|
return 1;
|
|
end if;
|
|
end Out_File_Col;
|
|
|
|
function Line (File : File_Type) return Positive;
|
|
|
|
function Line (File : File_Type) return Positive
|
|
is
|
|
Posn : Positive;
|
|
Line : Text_IO.Positive_Count;
|
|
begin
|
|
if Is_Open (File) then
|
|
Line := Text_IO.Line (File.File_Ref);
|
|
Posn := PC_To_P (Line);
|
|
else
|
|
Posn := 1;
|
|
end if;
|
|
return Posn;
|
|
exception
|
|
when Text_IO.Status_Error => return 1;
|
|
when Text_IO.Layout_Error => return PC_To_P (Text_IO.Count'Last);
|
|
when Text_IO.Device_Error => return 1;
|
|
when Standard.Storage_Error => return 1;
|
|
when Standard.Program_Error => return 1;
|
|
end Line;
|
|
|
|
function In_File_Line (File : File_Type) return Positive
|
|
is
|
|
begin
|
|
if Is_In (File) then
|
|
return Line (File);
|
|
else
|
|
return 1;
|
|
end if;
|
|
end In_File_Line;
|
|
|
|
function Out_File_Line (File : File_Type) return Positive
|
|
is
|
|
begin
|
|
if Is_Out (File) then
|
|
return Line (File);
|
|
else
|
|
return 1;
|
|
end if;
|
|
end Out_File_Line;
|
|
|
|
-- Character IO
|
|
|
|
procedure Get_Char (File : in File_Type;
|
|
Item : out Character)
|
|
is
|
|
begin
|
|
if Is_In (File) then
|
|
Text_IO.Get (File.File_Ref, Item);
|
|
else
|
|
Item := Character'First;
|
|
end if;
|
|
exception
|
|
when others => null;
|
|
end Get_Char;
|
|
|
|
procedure Put_Char (File : in File_Type;
|
|
Item : in Character)
|
|
is
|
|
begin
|
|
if Is_Out (File) then
|
|
Text_IO.Put (File.File_Ref, Item);
|
|
end if;
|
|
exception
|
|
when others => null;
|
|
end Put_Char;
|
|
|
|
procedure Get_Char_Immediate (File : in File_Type;
|
|
Item : out Character;
|
|
Status : out File_Status)
|
|
is
|
|
begin
|
|
if Is_In (File) then
|
|
Text_IO.Get_Immediate (File.File_Ref, Item);
|
|
Status := Ok;
|
|
else
|
|
Item := Character'First;
|
|
Status := Mode_Error;
|
|
end if;
|
|
exception
|
|
when others =>
|
|
Item := Character'First;
|
|
Status := End_Error;
|
|
end Get_Char_Immediate;
|
|
|
|
-- String IO
|
|
|
|
procedure Get_String (File : in File_Type;
|
|
Item : out String;
|
|
Stop : out Natural)
|
|
is
|
|
LSTP : Natural;
|
|
begin
|
|
if Is_In (File) then
|
|
LSTP := Item'First - 1;
|
|
loop
|
|
exit when End_Of_File (File);
|
|
LSTP := LSTP + 1;
|
|
Get_Char (File, Item (LSTP));
|
|
exit when LSTP = Item'Last;
|
|
end loop;
|
|
Stop := LSTP;
|
|
else
|
|
Stop := Item'First - 1;
|
|
end if;
|
|
end Get_String;
|
|
|
|
-- CFR 718 The behaviour of Put_String is now as follows:
|
|
-- If Stop is 0 then all characters in Item are output.
|
|
-- If Stop <= Item'Last then output Item(Item'First .. Stop).
|
|
-- If Stop > Item'Last then output all characters in Item, then pad with
|
|
-- spaces to width specified by Stop.
|
|
procedure Put_String (File : in File_Type;
|
|
Item : in String;
|
|
Stop : in Natural)
|
|
is
|
|
Pad : Natural;
|
|
begin
|
|
if Is_Out (File) then
|
|
if Stop = 0 then
|
|
Text_IO.Put (File.File_Ref, Item);
|
|
elsif Stop <= Item'Last then
|
|
Text_IO.Put (File.File_Ref, Item (Item'First .. Stop));
|
|
else
|
|
Pad := Stop - Item'Last;
|
|
Text_IO.Put (File.File_Ref, Item);
|
|
while Pad > 0 loop
|
|
Text_IO.Put (File.File_Ref, ' ');
|
|
Pad := Pad - 1;
|
|
end loop;
|
|
end if;
|
|
end if;
|
|
exception
|
|
when others => null;
|
|
end Put_String;
|
|
|
|
procedure Get_Line (File : in File_Type;
|
|
Item : out String;
|
|
Stop : out Natural)
|
|
is
|
|
begin
|
|
if Is_In (File) then
|
|
Text_IO.Get_Line (File.File_Ref, Item, Stop);
|
|
else
|
|
Stop := Item'First - 1;
|
|
end if;
|
|
exception
|
|
when others => Stop := Item'First - 1;
|
|
end Get_Line;
|
|
|
|
procedure Put_Line (File : in File_Type;
|
|
Item : in String;
|
|
Stop : in Natural)
|
|
is
|
|
ES : Positive;
|
|
begin
|
|
if Stop = 0 then
|
|
ES := Item'Last;
|
|
else
|
|
ES := Stop;
|
|
end if;
|
|
if Is_Out (File) then
|
|
Text_IO.Put_Line (File.File_Ref, Item (Item'First .. ES));
|
|
end if;
|
|
exception
|
|
when others => null;
|
|
end Put_Line;
|
|
|
|
|
|
-- Integer IO
|
|
|
|
procedure Get_Integer (File : in File_Type;
|
|
Item : out Integer;
|
|
Width : in Natural;
|
|
Read : out Boolean)
|
|
is
|
|
begin
|
|
if Is_In (File) then
|
|
Integer_IO.Get (File.File_Ref, Item, Width);
|
|
Read := True;
|
|
else
|
|
Read := False;
|
|
end if;
|
|
exception
|
|
when others => Read := False;
|
|
end Get_Integer;
|
|
|
|
procedure Put_Integer (File : in File_Type;
|
|
Item : in Integer;
|
|
Width : in Natural;
|
|
Base : in Number_Base)
|
|
is
|
|
begin
|
|
if Is_Out (File) then
|
|
Integer_IO.Put (File.File_Ref, Item, Width, Base);
|
|
end if;
|
|
exception
|
|
when others => null;
|
|
end Put_Integer;
|
|
|
|
procedure Get_Int_From_String (Source : in String;
|
|
Item : out Integer;
|
|
Start_Pos : in Positive;
|
|
Stop : out Natural)
|
|
is
|
|
begin
|
|
Integer_IO.Get (Source (Start_Pos .. Source'Last), Item, Stop);
|
|
exception
|
|
when others => Stop := Start_Pos - 1;
|
|
end Get_Int_From_String;
|
|
|
|
procedure Put_Int_To_String (Dest : in out String;
|
|
Item : in Integer;
|
|
Start_Pos : in Positive;
|
|
Base : in Number_Base)
|
|
is
|
|
begin
|
|
Integer_IO.Put (Dest (Start_Pos .. Dest'Last), Item, Base);
|
|
exception
|
|
when others => null;
|
|
end Put_Int_To_String;
|
|
|
|
|
|
-- Float IO
|
|
|
|
procedure Get_Float (File : in File_Type;
|
|
Item : out Float;
|
|
Width : in Natural;
|
|
Read : out Boolean)
|
|
is
|
|
begin
|
|
if Is_In (File) then
|
|
Real_IO.Get (File.File_Ref, Item, Width);
|
|
Read := True;
|
|
else
|
|
Read := False;
|
|
end if;
|
|
exception
|
|
when others => Read := False;
|
|
end Get_Float;
|
|
|
|
procedure Put_Float (File : in File_Type;
|
|
Item : in Float;
|
|
Fore : in Natural;
|
|
Aft : in Natural;
|
|
Exp : in Natural)
|
|
is
|
|
begin
|
|
if Is_Out (File) then
|
|
Real_IO.Put (File.File_Ref, Item, Fore, Aft, Exp);
|
|
end if;
|
|
exception
|
|
when others => null;
|
|
end Put_Float;
|
|
|
|
procedure Get_Float_From_String (Source : in String;
|
|
Item : out Float;
|
|
Start_Pos : in Positive;
|
|
Stop : out Natural)
|
|
is
|
|
begin
|
|
Real_IO.Get (Source (Start_Pos .. Source'Last), Item, Stop);
|
|
exception
|
|
when others => Stop := Start_Pos - 1;
|
|
end Get_Float_From_String;
|
|
|
|
procedure Put_Float_To_String (Dest : in out String;
|
|
Item : in Float;
|
|
Start_Pos : in Positive;
|
|
Aft : in Natural;
|
|
Exp : in Natural)
|
|
is
|
|
begin
|
|
Real_IO.Put (Dest (Start_Pos .. Dest'Last), Item, Aft, Exp);
|
|
exception
|
|
when others => null;
|
|
end Put_Float_To_String;
|
|
|
|
end SPARK_IO_05;
|
|
end Protected_Spark_Io_05;
|
|
|
|
--- Warning : 10: The body of package Protected_Spark_Io_05 is
|
|
hidden - hidden text is ignored by the Examiner.
|
|
|
|
|
|
|
|
--End of file--------------------------------------------------
|