108 lines
4.6 KiB
Plaintext
108 lines
4.6 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.
|
|
----------------------------------------------------------------
|
|
|
|
-------------------------------------------------------------------------------
|
|
-- (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.
|
|
|
|
|
|
|
|
--End of file--------------------------------------------------
|