88 lines
4.2 KiB
Ada
88 lines
4.2 KiB
Ada
----------------------------------------------------------------
|
|
-- 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
|
|
-- modified by Martin Carlisle to add Argument function
|
|
-------------------------------------------------------------------------------
|
|
--
|
|
-- 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.
|
|
--
|
|
--=============================================================================
|
|
|
|
-------------------------------------------------------------------------------
|
|
-- --
|
|
-- SPARK.Ada.Command_Line --
|
|
-- --
|
|
-- Description --
|
|
-- This is a binding to package Ada.Command_Line --
|
|
-- --
|
|
-- Language --
|
|
-- Specification : SPARK --
|
|
-- Private Part : SPARK --
|
|
-- Body : Ada --
|
|
-- --
|
|
-- Runtime Requirements and Dependencies --
|
|
-- Full Ada Runtime --
|
|
-- --
|
|
-- Verification --
|
|
-- N/A --
|
|
-- --
|
|
-- Exceptions --
|
|
-- None --
|
|
-------------------------------------------------------------------------------
|
|
with Spark.Ada.Text_IO;
|
|
--# inherit Spark.Ada.Text_IO;
|
|
|
|
package SPARK_Ada_Command_Line
|
|
--# own State;
|
|
--# initializes State;
|
|
is
|
|
|
|
-- function Argument_Count return Natural;
|
|
function Argument_Count return Natural;
|
|
--# global State;
|
|
|
|
procedure Create_File_From_Argument(Number : in Natural;
|
|
file : out Spark.Ada.Text_IO.File_Type);
|
|
--# global State;
|
|
--# derives file from number, State;
|
|
|
|
|
|
type Exit_Status is new Integer;
|
|
|
|
Success : constant Exit_Status;
|
|
Failure : constant Exit_Status;
|
|
|
|
-- procedure Exit_With_Status (Code : Exit_Status);
|
|
procedure Exit_With_Status (Code : in Exit_Status);
|
|
--# derives null from Code;
|
|
|
|
private
|
|
Success : constant Exit_Status := 0;
|
|
Failure : constant Exit_Status := 1;
|
|
end SPARK_Ada_Command_Line;
|