gnatprove_11.2.3_f7ece6d3/share/examples/spark/tokeneer/spark_io.adb

------------------------------------------------------------------
-- Tokeneer ID Station Support Software
--
-- Copyright (2003) United States Government, as represented
-- by the Director, National Security Agency. All rights reserved.
--
-- This material was originally developed by Praxis High Integrity
-- Systems Ltd. under contract to the National Security Agency.
------------------------------------------------------------------

pragma Ada_95;
package body Spark_IO is
   pragma SPARK_Mode (Off);
-- File Management

  procedure Create (File         :    out File_Type;
                    Name_Of_File : in     String;
                    Form_Of_File : in     String;
                    Status       :    out File_Status)
  is
  begin
    Status := Ok;
    File.File := new Ada.Text_IO.File_Type;
    Ada.Text_IO.Create ( File.File.all, Ada.Text_IO.Out_File,
                     Name_Of_File,  Form_Of_File);
  exception
    when Ada.Text_IO.Status_Error  => Status := Status_Error;
    when Ada.Text_IO.Name_Error    => Status := Name_Error;
    when Ada.Text_IO.Use_Error     => Status := Use_Error;
    when Ada.Text_IO.Device_Error  => Status := Device_Error;
    when Standard.Storage_Error    => Status := Storage_Error;
    when Standard.Program_Error    => Status := Program_Error;
  end Create;

  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
    Fmode : Ada.Text_IO.File_Mode;
  begin
    case Mode_Of_File is
      when In_File     => Fmode := Ada.Text_IO.In_File;
      when Out_File    => Fmode := Ada.Text_IO.Out_File;
      when Append_File => Fmode := Ada.Text_IO.Append_File;
    end case;
    Status := Ok;
    File.File := new Ada.Text_IO.File_Type;
    Ada.Text_IO.Open( File.File.all, Fmode, Name_Of_File, Form_Of_File);
  exception
    when Ada.Text_IO.Status_Error  => Status := Status_Error;
    when Ada.Text_IO.Name_Error    => Status := Name_Error;
    when Ada.Text_IO.Use_Error     => Status := Use_Error;
    when Ada.Text_IO.Device_Error  => Status := Device_Error;
    when Standard.Storage_Error    => Status := Storage_Error;
    when Standard.Program_Error    => Status := Program_Error;
  end Open;

  procedure Close (File   : in     File_Type;
                   Status :    out File_Status)
  is
  begin
    Ada.Text_IO.Close( File.File.all);
    Status := Ok;
  exception
    when Constraint_Error         => Status := Use_Error;
    when Ada.Text_IO.Status_Error => Status := Status_Error;
    when Ada.Text_IO.Device_Error => Status := Device_Error;
    when Standard.Storage_Error   => Status := Storage_Error;
    when Standard.Program_Error   => Status := Program_Error;
  end Close;

  procedure Delete (File   : in     File_Type;
                    Status :    out File_Status)
  is
  begin
    Ada.Text_IO.Delete( File.File.all);
    Status := Ok;
  exception
    when Ada.Text_IO.Status_Error => Status := Status_Error;
    when Ada.Text_IO.Use_Error    => Status := Use_Error;
    when Constraint_Error         => Status := Use_Error;
    when Ada.Text_IO.Device_Error => Status := Device_Error;
    when Standard.Storage_Error   => Status := Storage_Error;
    when Standard.Program_Error   => Status := Program_Error;
  end Delete;

  procedure Reset( File         : in out File_Type;
                   Mode_Of_File : in     File_Mode;
                   Status       :    out File_Status)
  is
    Fmode : Ada.Text_IO.File_Mode;
  begin
    case Mode_Of_File is
      when In_File     => Fmode := Ada.Text_IO.In_File;
      when Out_File    => Fmode := Ada.Text_IO.Out_File;
      when Append_File => Fmode := Ada.Text_IO.Append_File;
    end case;
    Ada.Text_IO.Reset( File.File.all, Fmode);
    Status := Ok;
  exception
    when Ada.Text_IO.Status_Error => Status := Status_Error;
    when Ada.Text_IO.Use_Error    => Status := Use_Error;
    when Ada.Text_IO.Device_Error => Status := Device_Error;
    when Standard.Storage_Error   => Status := Storage_Error;
    when Standard.Program_Error   => Status := Program_Error;
  end Reset;

  function Valid_File (File : File_Type) return Boolean
  is
    Valid : Boolean;
  begin
    case File.IO_Sort is
      when Stdin     => Valid := True;
      when Stdout    => Valid := True;
      when NamedFile => Valid := (File.File /= null);
    end case;
    return Valid;
  end Valid_File;

  function File_Ref (File : File_Type) return Ada.Text_IO.File_Type
  is
  begin
    case File.IO_Sort is
      when Stdin     => return Ada.Text_IO.Standard_Input;
      when Stdout    => return Ada.Text_IO.Standard_Output;
      when NamedFile =>
         pragma Warnings (Off, "cannot copy object of a limited type in Ada 2005");
         return File.File.all;
         pragma Warnings (On, "cannot copy object of a limited type in Ada 2005");
    end case;
  end File_Ref;

  function Is_Open( File : File_Type) return Boolean
  is
  begin
    return Valid_File( File) and then
           Ada.Text_IO.Is_Open( File_Ref( File));
  end Is_Open;

  function Mode( File : File_Type) return File_Mode
  is
    Fmode : File_Mode;
  begin
    if Is_Open( File) and then
       Ada.Text_IO.Is_Open( File_Ref( File)) then
      case Ada.Text_IO.Mode( File_Ref( File)) is
        when Ada.Text_IO.In_File     => Fmode := In_File;
        when Ada.Text_IO.Out_File    => Fmode := Out_File;
        when Ada.Text_IO.Append_File => Fmode := Append_File;
      end case;
    else
      Fmode := In_File;
    end if;
    return Fmode;
  end Mode;

  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
  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 := Ada.Text_IO.Name( File_Ref( File));
      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 := Ada.Text_IO.Form( File_Ref( File));
      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 Ada.Text_IO.Positive_Count
  is
    PC : Ada.Text_IO.Positive_Count;
  begin
    if P > Positive( Ada.Text_IO.Positive_Count'Last) then
      PC := Ada.Text_IO.Positive_Count'Last;
    else
      PC := Ada.Text_IO.Positive_Count( P);
    end if;
    return PC;
  end P_To_PC;

  function PC_To_P(PC : Ada.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    : Ada.Text_IO.Positive_Count;
  begin
    if Is_Out( File) then
      Gap := P_To_PC( Spacing);
      Ada.Text_IO.New_Line( File_Ref( File), Gap);
    end if;
  exception
    when others => null;
  end New_Line;

  procedure Skip_Line( File    : in File_Type;
                       Spacing : in Positive)
  is
    Gap    : Ada.Text_IO.Positive_Count;
  begin
    if Is_In( File) then
      Gap := P_To_PC( Spacing);
      Ada.Text_IO.Skip_Line( File_Ref( File), Gap);
    end if;
  exception
    when others => null;
  end Skip_Line;

  procedure New_Page ( File : in File_Type)
  is
  begin
    if Is_Out( File) then
      Ada.Text_IO.New_Page( File_Ref( File));
    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 := Ada.Text_IO.End_Of_Line( File_Ref( File));
    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 := Ada.Text_IO.End_Of_File( File_Ref( File));
    else
      EOF := True;
    end if;
    return EOF;
  end End_Of_File;

  procedure Set_Col (File : in File_Type;
                     Posn : in Positive)
  is
    Col    : Ada.Text_IO.Positive_Count;
  begin
    if Is_Open( File) then
      Col := P_To_PC( Posn);
      Ada.Text_IO.Set_Col( File_Ref( File), 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
  is
    Posn : Positive;
    Col  : Ada.Text_IO.Positive_Count;
  begin
    if Is_Open( File) then
      Col := Ada.Text_IO.Col( File_Ref( File));
      Posn := Pc_To_P( Col);
    else
      Posn := 1;
    end if;
    return Posn;
  exception
    when Ada.Text_IO.Status_Error => return 1;
    when Ada.Text_IO.Layout_Error => return PC_To_P( Ada.Text_IO.Count'Last);
    when Ada.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
  is
    Posn : Positive;
    Line : Ada.Text_IO.Positive_Count;
  begin
    if Is_Open( File) then
      Line := Ada.Text_IO.Line( File_Ref( File));
      Posn := PC_To_P( Line);
    else
      Posn := 1;
    end if;
    return Posn;
  exception
    when Ada.Text_IO.Status_Error => return 1;
    when Ada.Text_IO.Layout_Error => return PC_To_P( Ada.Text_IO.Count'Last);
    when Ada.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
      Ada.Text_IO.Get( File_Ref( File), 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
      Ada.Text_IO.Put( File_Ref( File), Item);
    end if;
  exception
    when others => null;
  end Put_Char;


-- 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
        Ada.Text_IO.Put( File_Ref( File), Item);
      elsif Stop <= Item'Last then
        Ada.Text_IO.Put( File_Ref( File), Item( Item'First .. Stop));
      else
        Pad := Stop - Item'Last;
        Ada.Text_IO.Put( File_Ref( File), Item);
        while Pad > 0 loop
          Ada.Text_IO.Put( File_Ref( File), ' ');
          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
      Ada.Text_IO.Get_Line( File_Ref( File), 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
      Ada.Text_IO.Put_Line( File_Ref( File), Item( Item'First .. ES));
    end if;
  exception
    when others => null;
  end Put_Line;


-- Integer IO

  package Integer_IO is new Ada.Text_IO.Integer_IO( Integer);

  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_Ref( File), 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_Ref( File), 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

  package Real_IO is new Ada.Text_IO.Float_IO( Float);

  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_Ref( File), 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_Ref( File), 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;