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