           *******************************************************
                            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.  
      ----------------------------------------------------------------
      
      -------------------------------------------------------------------------------
      -- (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.
      --
      --=============================================================================
      
      with Ada.Command_Line;
           ^
---        Warning           :  1: The identifier Ada is either undeclared or not 
           visible at this point.

      with Ada.Text_IO;
           ^
---        Warning           :  1: The identifier Ada is either undeclared or not 
           visible at this point.

      with Spark.Ada.Text_IO;
      with Gnat.Os_Lib;
           ^
---        Warning           :391: If the identifier Gnat 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.

      use type Spark.Ada.Text_IO.Exception_T;
      
      package body SPARK_Ada_Command_Line is
         --# hide SPARK_Ada_Command_Line;
      
         function Argument_Count return Natural is
         begin
            return Standard.Ada.Command_Line.Argument_Count;
         end Argument_Count;
      
      
         procedure Create_File_From_Argument(Number : in Natural;
            File : out Spark.Ada.Text_IO.File_Type) is
         begin
            if Argument_Count /= 1 then
               Ada.Text_IO.Put_Line(File => Ada.Text_IO.Standard_Error,
                  Item => "Usage: " & Standard.Ada.Command_Line.Command_Name &
                     " input_file");
               Gnat.Os_Lib.OS_Exit(1);
            end if;
            Spark.Ada.Text_IO.Open(File => File,
                                   Mode => Spark.Ada.Text_IO.In_File,
                                   Name => Standard.Ada.Command_Line.Argument(Number),
                                   Form => "");
            if Spark.Ada.Text_IO.Get_Last_Exception_File(File) /=
                  Spark.Ada.Text_IO.No_Exception then
               Ada.Text_IO.Put_Line(File => Ada.Text_IO.Standard_Error,
                  Item => Standard.Ada.Command_Line.Argument(Number) & ": not valid file");
               Gnat.Os_Lib.OS_Exit(1);
            end if;
         end Create_File_From_Argument;
      
      
      
         procedure Exit_With_Status (Code : in Exit_Status) is
         begin
            Gnat.Os_Lib.Os_Exit(Integer(Code));
         end Exit_With_Status;
      
      end SPARK_Ada_Command_Line;

---        Warning           : 10: The body of package SPARK_Ada_Command_Line is 
           hidden - hidden text is ignored by the Examiner.


Note: Flow analysis mode is automatic


--End of file--------------------------------------------------
