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
18WITH Dns_Types, Rr_Type, Rr_Type.Aaaa_Record_Type, Rr_Type.Dnskey_Record_Type,
19   Rr_Type.Rrsig_Record_Type, Unsigned_Types;
20USE TYPE Unsigned_Types.Unsigned16, Unsigned_Types.Unsigned32;
21--# inherit dns_types, Ada.Characters.Latin_1, Ada.Characters.Handling, error_msgs, rr_type, rr_type.a_record_type,
22--#   rr_type.aaaa_record_type, rr_type.dnskey_record_type, rr_type.rrsig_Record_Type,
23--#   rr_type.soa_record_type, unsigned_types, non_spark_stuff;
24
25--with Ada.Text_IO, Ada.Integer_Text_IO;
26
27PACKAGE Parser_Utilities IS
28
29   procedure CheckAndAppendOrigin(target : in out Rr_Type.DomainNameStringType;
30         Origin : in Rr_Type.DomainNameStringType;
31         CurrentLine : in rr_type.LineFromFileType;
32         LastPos : in Rr_Type.Linelengthindex;
33         LineCount : in unsigned_types.unsigned32;
34         Success : in out boolean);
35   --# derives target, success from target, origin, success
36   --# & null from currentLine, lastPos, lineCount;
37
38   procedure checkValidHostName(Name: Rr_Type.DomainNameStringType; success: in out boolean);
39      --# derives success from name, success;
40
41   procedure CheckValidSRVOwner(Name: Rr_Type.DomainNameStringType; success: in out boolean);
42      --# derives success from name, success;
43
44
45   procedure findFirstToken(s : in rr_type.LineFromFileType;
46                            length : in rr_type.LineLengthIndex;
47                            T : OUT Rr_Type.RrItemType);
48   --# derives T from s, length;
49
50   procedure findNextToken(s : in rr_type.LineFromFileType;
51                           length : in rr_type.LineLengthIndex;
52                           BegIdx : in OUT rr_type.LineLengthIndex;
53                           EndIdx : OUT rr_type.LineLengthIndex;
54                           T : OUT Rr_Type.RrItemType);
55   --# derives begIdx, endIdx, T from s, length, begIdx;
56   --# pre begIdx <= length;
57   --# post begIdx <= endIdx and begIdx <= length and endIdx <= length
58   --#  and ((T = rr_type.Number) ->
59   --#      (for all I in integer range begIdx..endIdx => (S(I) >= '0' and S(I) <= '9')));
60
61   procedure convert8BitUnsigned(value: out Unsigned_Types.Unsigned8;
62      ZoneFileLine : in rr_type.LineFromFileType;
63      BegIdx : in rr_type.LineLengthIndex;
64      EndIdx : in rr_type.LineLengthIndex;
65      Success : in out Boolean);
66   --# derives value from zoneFileLine, begIdx, endIdx & success from zoneFileLine, begIdx, endIdx, success;
67   --# pre for all I in integer range BegIdx..EndIdx => (ZoneFileLine(I) >= '0' and ZoneFileLine(I) <= '9');
68
69   procedure convert16BitUnsigned(value: out Unsigned_Types.Unsigned16;
70      ZoneFileLine : in rr_type.LineFromFileType;
71      BegIdx : in rr_type.LineLengthIndex;
72      EndIdx : in rr_type.LineLengthIndex;
73      Success : in out Boolean);
74   --# derives value from zoneFileLine, begIdx, endIdx & success from zoneFileLine, begIdx, endIdx, success;
75   --# pre for all I in integer range BegIdx..EndIdx => (ZoneFileLine(I) >= '0' and ZoneFileLine(I) <= '9');
76
77   procedure convert32BitUnsigned(value: out Unsigned_Types.Unsigned32;
78      ZoneFileLine : in rr_type.LineFromFileType;
79      BegIdx : in rr_type.LineLengthIndex;
80      EndIdx : in rr_type.LineLengthIndex;
81      Success : in out Boolean);
82   --# derives value from zoneFileLine, begIdx, endIdx & success from zoneFileLine, begIdx, endIdx, success;
83   --# pre for all I in integer range BegIdx..EndIdx => (ZoneFileLine(I) >= '0' and ZoneFileLine(I) <= '9');
84
85   procedure ConvertTimeSpec(S : in Rr_Type.LineFromFileType; begIdx: in rr_type.LineLengthIndex;
86      endIdx: in Rr_Type.LineLengthIndex; RetVal : out Unsigned_Types.Unsigned32; success: in out Boolean);
87   --# derives retVal,success from S, begIdx, endIdx, success;
88
89   procedure ConvertTimeString(TimeVal : out Unsigned_Types.Unsigned32;
90      TimeString: in Rr_Type.Rrsig_Record_Type.TimeStringType;
91      Success : in out Boolean);
92   --# derives timeVal from timeString & success from timeString, success;
93   --# pre for all I in Rr_Type.Rrsig_Record_Type.TimeStringTypeIndex => (timeString(I) >= '0' and timeString(I) <= '9');
94
95   procedure AddToKeyR(RRSIG_Rec : in out rr_type.rrsig_record_type.RRSIGRecordType;
96                      S: in Rr_Type.LineFromFileType;
97                      Length : in Rr_Type.LineLengthIndex;
98                      allDone : out boolean;
99                      success : in out boolean);
100   --# derives RRSIG_Rec from RRSIG_Rec, S, Length & AllDone from S, Length
101   --#   & Success from RRSIG_Rec, S, Length, Success;
102
103   procedure AddToKey(DNSKEY_Rec : in out rr_type.dnskey_record_type.DNSKeyRecordType;
104                      S: in Rr_Type.LineFromFileType;
105                      Length : in Rr_Type.LineLengthIndex;
106                      success : in out boolean);
107   --# derives DNSKEY_Rec from DNSKEY_Rec, S, Length & Success from DNSKEY_Rec, S, Length, Success;
108
109   function convertIpv4(s : in rr_type.LineFromFileType;
110                        begIdx: IN rr_type.LineLengthIndex;
111                        EndIdx: IN Rr_Type.LineLengthIndex) RETURN Unsigned_Types.Unsigned32;
112
113   function convertIpv6(s : in rr_type.LineFromFileType;
114                        begIdx: in rr_type.LineLengthIndex;
115                        endIdx: in rr_type.LineLengthIndex) RETURN rr_type.aaaa_record_type.IPV6AddrType;
116
117   function getRecordType(s : in rr_type.LineFromFileType;
118                          begIdx : in rr_type.LineLengthIndex;
119                    	  endIdx : in rr_type.LineLengthIndex) return dns_types.Query_Type;
120   --# pre begIdx <= endIdx;
121
122
123END Parser_Utilities;
124
125