1---------------------------------------------------------------- 2-- IRONSIDES - DNS SERVER 3-- 4-- By: Martin C. Carlisle and Barry S. Fagin 5-- Department of Computer Science 6-- United States Air Force Academy 7-- 8-- This is free software; you can redistribute it and/or 9-- modify without restriction. We do ask that you please keep 10-- the original author information, and clearly indicate if the 11-- software has been modified. 12-- 13-- This software is distributed in the hope that it will be useful, 14-- but WITHOUT ANY WARRANTY; without even the implied warranty 15-- of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. 16---------------------------------------------------------------- 17 18------------------------------------------------------------------------------- 19-- (C) Altran Praxis Limited 20-- modified by Martin Carlisle to add Argument function 21------------------------------------------------------------------------------- 22-- 23-- The SPARK toolset is free software; you can redistribute it and/or modify it 24-- under terms of the GNU General Public License as published by the Free 25-- Software Foundation; either version 3, or (at your option) any later 26-- version. The SPARK toolset is distributed in the hope that it will be 27-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of 28-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General 29-- Public License for more details. You should have received a copy of the GNU 30-- General Public License distributed with the SPARK toolset; see file 31-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of 32-- the license. 33-- 34--============================================================================= 35 36------------------------------------------------------------------------------- 37-- -- 38-- SPARK.Ada.Command_Line -- 39-- -- 40-- Description -- 41-- This is a binding to package Ada.Command_Line -- 42-- -- 43-- Language -- 44-- Specification : SPARK -- 45-- Private Part : SPARK -- 46-- Body : Ada -- 47-- -- 48-- Runtime Requirements and Dependencies -- 49-- Full Ada Runtime -- 50-- -- 51-- Verification -- 52-- N/A -- 53-- -- 54-- Exceptions -- 55-- None -- 56------------------------------------------------------------------------------- 57with Spark.Ada.Text_IO; 58--# inherit Spark.Ada.Text_IO; 59 60package SPARK_Ada_Command_Line 61--# own State; 62--# initializes State; 63is 64 65 -- function Argument_Count return Natural; 66 function Argument_Count return Natural; 67 --# global State; 68 69 procedure Create_File_From_Argument(Number : in Natural; 70 file : out Spark.Ada.Text_IO.File_Type); 71 --# global State; 72 --# derives file from number, State; 73 74 75 type Exit_Status is new Integer; 76 77 Success : constant Exit_Status; 78 Failure : constant Exit_Status; 79 80 -- procedure Exit_With_Status (Code : Exit_Status); 81 procedure Exit_With_Status (Code : in Exit_Status); 82 --# derives null from Code; 83 84private 85 Success : constant Exit_Status := 0; 86 Failure : constant Exit_Status := 1; 87end SPARK_Ada_Command_Line; 88