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