978 lines
49 KiB
Plaintext
978 lines
49 KiB
Plaintext
*******************************************************
|
|
Listing of SPARK Text
|
|
Examiner GPL Edition
|
|
|
|
*******************************************************
|
|
|
|
|
|
Line
|
|
----------------------------------------------------------------
|
|
-- 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.
|
|
----------------------------------------------------------------
|
|
|
|
WITH Ada.Characters.Handling, Error_Msgs, Parser_Utilities, Rr_Type.Aaaa_Record_Type,
|
|
Rr_Type.Mx_Record_Type, Rr_Type.Soa_Record_Type,
|
|
dns_types, unsigned_types, Ada.Characters.Latin_1;
|
|
--With Ada.Text_IO, ada.Integer_Text_IO;
|
|
USE TYPE Rr_Type.RrItemType, Rr_Type.Aaaa_Record_Type.IPV6AddrType,
|
|
Dns_Types.Query_Type, Unsigned_Types.Unsigned32, Unsigned_Types.Unsigned16,
|
|
unsigned_types.Unsigned8;
|
|
|
|
package body zone_file_parser is
|
|
|
|
procedure ParseDNSKeyHeader(DNSKEY_Rec : out rr_type.dnskey_record_type.DNSKeyRecordType;
|
|
zoneFileLine : in rr_type.LineFromFileType;
|
|
ZLength : in Rr_Type.LineLengthIndex;
|
|
Success : in out Boolean)
|
|
is
|
|
CORRECT_PROTOCOL_VALUE : constant unsigned_types.Unsigned8 := 3;
|
|
begIdx : rr_type.LineLengthIndex := 1;
|
|
endIdx : rr_type.LineLengthIndex;
|
|
foundType : rr_type.rrItemType;
|
|
begin
|
|
--SPARK requires all fields of OUT parameter records be assigned
|
|
DNSKEY_Rec := Rr_Type.Dnskey_Record_Type.BlankDNSKeyRecord;
|
|
|
|
--find the record type indicator, which must be present since this routine was called
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
|
|
--second condition always true if precondition of routine is met, but it helps the prover
|
|
WHILE FoundType /= rr_type.RecordIndicator and endIdx < zlength LOOP
|
|
--# assert endIdx < zlength;
|
|
begIdx := ((begIdx-begIdx)+endIdx)+1; --makes flow error go away
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
END LOOP;
|
|
--parse FLAG field (unsigned 16-bit #)
|
|
if (endIdx = zLength) then
|
|
success := false;
|
|
else
|
|
BegIdx := EndIdx + 1;
|
|
parser_utilities.findNextToken(zoneFileLine, zLength, begIdx, endIdx, foundType);
|
|
if foundType /= rr_type.Number then
|
|
success := false;
|
|
ELSE --convert token to 16-bit number
|
|
parser_utilities.convert16BitUnsigned(DNSKEY_Rec.flags, zoneFileLine, begIdx, endIdx, success);
|
|
end if;
|
|
end if;
|
|
|
|
--parse PROTOCOL field (unsigned 8-bit #, must be 3)
|
|
if Success then
|
|
if (endIdx = zLength) then
|
|
success := false;
|
|
else
|
|
begIdx := endIdx + 1;
|
|
parser_utilities.findNextToken(zoneFileLine, zLength, begIdx, endIdx, foundType);
|
|
if foundType /= rr_type.Number then
|
|
success := false;
|
|
ELSE --convert token to unsigned 8-bit number
|
|
parser_utilities.convert8BitUnsigned(DNSKEY_Rec.protocol, zoneFileLine, begIdx, endIdx, success);
|
|
end if;
|
|
if DNSKEY_Rec.Protocol /= CORRECT_PROTOCOL_VALUE then
|
|
Success := False;
|
|
end if;
|
|
end if;
|
|
end if;
|
|
|
|
--parse ALGORITHM field (unsigned 8-bit #)
|
|
if Success then
|
|
if (endIdx = zLength) then
|
|
success := false;
|
|
else
|
|
begIdx := endIdx + 1;
|
|
parser_utilities.findNextToken(zoneFileLine, zLength, begIdx, endIdx, foundType);
|
|
if foundType /= rr_type.Number then
|
|
success := false;
|
|
ELSE --convert token to unsigned 8-bit number
|
|
parser_utilities.convert8BitUnsigned(DNSKEY_Rec.algorithm, zoneFileLine, begIdx, endIdx, success);
|
|
end if;
|
|
end if;
|
|
end if;
|
|
end ParseDNSKeyHeader;
|
|
|
|
+++ Flow analysis of subprogram ParseDNSKeyHeader
|
|
performed: no errors found.
|
|
|
|
|
|
procedure ParseRRSig2ndLine(RRSIG_Rec: out rr_type.rrsig_record_type.RRSIGRecordType;
|
|
zoneFileLine : in rr_type.LineFromFileType;
|
|
ZLength : in Rr_Type.LineLengthIndex;
|
|
Success : in out Boolean)
|
|
is
|
|
BegIdx : Rr_Type.LineLengthIndex;
|
|
EndIdx : Rr_Type.LineLengthIndex;
|
|
LengthOfToken : Rr_Type.LineLengthIndex;
|
|
FoundType : Rr_Type.RrItemType;
|
|
TimeString : Rr_Type.Rrsig_Record_Type.TimeStringType :=
|
|
Rr_Type.Rrsig_Record_Type.TimeStringType'(others => ' ');
|
|
begin
|
|
RRSIG_Rec := Rr_Type.Rrsig_Record_Type.BlankRRSIGRecord;
|
|
--parse SIG_INCEPTION field (YYYYMMDDHHmmSS or unsigned 32-bit #)
|
|
begIdx := 1;
|
|
parser_utilities.findNextToken(zoneFileLine, zLength, begIdx, endIdx, foundType);
|
|
Success := Success and (foundType = rr_type.Number); --fail if not a number
|
|
|
|
if Success then --next token is a number
|
|
--convert token to unsigned 32-bit number
|
|
--If it's not of length timeStringLength, can't be YYYYMMDDHHmmSS
|
|
if ((EndIdx-BegIdx)+1 /= rr_type.rrsig_record_type.timeStringLength) then
|
|
Parser_Utilities.Convert32BitUnsigned(RRSIG_Rec.OrigTTL, ZoneFileLine,
|
|
BegIdx, EndIdx, Success);
|
|
else --convert YYYYMMDDHHmmSS to #secs since 1 Jan 1970 00:00:00 UTC
|
|
for I in Rr_Type.Rrsig_Record_Type.TimeStringTypeIndex loop
|
|
--# assert begIdx = begIdx% and endIdx = endIdx% and zLength = zlength%
|
|
--# and endIdx <= zLength
|
|
--# and endIdx-begIdx = rr_type.rrsig_record_type.timeStringLength-1
|
|
--# and I <= Rr_Type.Rrsig_Record_Type.TimeStringTypeIndex'Last;
|
|
TimeString(I) := ZoneFileLine(BegIdx+(I-1));
|
|
end loop;
|
|
--establish and prove the precondition for convertTimeString (all numbers)
|
|
for I in Rr_Type.Rrsig_Record_Type.TimeStringTypeIndex loop
|
|
--# assert for all J in Integer range 1..I-1 => (TimeString(J) >= '0' and TimeString(J) <= '9');
|
|
if (TimeString(I) < '0' or TimeString(I) > '9') then
|
|
Success := False;
|
|
exit;
|
|
end if;
|
|
end loop;
|
|
if Success then
|
|
parser_utilities.convertTimeString(RRSIG_Rec.SigInception, TimeString, Success);
|
|
end if;
|
|
end if; --timeString or simple number
|
|
end if; --successful so far
|
|
|
|
--KEY_TAG
|
|
Success := Success and (EndIdx < ZLength); --fail if at EOL
|
|
if Success then
|
|
begIdx := endIdx + 1;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
Success := (FoundType = Rr_Type.Number);
|
|
if Success then
|
|
Parser_Utilities.Convert16BitUnsigned(RRSIG_Rec.KeyTag, ZoneFileLine, BegIdx,
|
|
EndIdx, Success);
|
|
end if;
|
|
end if;
|
|
|
|
--SIGNER_NAME
|
|
Success := Success and (EndIdx < ZLength); --fail if at EOL
|
|
if Success then
|
|
begIdx := endIdx + 1;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
Success := (FoundType = Rr_Type.DomainNameOrTimeSpec);
|
|
if Success then
|
|
--SPARK caught these parens in the wrong place, nice!
|
|
LengthofToken := (EndIdx-BegIdx)+1;
|
|
if LengthOfToken > Rr_Type.MaxDomainNameLength then
|
|
success := false;
|
|
Error_Msgs.PrintDomainLengthErrorInfo(ZoneFileLine, BegIdx, EndIdx);
|
|
else
|
|
--have a domain name, but must still pad it
|
|
for I in Integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
--# and endIdx = endIdx%;
|
|
RRSIG_Rec.signerName((I+1)-begIdx) := ZoneFileLine(I);
|
|
end loop;
|
|
for I in Integer range endIdx+1..rr_type.maxDomainNameLength loop
|
|
-- Remind prover that endIdx is in type
|
|
--# assert endIdx >= 1;
|
|
RRSIG_Rec.signerName(I) := ' ';
|
|
end loop;
|
|
end if;
|
|
end if;
|
|
end if;
|
|
|
|
--to do
|
|
end ParseRRSig2ndLine;
|
|
|
|
+++ Flow analysis of subprogram ParseRRSig2ndLine
|
|
performed: no errors found.
|
|
|
|
|
|
--this is only called from ParseRRSigHeader, created because otherwise ParseRRSigHeader
|
|
--is too complex for Examiner
|
|
procedure ParseTypeCoveredAlgorithmNumLabels(RRSIG_Rec : in out Rr_Type.Rrsig_Record_Type.RRSIGRecordType;
|
|
ZoneFileLine : in Rr_Type.LineFromFileType;
|
|
ZLength : in Rr_Type.LineLengthIndex;
|
|
EndIdx : in out Rr_Type.LineLengthIndex;
|
|
Success : in out Boolean)
|
|
--# derives RRSIG_Rec from RRSIG_Rec, zoneFileLine, zLength, endIDx, success
|
|
--# & endIdx, success from zoneFileLine, zLength, endIdx, success;
|
|
is
|
|
begIdx : rr_type.LineLengthIndex;
|
|
FoundType : Rr_Type.RrItemType;
|
|
begin
|
|
|
|
--TYPE_COVERED
|
|
Success := Success and (EndIdx < ZLength); --fail if at EOL
|
|
if Success then
|
|
begIdx := endIdx + 1;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
Success := (FoundType = Rr_Type.RecordIndicator);
|
|
if Success then
|
|
RRSIG_Rec.TypeCovered := Parser_Utilities.GetRecordType(ZoneFileLine, BegIdx, EndIdx);
|
|
end if;
|
|
end if;
|
|
|
|
--ALGORITHM
|
|
Success := Success and (EndIdx < ZLength); --fail if at EOL
|
|
if Success then
|
|
begIdx := endIdx + 1;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
Success := (FoundType = Rr_Type.Number);
|
|
if Success then
|
|
Parser_Utilities.Convert8BitUnsigned(RRSIG_Rec.Algorithm, ZoneFileLine, BegIdx,
|
|
EndIdx, Success);
|
|
end if;
|
|
end if;
|
|
|
|
--NUM_LABELS
|
|
Success := Success and (EndIdx <ZLength); --fail if at EOL
|
|
if Success then
|
|
begIdx := endIdx + 1;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
Success := (FoundType = Rr_Type.Number);
|
|
if Success then
|
|
Parser_Utilities.Convert8BitUnsigned(RRSIG_Rec.NumLabels, ZoneFileLine, BegIdx,
|
|
EndIdx, Success);
|
|
end if;
|
|
end if;
|
|
|
|
end ParseTypeCoveredAlgorithmNumLabels;
|
|
|
|
+++ Flow analysis of subprogram
|
|
ParseTypeCoveredAlgorithmNumLabels performed: no errors found.
|
|
|
|
|
|
procedure ParseRRSigHeader(RRSIG_Rec: out rr_type.rrsig_record_type.RRSIGRecordType;
|
|
zoneFileLine : in rr_type.LineFromFileType;
|
|
ZLength : in Rr_Type.LineLengthIndex;
|
|
Success : in out Boolean)
|
|
is
|
|
begIdx : rr_type.LineLengthIndex := 1;
|
|
endIdx : rr_type.LineLengthIndex;
|
|
FoundType : Rr_Type.RrItemType;
|
|
|
|
TimeString : Rr_Type.Rrsig_Record_Type.TimeStringType :=
|
|
Rr_Type.Rrsig_Record_Type.TimeStringType'(others => ' ');
|
|
|
|
begin
|
|
RRSIG_Rec := Rr_Type.Rrsig_Record_Type.BlankRRSIGRecord;
|
|
|
|
--find the record type indicator (RRSIG), which must be present since this routine was called
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
|
|
--second condition always true if precondition of routine is met, but it helps the prover
|
|
WHILE FoundType /= rr_type.RecordIndicator and endIdx < zlength LOOP
|
|
--# assert endIdx < zlength;
|
|
begIdx := ((begIdx-begIdx)+endIdx)+1; --makes flow error go away
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
END LOOP;
|
|
|
|
--parse TYPE_COVERED, ALGORITHM and NUM_LABELS fields
|
|
ParseTypeCoveredAlgorithmNumLabels(RRSIG_Rec, ZoneFileLine, ZLength, EndIdx, Success);
|
|
|
|
--parse ORIG_TTL field (time spec)
|
|
Success := Success and (endIdx < zLength); --fail if at EOL
|
|
if Success then
|
|
begIdx := endIdx + 1;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
if FoundType = Rr_Type.Number then
|
|
Parser_Utilities.Convert32BitUnsigned(RRSIG_Rec.OrigTTL, ZoneFileLine, BegIdx, EndIdx,
|
|
Success);
|
|
elsif FoundType = rr_type.DomainNameOrTimeSpec then
|
|
Parser_Utilities.ConvertTimeSpec(ZoneFileLine, BegIdx, EndIdx, RRSIG_Rec.OrigTTL,
|
|
Success);
|
|
else
|
|
Success := false;
|
|
end if;
|
|
end if;
|
|
|
|
--parse SIG_EXPIRATION field (YYYYMMDDHHmmSS or unsigned 32-bit #)
|
|
Success := Success and (endIdx < zLength); --fail if at EOL
|
|
if Success then
|
|
begIdx := endIdx + 1;
|
|
parser_utilities.findNextToken(zoneFileLine, zLength, begIdx, endIdx, foundType);
|
|
Success := (foundType = rr_type.Number); --fail if not a number
|
|
end if;
|
|
|
|
if Success then --next token is a number
|
|
--convert token to unsigned 32-bit number
|
|
--If it's not of length timeStringLength, can't be YYYYMMDDHHmmSS
|
|
if ((EndIdx-BegIdx)+1 /= rr_type.rrsig_record_type.timeStringLength) then
|
|
Parser_Utilities.Convert32BitUnsigned(RRSIG_Rec.OrigTTL, ZoneFileLine,
|
|
BegIdx, EndIdx, Success);
|
|
else --convert YYYYMMDDHHmmSS to #secs since 1 Jan 1970 00:00:00 UTC
|
|
for I in Rr_Type.Rrsig_Record_Type.TimeStringTypeIndex loop
|
|
--# assert begIdx = begIdx% and endIdx = endIdx% and zLength = zlength%
|
|
--# and endIdx <= zLength
|
|
--# and endIdx-begIdx = rr_type.rrsig_record_type.timeStringLength-1
|
|
--# and I <= Rr_Type.Rrsig_Record_Type.TimeStringTypeIndex'Last;
|
|
TimeString(I) := ZoneFileLine(BegIdx+(I-1));
|
|
end loop;
|
|
--establish and prove the precondition for convertTimeString (all numbers)
|
|
for I in Rr_Type.Rrsig_Record_Type.TimeStringTypeIndex loop
|
|
--# assert for all J in Integer range 1..I-1 => (TimeString(J) >= '0' and TimeString(J) <= '9');
|
|
if (TimeString(I) < '0' or TimeString(I) > '9') then
|
|
Success := False;
|
|
exit;
|
|
end if;
|
|
end loop;
|
|
if Success then
|
|
parser_utilities.convertTimeString(RRSIG_Rec.SigExpiration, TimeString, Success);
|
|
end if;
|
|
end if; --timeString or simple number
|
|
end if; --successful so far
|
|
|
|
--parse left paren
|
|
Success := Success and (endIdx < zLength); --fail if at EOL
|
|
if Success then
|
|
begIdx := endIdx + 1;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
--make bogus flow errors go away
|
|
if (FoundType /= Rr_Type.LParen) and (begIdx = begIdx) and (endIdx = endIdx) then
|
|
Success := False;
|
|
end if;
|
|
end if;
|
|
end ParseRRSigHeader;
|
|
|
|
+++ Flow analysis of subprogram ParseRRSigHeader
|
|
performed: no errors found.
|
|
|
|
|
|
|
|
--precondition is that zoneFileLine contains a record indicator, but can't
|
|
--express that in SPARK
|
|
procedure parseDomainName(newDomainName : out rr_type.DomainNameStringType;
|
|
zoneFileLine : in rr_type.LineFromFileType;
|
|
zLength : in rr_type.LineLengthIndex; success : in out boolean)
|
|
is
|
|
begIdx : rr_type.LineLengthIndex := 1;
|
|
endIdx : rr_type.LineLengthIndex;
|
|
foundType : rr_type.rrItemType;
|
|
lengthOfToken : rr_type.LineLengthIndex;
|
|
|
|
BEGIN
|
|
newDomainName := rr_type.blankDomainName;
|
|
--find the record type indicator, which must be present since this routine was called
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
|
|
--second condition always true if precondition of routine is met, but it helps the prover
|
|
WHILE FoundType/= rr_type.RecordIndicator and endIdx < zlength LOOP
|
|
--# assert endIdx < zlength;
|
|
begIdx := ((begIdx-begIdx)+endIdx)+1; --makes flow error go away
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
END LOOP;
|
|
|
|
--check to make sure something is after the record type, find its position if so
|
|
if (endIdx >= zLength) then
|
|
success := false;
|
|
else
|
|
begIdx := endIdx+1;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
--don't bother checking if FoundType is a domainName, just take whatever is there
|
|
LengthOfToken := (EndIdx-BegIdx)+1;
|
|
--superfluous test makes flow error go away
|
|
if (lengthOfToken > rr_type.MaxDomainNameLength and FoundType = FoundType) then
|
|
success := false;
|
|
Error_Msgs.PrintDomainLengthErrorInfo(ZoneFileLine, BegIdx, EndIdx);
|
|
else
|
|
--have a domain name, but must still pad it
|
|
for I in Integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
--# and endIdx = endIdx%;
|
|
NewDomainName((I+1)-begIdx) := ZoneFileLine(I);
|
|
end loop;
|
|
for I in Integer range endIdx+1..rr_type.maxDomainNameLength loop
|
|
-- Remind prover that endIdx is in type
|
|
--# assert endIdx >= 1;
|
|
newDomainName(I) := ' ';
|
|
end loop;
|
|
end if;
|
|
end if;
|
|
END ParseDomainName;
|
|
|
|
+++ Flow analysis of subprogram parseDomainName
|
|
performed: no errors found.
|
|
|
|
|
|
--just like ParseDomainName, but also grabs character string after it
|
|
procedure ParseDomainNameAndRRString(
|
|
NewDomainName : out Rr_Type.DomainNameStringType;
|
|
RRString : out Rr_type.LineFromFileType;
|
|
zoneFileLine : in rr_type.LineFromFileType;
|
|
ZLength : in Rr_Type.LineLengthIndex;
|
|
success : in out boolean)
|
|
is
|
|
begIdx : rr_type.LineLengthIndex := 1;
|
|
endIdx : rr_type.LineLengthIndex;
|
|
foundType : rr_type.rrItemType;
|
|
lengthOfToken : rr_type.LineLengthIndex;
|
|
|
|
BEGIN
|
|
RRString := rr_type.BlankLine;
|
|
newDomainName := rr_type.blankDomainName;
|
|
--find the record type indicator, which must be present since this routine was called
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
|
|
--second condition always true if precondition of routine is met, but it helps the prover
|
|
WHILE FoundType/= rr_type.RecordIndicator and endIdx < zlength LOOP
|
|
--# assert endIdx < zlength;
|
|
begIdx := ((begIdx-begIdx)+endIdx)+1; --makes flow error go away
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
END LOOP;
|
|
|
|
--check to make sure something is after the record type, find its position if so
|
|
if (endIdx >= zLength) then
|
|
success := false;
|
|
else
|
|
begIdx := endIdx+1;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
--don't bother checking if FoundType is a domainName, just take whatever is there
|
|
LengthOfToken := (EndIdx-BegIdx)+1;
|
|
--superfluous test makes flow error go away
|
|
if (lengthOfToken > rr_type.MaxDomainNameLength and FoundType = FoundType) then
|
|
success := false;
|
|
Error_Msgs.PrintDomainLengthErrorInfo(ZoneFileLine, BegIdx, EndIdx);
|
|
else
|
|
--have a domain name, but must still pad it
|
|
for I in Integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
--# and endIdx = endIdx%;
|
|
NewDomainName((I+1)-begIdx) := ZoneFileLine(I);
|
|
end loop;
|
|
for I in Integer range endIdx+1..rr_type.MaxDomainNameLength loop
|
|
-- Remind prover that endIdx is in type
|
|
--# assert endIdx >= 1;
|
|
newDomainName(I) := ' ';
|
|
end loop;
|
|
end if;
|
|
--this is the extra code
|
|
if (endIdx >= zLength) then
|
|
success := false;
|
|
else
|
|
BegIdx := EndIdx+1;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
--rrstring is everything after the domain name to the end of the line
|
|
EndIdx := (EndIdx - EndIdx) + ZLength; --make flow error go away
|
|
LengthOfToken := (EndIdx-BegIdx)+1;
|
|
--superfluous test makes flow error go away
|
|
--for now, rrstring length max is same as domain name length max
|
|
if (lengthOfToken > rr_type.MaxDomainNameLength and FoundType = FoundType) then
|
|
success := false;
|
|
Error_Msgs.PrintRRStringLengthErrorInfo(ZoneFileLine, BegIdx, EndIdx);
|
|
else
|
|
--have an rrstring, but must still pad it
|
|
for I in Integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
--# and endIdx = endIdx%;
|
|
RRString((I+1)-begIdx) := ZoneFileLine(I);
|
|
end loop;
|
|
for I in Integer range ((endIdx+2)-begIdx)..rr_type.lineLengthIndex'Last loop
|
|
-- Remind prover of postcondition from FindNextToken
|
|
--# assert endIdx >= begIdx;
|
|
RRString(I) := ' ';
|
|
end loop;
|
|
end if;
|
|
end if;
|
|
end if;
|
|
END ParseDomainNameAndRRString;
|
|
|
|
+++ Flow analysis of subprogram
|
|
ParseDomainNameAndRRString performed: no errors found.
|
|
|
|
|
|
procedure ParseTimeSpec(newTimeSpec : out Unsigned_Types.Unsigned32;
|
|
zoneFileLine : in Rr_Type.LineFromFileType;
|
|
zLength : in Rr_Type.LineLengthIndex; success : in out Boolean)
|
|
is
|
|
begIdx : rr_type.LineLengthIndex := 1;
|
|
endIdx : rr_type.LineLengthIndex;
|
|
foundType : rr_type.rrItemType;
|
|
begin
|
|
newTimeSpec := 0;
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
|
|
--next token must be a time specifier or number, otherwise error
|
|
if (foundType /= rr_type.DomainNameOrTimeSpec and foundType /= rr_type.Number) then
|
|
success := false;
|
|
else
|
|
parser_utilities.ConvertTimeSpec(zoneFileLine, begIdx, endIdx, newTimeSpec, success);
|
|
end if; --number found?
|
|
end ParseTimeSpec;
|
|
|
|
+++ Flow analysis of subprogram ParseTimeSpec
|
|
performed: no errors found.
|
|
|
|
|
|
procedure ParseControlLine(newOrigin : in out rr_type.DomainNameStringType;
|
|
NewTTL : in out Unsigned_Types.Unsigned32;
|
|
zoneFileLine : in rr_type.LineFromFileType;
|
|
ZLength : in Rr_Type.LineLengthIndex; Success : in out Boolean)
|
|
is
|
|
begIdx : rr_type.LineLengthIndex := 1;
|
|
EndIdx : Rr_Type.LineLengthIndex;
|
|
FoundType : Rr_Type.RrItemType;
|
|
TmpLine : rr_type.LineFromFileType := rr_type.LineFromFileType'(others => ' ');
|
|
begin
|
|
|
|
--find the control command, which must be present since this routine was called
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
if FoundType = Rr_Type.Control then --should always be true
|
|
--only $TTL and $ORIGIN currently recogznied
|
|
--phrasing conditions this way helps the prover
|
|
if BegIdx <= EndIdx-6 then --$ORIGIN?
|
|
if ZoneFileline(BegIdx+1) = 'O' and
|
|
ZoneFileline(BegIdx+2) = 'R' and
|
|
ZoneFileline(BegIdx+3) = 'I' and
|
|
ZoneFileline(BegIdx+4) = 'G' and
|
|
ZoneFileline(BegIdx+5) = 'I' and
|
|
ZoneFileline(BegIdx+6) = 'N' then
|
|
if begIdx < Zlength and endIdx < Zlength then
|
|
Begidx := EndIdx + 1;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
end if;
|
|
if FoundType /= Rr_Type.DomainNameOrTimeSpec then
|
|
Success := False;
|
|
elsif ZoneFileLine(EndIdx) /= '.' then
|
|
Success := False; --argument to $ORIGIN must end with '.'
|
|
else
|
|
--create a line with a dummy record indicator and the domain name
|
|
--so it can be parsed with ParseDomainName
|
|
for I in Integer range BegIdx..EndIdx loop
|
|
--# assert begIdx >= 1 and begIdx <= endIdx;
|
|
tmpLine(I) := zoneFileLine(I);
|
|
end loop;
|
|
--we know the domain name can't start before pos 6,
|
|
--so this will work
|
|
TmpLine(1) := 'A';
|
|
ParseDomainName(NewOrigin, TmpLine, Rr_Type.MaxLineLength, Success);
|
|
end if;
|
|
else
|
|
Success := False;
|
|
end if; --control token of length 6
|
|
elsif BegIdx <= EndIdx-3 then --$TTL?
|
|
if ZoneFileline(BegIdx+1) = 'T' and
|
|
ZoneFileline(BegIdx+2) = 'T' and
|
|
ZoneFileline(BegIdx+3) = 'L' then
|
|
if begIdx < Zlength and endIdx < Zlength then
|
|
Begidx := EndIdx + 1;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
end if;
|
|
if FoundType /= Rr_Type.DomainNameOrTimeSpec and FoundType /= Rr_Type.Number then
|
|
Success := False;
|
|
else
|
|
--create a line with only the time spec on it so it can be parsed
|
|
--with ParseTimeSpec
|
|
for I in Integer range BegIdx..EndIdx loop
|
|
--# assert begIdx >= 1 and begIdx <= endIdx;
|
|
tmpLine(I) := zoneFileLine(I);
|
|
end loop;
|
|
ParseTimeSpec(NewTTL, TmpLine, Rr_Type.MaxLineLength, Success);
|
|
|
|
end if;
|
|
else
|
|
Success := False;
|
|
end if; --control token of length 3
|
|
|
|
end if; --$TTL or $ORIGIN
|
|
else
|
|
Success := False;
|
|
end if; --whether or not control token found
|
|
end ParseControlLine;
|
|
|
|
+++ Flow analysis of subprogram ParseControlLine
|
|
performed: no errors found.
|
|
|
|
|
|
procedure parseSerialNumber(newSerialNumber : out unsigned_types.Unsigned32;
|
|
zoneFileLine : in rr_type.LineFromFileType;
|
|
ZLength : in Rr_Type.LineLengthIndex;
|
|
success : in out boolean)
|
|
is
|
|
begIdx : rr_type.LineLengthIndex := 1;
|
|
endIdx : rr_type.LineLengthIndex;
|
|
foundType : rr_type.rrItemType;
|
|
digitVal : unsigned_types.unsigned32;
|
|
TmpVal : long_long_integer;
|
|
|
|
BEGIN
|
|
newSerialNumber := 0;
|
|
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
|
|
--next token must be a number, otherwise error
|
|
if (foundType /= rr_type.Number) then
|
|
success := false;
|
|
else
|
|
tmpVal := 0;
|
|
for i in integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and tmpVal >= 0 and tmpVal <= rr_type.SOA_record_type.MAX_SERIAL_VAL;
|
|
digitVal := Character'Pos(zoneFileLine(I)) - Character'Pos('0');
|
|
TmpVal := 10*TmpVal + long_long_integer(digitVal);
|
|
--bail out early if serial# is too large
|
|
exit when tmpVal > rr_type.SOA_record_type.MAX_SERIAL_VAL;
|
|
end loop;
|
|
--make sure it's not too big
|
|
if tmpVal > rr_type.SOA_record_type.MAX_SERIAL_VAL then
|
|
success := false;
|
|
else --have a valid serial number
|
|
newSerialNumber := unsigned_types.unsigned32(tmpVal);
|
|
end if; --too large pref?
|
|
end if; --number found?
|
|
end ParseSerialNumber;
|
|
|
|
+++ Flow analysis of subprogram parseSerialNumber
|
|
performed: no errors found.
|
|
|
|
|
|
--precondition is that zoneFileLine contains a record indicator
|
|
--Data item after "MX" record indicator should be a valid 16-bit integer
|
|
procedure parsePrefandDomainName(newPref : out unsigned_types.Unsigned16;
|
|
newDomainName : out rr_type.DomainNameStringType;
|
|
zoneFileLine : in rr_type.LineFromFileType;
|
|
zLength : in rr_type.LineLengthIndex; success : in out boolean)
|
|
is
|
|
begIdx : rr_type.LineLengthIndex := 1;
|
|
endIdx : rr_type.LineLengthIndex;
|
|
foundType : rr_type.rrItemType;
|
|
digitVal : unsigned_types.unsigned16;
|
|
TmpVal : unsigned_types.unsigned16;
|
|
lengthofToken : rr_type.LineLengthIndex;
|
|
|
|
BEGIN
|
|
newPref := 0;
|
|
newDomainName := rr_type.blankDomainName;
|
|
|
|
--find the record type indicator, which must be present since this routine was called
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
|
|
--second condition always true if precondition of routine is met, but it helps the prover
|
|
WHILE FoundType/= rr_type.RecordIndicator and endIdx < zlength LOOP
|
|
--# assert endIdx < zlength;
|
|
begIdx := ((begIdx-begIdx)+endIdx)+1; --makes flow error go away
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
END LOOP;
|
|
|
|
--check to make sure something is after the record type, find its position if so
|
|
if (endIdx = zLength) then
|
|
success := false;
|
|
else
|
|
begIdx := endIdx + 1;
|
|
parser_utilities.findNextToken(zoneFileLine, zLength, begIdx, endIdx, foundType);
|
|
if foundType /= rr_type.Number then
|
|
success := false;
|
|
ELSE --convert token to number
|
|
tmpVal := 0;
|
|
for i in integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and tmpVal <= rr_type.mx_record_type.MAX_PREF_VAL;
|
|
digitVal := Character'Pos(zoneFileLine(I)) - Character'Pos('0');
|
|
TmpVal := 10*TmpVal + digitVal;
|
|
exit when tmpVal > rr_type.mx_record_type.MAX_PREF_VAL;
|
|
end loop;
|
|
--make sure it's not too big
|
|
if tmpVal > rr_type.mx_record_type.MAX_PREF_VAL then
|
|
success := false;
|
|
else --have a valid preference value
|
|
newPref := tmpVal;
|
|
--next token must be a domain name
|
|
if (endIdx >= zLength) then -- use of ">=" helps the prover
|
|
success := false;
|
|
else
|
|
begIdx := endIdx+1;
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
lengthOfToken := (endIdx-begIdx)+1;
|
|
if foundType /= rr_type.DomainNameorTimeSpec then
|
|
success := false;
|
|
elsif (lengthOfToken > rr_type.MaxDomainNameLength) then
|
|
success := false;
|
|
Error_Msgs.PrintDomainLengthErrorInfo(ZoneFileLine, BegIdx, EndIdx);
|
|
else
|
|
--have a domain name, but must still pad it
|
|
for I in Integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
--# and endIdx = endIdx%;
|
|
NewDomainName((I+1)-begIdx) := ZoneFileLine(I);
|
|
end loop;
|
|
for I in Integer range endIdx+1..rr_type.maxDomainNameLength loop
|
|
-- Remind prover that endIdx is in type
|
|
--# assert endIdx >= 1;
|
|
newDomainName(I) := ' ';
|
|
end loop;
|
|
end if; --valid domain name?
|
|
end if; --end of string reached after preference value?
|
|
end if; --too large pref?
|
|
end if; --number found?
|
|
end if; --end of string reached after record indicator?
|
|
end parsePrefAndDomainName;
|
|
|
|
+++ Flow analysis of subprogram
|
|
parsePrefAndDomainName performed: no errors found.
|
|
|
|
|
|
procedure parseIpv4(newIpv4 : out unsigned_types.Unsigned32;
|
|
zoneFileLine : in rr_type.LineFromFileType;
|
|
zLength : in rr_type.LineLengthIndex; success : in out boolean)
|
|
is
|
|
begIdx : rr_type.LineLengthIndex := 1;
|
|
endIdx : rr_type.LineLengthIndex;
|
|
foundType : rr_type.rrItemType;
|
|
TmpVal : unsigned_types.unsigned32;
|
|
|
|
BEGIN
|
|
newIpv4 := 0;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
--loop until you find an ipV4
|
|
WHILE FoundType /= rr_type.Ipv4 and endIdx < zlength LOOP
|
|
--# assert endIdx < zlength;
|
|
begIdx := ((begIdx-begidx)+endIdx)+1;
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
END LOOP;
|
|
|
|
if FoundType /= rr_type.Ipv4 and EndIdx >= ZLength then -- ">=" helps the prover
|
|
success := false;
|
|
else
|
|
TmpVal := parser_utilities.ConvertIpv4(ZoneFileLine, begIdx, endIdx);
|
|
if TmpVal = 0 then
|
|
Success := False;
|
|
else
|
|
newIpv4 := tmpVal;
|
|
end if;
|
|
end if;
|
|
end parseIpv4;
|
|
|
|
+++ Flow analysis of subprogram parseIpv4 performed:
|
|
no errors found.
|
|
|
|
|
|
procedure parseIpv6(newIpv6 : out rr_type.aaaa_record_type.IPV6AddrType;
|
|
zoneFileLine : in rr_type.LineFromFileType;
|
|
zLength : in rr_type.LineLengthIndex; success : in out boolean)
|
|
is
|
|
begIdx : rr_type.LineLengthIndex := 1;
|
|
endIdx : rr_type.LineLengthIndex;
|
|
foundType : rr_type.rrItemType;
|
|
|
|
BEGIN
|
|
newIpv6 := rr_type.aaaa_record_type.INVALID_IPV6_ADDR;
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
|
|
--loop until you find an ipV6
|
|
WHILE FoundType /= rr_type.Ipv6 and endIdx < zlength LOOP
|
|
--# assert endIdx < zlength;
|
|
begIdx := ((begIdx-begidx)+endIdx)+1;
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
END LOOP;
|
|
|
|
if FoundType /= rr_type.Ipv6 and EndIdx >= ZLength then -- ">=" helps the prover
|
|
success := false;
|
|
else
|
|
newIpv6 := parser_utilities.ConvertIpv6(ZoneFileLine, begIdx, endIdx);
|
|
if newIpv6 = rr_type.aaaa_record_type.INVALID_IPV6_ADDR then
|
|
success := false;
|
|
end if;
|
|
end if;
|
|
end ParseIpv6;
|
|
|
|
+++ Flow analysis of subprogram parseIpv6 performed:
|
|
no errors found.
|
|
|
|
|
|
--precondition is that zoneFileLine contains a record indicator, but can't
|
|
--express that in SPARK
|
|
--Basically like parseDomainName done twice
|
|
procedure ParseNameServerAndEmail(newNameServer : out Rr_Type.DomainNameStringType;
|
|
newEmail : out rr_type.DomainNameStringType;
|
|
zoneFileLine : in rr_type.LineFromFileType;
|
|
zLength : in rr_type.LineLengthIndex; success : in out boolean)
|
|
is
|
|
begIdx : rr_type.LineLengthIndex := 1;
|
|
endIdx : rr_type.LineLengthIndex;
|
|
foundType : rr_type.rrItemType;
|
|
lengthOfToken : rr_type.LineLengthIndex;
|
|
|
|
BEGIN
|
|
NewNameServer := Rr_Type.BlankDomainName;
|
|
newEmail := rr_type.blankDomainName;
|
|
--find the record type indicator, which must be present since this routine was called
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
|
|
--second condition always true if precondition of routine is met, but it helps the prover
|
|
WHILE FoundType/= rr_type.RecordIndicator and endIdx < zlength LOOP
|
|
--# assert endIdx < zlength;
|
|
begIdx := ((begIdx-begIdx)+endIdx)+1; --makes flow error go away
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, foundType);
|
|
END LOOP;
|
|
|
|
--check to make sure something is after the record type, find its position if so
|
|
if (EndIdx >= ZLength) then
|
|
success := false;
|
|
else
|
|
begIdx := endIdx+1;
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
lengthOfToken := (endIdx-begIdx)+1;
|
|
if foundType /= rr_type.DomainNameOrTimeSpec then
|
|
Success := False;
|
|
elsif (LengthOfToken > Rr_Type.MaxDomainNameLength) then
|
|
success := false;
|
|
Error_Msgs.PrintDomainLengthErrorInfo(ZoneFileLine, BegIdx, EndIdx);
|
|
else
|
|
--have a domain name, but must still pad it
|
|
for I in Integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
--# and endIdx = endIdx%;
|
|
newNameServer((I+1)-begIdx) := ZoneFileLine(I);
|
|
end loop;
|
|
for I in Integer range endIdx+1..rr_type.maxDomainNameLength loop
|
|
-- Remind prover that endIdx is in type
|
|
--# assert endIdx >= 1;
|
|
newNameServer(I) := ' ';
|
|
end loop;
|
|
end if;
|
|
|
|
end if;
|
|
|
|
--do it all again to get the email
|
|
--check to make sure something is after the name server, find its position if so
|
|
if (EndIdx >= ZLength) then
|
|
success := false;
|
|
else
|
|
begIdx := endIdx+1;
|
|
parser_utilities.findNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, FoundType);
|
|
lengthOfToken := (endIdx-begIdx)+1;
|
|
if FoundType /= Rr_Type.DomainNameOrTimeSpec then
|
|
success := false;
|
|
elsif (lengthOfToken > rr_type.MaxDomainNameLength) then
|
|
success := false;
|
|
Error_Msgs.PrintDomainLengthErrorInfo(ZoneFileLine, BegIdx, EndIdx);
|
|
else
|
|
--have a domain name, but must still pad it
|
|
for I in Integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
--# and endIdx = endIdx%;
|
|
newEmail((I+1)-begIdx) := ZoneFileLine(I);
|
|
end loop;
|
|
for I in Integer range endIdx+1..rr_type.maxDomainNameLength loop
|
|
-- Remind prover that endIdx is in type
|
|
--# assert endIdx >= 1;
|
|
newEmail(I) := ' ';
|
|
end loop;
|
|
end if;
|
|
end if;
|
|
END ParseNameServerAndEmail;
|
|
|
|
+++ Flow analysis of subprogram
|
|
ParseNameServerAndEmail performed: no errors found.
|
|
|
|
|
|
--domain name, TTL and class on a line are all optional, if blank default to last known values
|
|
--succeeds if a record type is found
|
|
procedure ParseOwnerTTLClassAndRecordType(
|
|
newOwner : in out rr_type.DomainNameStringType;
|
|
newTTL : in out unsigned_types.Unsigned32;
|
|
newClass : in out rr_type.classType;
|
|
newType : in out dns_types.Query_Type;
|
|
zoneFileLine : in rr_type.LineFromFileType;
|
|
zLength : in rr_type.LineLengthIndex; success : in out boolean) is
|
|
begIdx : rr_type.LineLengthIndex := 1;
|
|
endIdx : rr_type.LineLengthIndex;
|
|
Token : Rr_Type.LineFromFileType := Rr_Type.LineFromFileType'(others => ' ');
|
|
lengthOfToken : rr_type.LineLengthIndex;
|
|
TokenType : Rr_Type.RrItemType;
|
|
recordTypeFound : boolean := false;
|
|
firstChar : Character;
|
|
LastChar : Character;
|
|
|
|
begin
|
|
--if 1st char isn't blank, then first token is a domainName regardless of
|
|
--returned value of TokenType
|
|
if (zoneFileLine(1) /= ' ') and (zoneFileLine(1) /= Ada.Characters.Latin_1.HT) then
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, TokenType);
|
|
lengthOfToken := ((endIdx-begIdx)+1);
|
|
for i in integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and begIdx <= endIdx;
|
|
token((i+1)-begIdx) := zoneFileLine(i);
|
|
end loop;
|
|
if (lengthOfToken >= rr_type.MaxDomainNameLength) then
|
|
success := false;
|
|
error_msgs.printDomainLengthErrorInfo(zoneFileLine, begIdx, endIdx);
|
|
else
|
|
newOwner := rr_type.BlankDomainName; --in case previous owner longer than new one
|
|
for I in Integer range 1..LengthOfToken loop
|
|
--# assert lengthOfToken = lengthOfToken%
|
|
--# and lengthOfToken < rr_type.MaxDomainNameLength;
|
|
newOwner(I) := token(I);
|
|
end loop;
|
|
end if;
|
|
--line must contain a record type or the parse fails
|
|
--use of ">=" helps the prover
|
|
if (endIdx >= zlength or tokenType = rr_type.Comment) then
|
|
Success := False;
|
|
else
|
|
begIdx := endIdx+1;
|
|
end if;
|
|
end if;
|
|
|
|
--now keep going until you find a record type, which will be present in
|
|
--every valid record in the file
|
|
WHILE (NOT RecordTypeFound) AND Success LOOP
|
|
Parser_Utilities.FindNextToken(ZoneFileLine, ZLength, BegIdx, EndIdx, TokenType);
|
|
--postcondition from findNextToken()
|
|
--# assert begIdx <= endIdx;
|
|
for i in integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and begIdx <= endIdx;
|
|
token((i+1)-begIdx) := zoneFileLine(i);
|
|
end loop;
|
|
case TokenType is
|
|
when Rr_Type.Number | Rr_Type.DomainNameOrTimeSpec =>
|
|
Parser_Utilities.ConvertTimeSpec(ZoneFileLine, BegIdx, EndIdx, NewTTL, Success);
|
|
when Rr_Type.Class =>
|
|
firstChar := Ada.Characters.Handling.To_Upper(token(begIdx));
|
|
lastChar := Ada.Characters.Handling.To_Upper(token(endIdx));
|
|
if firstChar = 'C' and lastChar = 'H' then
|
|
newClass := rr_type.CH;
|
|
elsif firstChar = 'C' and lastChar = 'S' then
|
|
newClass := rr_type.CS;
|
|
elsif firstChar = 'H' and lastChar = 'S' then
|
|
newClass := rr_type.HS;
|
|
elsif firstChar = 'I' and lastChar = 'N' then
|
|
newClass := rr_type.INTERNET;
|
|
END IF;
|
|
WHEN Rr_Type.RecordIndicator =>
|
|
RecordTypeFound := True; --this means we have found a valid record type indicator
|
|
NewType := Parser_Utilities.GetRecordType(ZoneFileLine, BegIdx, EndIdx);
|
|
when others =>
|
|
Success := False;
|
|
end case;
|
|
|
|
--line must contain a record type or the parse fails
|
|
--use of ">=" helps the prover
|
|
if (endIdx >= zlength or tokenType = rr_type.Comment) then
|
|
if not recordTypeFound then
|
|
Success := False;
|
|
end if;
|
|
else
|
|
begIdx := endIdx+1;
|
|
end if;
|
|
END LOOP; --while record type token not found and line still has tokens
|
|
|
|
end parseOwnerTTLCLassAndRecordType;
|
|
|
|
+++ Flow analysis of subprogram
|
|
parseOwnerTTLClassAndRecordType performed: no errors found.
|
|
|
|
end zone_file_parser;
|
|
|
|
|
|
--End of file--------------------------------------------------
|