1073 lines
49 KiB
Plaintext
1073 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 non_spark_stuff, error_msgs, Ada.Characters.Handling, Ada.Characters.Latin_1, Rr_Type.A_Record_Type,
|
|
rr_type.soa_record_type;
|
|
use type Rr_Type.RrItemType;
|
|
|
|
PACKAGE BODY Parser_Utilities IS
|
|
|
|
BLANK : constant Character := ' ';
|
|
TAB : constant Character := Ada.Characters.Latin_1.HT;
|
|
COMMENT_CHAR : constant Character := ';';
|
|
CONTROL_CHAR : constant Character := '$';
|
|
ORIGIN_CHAR : constant Character := '@'; --also definied in rr_type.adb
|
|
L_PAREN: constant Character := '(';
|
|
R_PAREN: constant Character := ')';
|
|
|
|
SecondsInAMinute: constant natural := 60;
|
|
MinutesInAnHour: constant natural := 60;
|
|
HoursInADay: constant natural := 24;
|
|
DaysInAWeek: constant Natural := 7;
|
|
MaxDaysInAMonth : constant Natural := 31;
|
|
MonthsInAYear: constant natural := 12;
|
|
|
|
--CH, CS, HS and IN are only valid namespace classes
|
|
function isClass(s : in rr_type.LineFromFileType; begIdx : in rr_type.LineLengthIndex;
|
|
endIdx : in rr_type.LineLengthIndex) return boolean is
|
|
Retval : Boolean;
|
|
subtype two_range is integer range 1..2;
|
|
subtype string2 is string(two_range);
|
|
Class : String2 := " ";
|
|
begin
|
|
--helps prover
|
|
if begIdx = endIdx-1 then
|
|
Class(1) := Ada.Characters.Handling.To_Upper(S(BegIdx));
|
|
Class(2) := Ada.Characters.Handling.To_Upper(S(endIdx));
|
|
Retval := (Class="CH") or else (Class="CS") or else (Class="HS")
|
|
or else (Class="IN");
|
|
else
|
|
retval := false;
|
|
end if;
|
|
return retval;
|
|
end IsClass;
|
|
|
|
+++ Flow analysis of subprogram isClass performed:
|
|
no errors found.
|
|
|
|
|
|
--For now, only {A,AAAA,CNAME,DNSKEY,MX,NS,PTR,SOA} records recognized
|
|
--{RP,SRV,TXT recognized but not implemented}
|
|
function isRecord(s : in rr_type.LineFromFileType; begIdx : in rr_type.LineLengthIndex;
|
|
endIdx : in rr_type.LineLengthIndex) return boolean
|
|
--# pre begIdx <= endIdx;
|
|
is
|
|
firstChar : character;
|
|
lastChar : character;
|
|
lengthToken : rr_type.LineLengthIndex;
|
|
retval : boolean;
|
|
begin
|
|
firstChar:= Ada.Characters.Handling.To_Upper(S(BegIdx));
|
|
lastChar := Ada.Characters.Handling.To_Upper(S(EndIdx));
|
|
lengthToken := (endIdx-begIdx)+1;
|
|
--ugly but it gets the job done
|
|
--A
|
|
IF firstChar = 'A' AND LengthToken = 1 THEN
|
|
Retval := True;
|
|
--NS
|
|
elsif firstChar = 'N' and lastChar = 'S' and lengthToken = 2 then
|
|
Retval := True;
|
|
--MX
|
|
elsif firstChar = 'M' and lastChar = 'X' and lengthToken = 2 then
|
|
Retval := True;
|
|
--RP
|
|
elsif firstChar = 'R' and lastChar = 'P' and lengthToken = 2 then
|
|
Retval := True;
|
|
--PTR
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'P' and lastChar = 'R' and begIdx <= endIdx-2 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'T' then
|
|
Retval := true;
|
|
else
|
|
RetVal := false;
|
|
end if;
|
|
--SOA
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'S' and lastChar = 'A' and begIdx <= endIdx-2 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'O' then
|
|
Retval := true;
|
|
else
|
|
RetVal := false;
|
|
end if;
|
|
--SRV
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'S' and lastChar = 'V' and begIdx <= endIdx-2 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'R' then
|
|
Retval := true;
|
|
else
|
|
RetVal := false;
|
|
end if;
|
|
--TXT
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'T' and lastChar = 'T' and begIdx <= endIdx-2 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'X' then
|
|
Retval := true;
|
|
else
|
|
RetVal := false;
|
|
end if;
|
|
--AAAA
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'A' and lastChar = 'A' and begIdx <= endIdx-3 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'A' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+2)) = 'A' then
|
|
Retval := true;
|
|
else
|
|
RetVal := false;
|
|
end if;
|
|
|
|
--NSEC
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'N' and lastChar = 'C' and begIdx <= endIdx-3 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'S' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+2)) = 'E' then
|
|
Retval := true;
|
|
else
|
|
RetVal := false;
|
|
end if;
|
|
|
|
--CNAME
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'C' and lastChar = 'E' and begIdx <= endIdx-4 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'N' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+2)) = 'A' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+3)) = 'M' then
|
|
Retval := true;
|
|
else
|
|
RetVal := false;
|
|
end if;
|
|
|
|
--RRSIG
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'R' and lastChar = 'G' and begIdx <= endIdx-4 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'R' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+2)) = 'S' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+3)) = 'I' then
|
|
Retval := true;
|
|
else
|
|
RetVal := false;
|
|
end if;
|
|
|
|
--DNSKEY
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'D' and lastChar = 'Y' and begIdx <= endIdx-5 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'N' and
|
|
Ada.Characters.Handling.To_Upper(S(BegIdx+2)) = 'S' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+3)) = 'K' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+4)) = 'E' then
|
|
Retval := true;
|
|
else
|
|
RetVal := false;
|
|
end if;
|
|
ELSE
|
|
retVal := false;
|
|
end if;
|
|
return retval;
|
|
END IsRecord;
|
|
|
|
+++ Flow analysis of subprogram isRecord performed:
|
|
no errors found.
|
|
|
|
|
|
--Called only when s(begIdx..endIdx) is valid record type indicator
|
|
--For now, only {A,AAAA,CNAME,DNSKEY,MX,NS,NSEC,PTR,SOA} records supported
|
|
--{RP,SRV,TXT recognized but not implemented}
|
|
function getRecordType(s : in rr_type.LineFromFileType; begIdx : in rr_type.LineLengthIndex;
|
|
endIdx : in rr_type.LineLengthIndex) return dns_types.Query_Type
|
|
is
|
|
firstChar : character;
|
|
lastChar : character;
|
|
lengthToken : rr_type.LineLengthIndex;
|
|
retval : dns_types.Query_Type;
|
|
begin
|
|
firstChar := Ada.Characters.Handling.to_upper(s(begIdx));
|
|
lastChar := Ada.Characters.Handling.to_upper(s(endIdx));
|
|
lengthToken := (endIdx-begIdx)+1;
|
|
--ugly but it gets the job done
|
|
--A
|
|
if firstChar = 'A' and lengthToken = 1 then
|
|
Retval := Dns_Types.A;
|
|
--NS
|
|
elsif firstChar = 'N' and lastChar = 'S' and lengthToken = 2 then
|
|
Retval := Dns_Types.NS;
|
|
--MX
|
|
elsif firstChar = 'M' and lastChar = 'X' and lengthToken = 2 then
|
|
Retval := Dns_Types.MX;
|
|
--RP
|
|
elsif firstChar = 'R' and lastChar = 'P' and lengthToken = 2 then
|
|
Retval := DNS_Types.UNIMPLEMENTED;
|
|
--PTR
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'P' and lastChar = 'R' and begIdx <= endIdx-2 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'T' then
|
|
Retval := Dns_Types.PTR;
|
|
else
|
|
RetVal := dns_types.ERROR;
|
|
end if;
|
|
--SOA
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'S' and lastChar = 'A' and begIdx <= endIdx-2 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'O' then
|
|
Retval := dns_types.SOA;
|
|
else
|
|
RetVal := dns_types.ERROR;
|
|
end if;
|
|
--SRV
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'S' and lastChar = 'V' and begIdx <= endIdx-2 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'R' then
|
|
Retval := dns_types.UNIMPLEMENTED;
|
|
else
|
|
RetVal := dns_types.ERROR;
|
|
end if;
|
|
--TXT
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'T' and lastChar = 'T' and begIdx <= endIdx-2 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'X' then
|
|
Retval := dns_types.UNIMPLEMENTED;
|
|
else
|
|
RetVal := dns_types.ERROR;
|
|
end if;
|
|
--AAAA
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'A' and lastChar = 'A' and begIdx <= endIdx-3 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'A' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+2)) = 'A' then
|
|
Retval := Dns_Types.AAAA;
|
|
else
|
|
RetVal := Dns_Types.ERROR;
|
|
end if;
|
|
--NSEC
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'N' and lastChar = 'C' and begIdx <= endIdx-3 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'S' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+2)) = 'E' then
|
|
Retval := Dns_Types.NSEC;
|
|
else
|
|
RetVal := Dns_Types.ERROR;
|
|
end if;
|
|
--CNAME
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'C' and lastChar = 'E' and begIdx <= endIdx-4 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'N' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+2)) = 'A' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+3)) = 'M' then
|
|
Retval := Dns_Types.CNAME;
|
|
else
|
|
RetVal := Dns_Types.ERROR;
|
|
end if;
|
|
--RRSIG
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'R' and lastChar = 'G' and begIdx <= endIdx-4 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'R' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+2)) = 'S' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+3)) = 'I' then
|
|
Retval := Dns_Types.RRSIG;
|
|
else
|
|
RetVal := Dns_Types.ERROR;
|
|
end if;
|
|
--DNSKEY
|
|
--formulation of third condition helps prover
|
|
elsif firstChar = 'D' and lastChar = 'Y' and begIdx <= endIdx-5 then
|
|
if Ada.Characters.Handling.to_upper(s(begIdx+1)) = 'N' and
|
|
Ada.Characters.Handling.To_Upper(S(BegIdx+2)) = 'S' and
|
|
Ada.Characters.Handling.to_upper(s(begIdx+3)) = 'K' and
|
|
Ada.Characters.Handling.To_Upper(S(BegIdx+4)) = 'E' then
|
|
RetVal := Dns_Types.DNSKEY;
|
|
else
|
|
RetVal := Dns_Types.ERROR;
|
|
end if;
|
|
ELSE
|
|
RetVal := Dns_Types.UNIMPLEMENTED;
|
|
end if;
|
|
return retval;
|
|
end GetRecordType;
|
|
|
|
+++ Flow analysis of subprogram getRecordType
|
|
performed: no errors found.
|
|
|
|
|
|
procedure CheckAndAppendOrigin(target : in out Rr_Type.DomainNameStringType;
|
|
Origin : in Rr_Type.DomainNameStringType;
|
|
CurrentLine : in rr_type.LineFromFileType;
|
|
LastPos : in Rr_Type.Linelengthindex;
|
|
LineCount : in unsigned_types.unsigned32;
|
|
Success : in out boolean
|
|
)
|
|
is
|
|
begin
|
|
--if target does not end in '.', append Origin string
|
|
if target(Rr_Type.DomainNameLength(target)) /= '.'then
|
|
if origin = Rr_Type.BlankDomainName then
|
|
error_msgs.printBlankOriginWarning(currentLine, lastPos, lineCount);
|
|
else
|
|
Rr_Type.appendDomainNames(target, origin, Success);
|
|
if not Success then
|
|
error_msgs.printAppendDomainLengthErrorInfo(currentLine, lastPos, lineCount);
|
|
end if;
|
|
end if;
|
|
end if; --check for domain name ending in '.'
|
|
end CheckAndAppendOrigin;
|
|
|
|
+++ Flow analysis of subprogram CheckAndAppendOrigin
|
|
performed: no errors found.
|
|
|
|
|
|
procedure checkValidHostName(Name: Rr_Type.DomainNameStringType; success: in out boolean)
|
|
is
|
|
Length: Rr_Type.DomainNameStringTypeIndex;
|
|
retVal : boolean := true;
|
|
begin
|
|
--only characters allowed are alphanumerics, '.' and '-'
|
|
|
|
Length := Rr_Type.DomainNameLength(Name);
|
|
|
|
--has to start and end with alphanumeric
|
|
--use length-1 because name(length) is always a period, doesn't count
|
|
--SPARK caught runtime error for length=1, nice!
|
|
if Name(1) = '.' or Name(1) = '-' or (length > 1 and then (Name(Length-1) = '.' or Name(Length-1) = '-')) then
|
|
RetVal := False;
|
|
else
|
|
for I in Integer range 2..Length-2 loop
|
|
--# assert true;
|
|
--periods must come after alphanumeric
|
|
if Name(I) = '.' then
|
|
if (Name(I-1) = '.' or Name(I-1) = '-') then
|
|
RetVal := False;
|
|
end if;
|
|
--if not period, must be alphanumeric or underscore
|
|
elsif not Ada.Characters.Handling.Is_Alphanumeric(Name(I)) and Name(I) /= '-' then
|
|
RetVal := False;
|
|
end if;
|
|
end loop;
|
|
end if;
|
|
success := success and retVal;
|
|
end CheckValidHostName;
|
|
|
|
+++ Flow analysis of subprogram checkValidHostName
|
|
performed: no errors found.
|
|
|
|
|
|
--Just like findNextToken below , but starts at beginning of line, no index values
|
|
--returned. Only used to see what the first token on the line is.
|
|
procedure findFirstToken(s : in rr_type.LineFromFileType; length : in rr_type.LineLengthIndex;
|
|
T : out rr_type.rrItemType)
|
|
is
|
|
|
|
begIdx : rr_type.LineLengthIndex := 1;
|
|
endIdx : rr_type.LineLengthIndex;
|
|
ContainsOnlyNumbers : boolean;
|
|
containsOnlyLetters : boolean;
|
|
ContainsPeriod : Boolean;
|
|
containsColon : boolean;
|
|
ContainsDecimalNumbers : Boolean;
|
|
ContainsHexNumbers : Boolean;
|
|
ContainsLetters : Boolean;
|
|
--NOTE: Can domain names have anything other than letters, numbers or periods?
|
|
BEGIN
|
|
while begIdx < length and then (s(begIdx) = BLANK or s(begIdx) = TAB) loop
|
|
--# assert begIdx >= 1 and begIdx < length;
|
|
begIdx := begIdx + 1;
|
|
end loop;
|
|
|
|
endIdx := begIdx;
|
|
while endIdx < length and then (s(endIdx) /= BLANK and s(endIdx) /= TAB
|
|
and s(endIdx) /= COMMENT_CHAR and s(endIdx) /= L_PAREN and s(endIdx) /= R_PAREN) loop
|
|
--# assert begIdx >= 1 and begIdx <= length and
|
|
--# endIdx >= begIdx and endIdx < length;
|
|
endIdx := endIdx + 1;
|
|
END LOOP;
|
|
if (s(endIdx) = BLANK or s(endIdx) = TAB or s(endIdx) = COMMENT_CHAR) and endIdx > 1 and endIdx > begIdx then
|
|
EndIdx := EndIdx-1;
|
|
end if;
|
|
ContainsOnlyNumbers := true;
|
|
ContainsOnlyLetters := True;
|
|
|
|
ContainsPeriod := False;
|
|
containsColon := false;
|
|
ContainsDecimalNumbers := False;
|
|
ContainsHexNumbers := false;
|
|
ContainsLetters := False;
|
|
|
|
FOR I IN Integer RANGE BegIdx..EndIdx LOOP
|
|
--# assert begIdx >= 1 and begIdx <= length and
|
|
--# endIdx >= begIdx and endIdx <= length;
|
|
ContainsOnlyNumbers := ContainsOnlyNumbers AND Ada.Characters.Handling.Is_Digit(S(I));
|
|
ContainsDecimalNumbers := ContainsDecimalNumbers or Ada.Characters.Handling.Is_Digit(S(I));
|
|
containsHexNumbers := containsHexNumbers or Ada.Characters.Handling.Is_Hexadecimal_Digit(S(I));
|
|
ContainsOnlyLetters := ContainsOnlyLetters AND Ada.Characters.Handling.Is_Letter(S(I));
|
|
containsLetters := containsLetters or Ada.Characters.Handling.Is_Letter(S(I));
|
|
ContainsPeriod := ContainsPeriod or S(I) = '.';
|
|
ContainsColon := ContainsColon or S(I) = ':';
|
|
end loop;
|
|
|
|
--figure out what we've got
|
|
IF S(BegIdx) = COMMENT_CHAR then
|
|
T := Rr_Type.Comment;
|
|
elsIF S(BegIdx) = CONTROL_CHAR then
|
|
T := Rr_Type.Control;
|
|
elsIF S(BegIdx) = L_PAREN THEN
|
|
T := Rr_Type.LParen;
|
|
elsIF S(BegIdx) = R_PAREN THEN
|
|
T := Rr_Type.RParen;
|
|
--@ counts as a domain name, will be replaced with $ORIGIN
|
|
--. counts as domain name, could appear as value of $ORIGIN
|
|
elsIf (S(BegIdx) = ORIGIN_CHAR or S(BegIdx) = '.') and BegIdx = EndIdx then
|
|
T := Rr_Type.DomainNameOrTimeSpec;
|
|
elsif containsDecimalNumbers and containsOnlyNumbers then
|
|
T := Rr_Type.Number;
|
|
elsif containsDecimalNumbers and containsPeriod and not containsLetters and not containsColon then
|
|
T := Rr_Type.Ipv4;
|
|
elsif containsHexNumbers and containsColon and not containsPeriod then
|
|
T := Rr_Type.Ipv6;
|
|
elsif containsOnlyLetters and isClass(s,begIdx,endIdx) then
|
|
T := rr_Type.Class;
|
|
elsif containsOnlyLetters and isRecord(s,begIdx,endIdx) then
|
|
T := rr_Type.RecordIndicator;
|
|
elsif containsLetters then
|
|
T := Rr_Type.DomainNameOrTimeSpec;
|
|
elsif BegIdx = Length then --this means blank line, treated as a comment
|
|
T := rr_type.Comment;
|
|
else --error of some sort, e.g. invalid class or record type
|
|
T := Rr_Type.Other;
|
|
end if;
|
|
--Ada.Text_Io.Put("TOKEN = " & Rr_Type.RrItemType'Image(T));
|
|
--ada.text_io.new_line;
|
|
|
|
end findFirstToken;
|
|
|
|
+++ Flow analysis of subprogram findFirstToken
|
|
performed: no errors found.
|
|
|
|
|
|
|
|
procedure findNextToken(s : in rr_type.LineFromFileType; length : in rr_type.LineLengthIndex;
|
|
begIdx : in out rr_type.LineLengthIndex;
|
|
endIdx : out rr_type.LineLengthIndex;
|
|
T : out rr_type.rrItemType)
|
|
is
|
|
ContainsOnlyNumbers : boolean;
|
|
containsOnlyLetters : boolean;
|
|
ContainsPeriod : Boolean;
|
|
containsColon : boolean;
|
|
ContainsDecimalNumbers : Boolean;
|
|
ContainsHexNumbers : Boolean;
|
|
ContainsLetters : Boolean;
|
|
--NOTE: Can domain names have anything other than letters, numbers or periods?
|
|
BEGIN
|
|
while begIdx < length and then (s(begIdx) = BLANK or s(begIdx) = TAB) loop
|
|
--# assert begIdx < length;
|
|
begIdx := begIdx + 1;
|
|
end loop;
|
|
endIdx := begIdx;
|
|
while endIdx < length and then (s(endIdx) /= BLANK and s(endIdx) /= TAB
|
|
and S(EndIdx) /= COMMENT_CHAR and S(EndIdx) /= L_PAREN and S(EndIdx) /= R_PAREN
|
|
and s(endIdx) /= ORIGIN_CHAR) loop
|
|
--# assert begIdx <= length and
|
|
--# endIdx >= begIdx and endIdx < length;
|
|
endIdx := endIdx + 1;
|
|
END LOOP;
|
|
if (S(EndIdx) = BLANK or S(EndIdx) = TAB or S(EndIdx) = COMMENT_CHAR)
|
|
and endIdx > 1 and endIdx > begIdx then
|
|
EndIdx := EndIdx-1;
|
|
end if;
|
|
|
|
ContainsOnlyNumbers := true;
|
|
ContainsOnlyLetters := True;
|
|
|
|
ContainsPeriod := False;
|
|
containsColon := false;
|
|
ContainsDecimalNumbers := False;
|
|
ContainsHexNumbers := false;
|
|
ContainsLetters := False;
|
|
|
|
FOR I IN Integer RANGE BegIdx..EndIdx LOOP
|
|
ContainsOnlyNumbers := ContainsOnlyNumbers AND S(I) >= '0' AND S(I) <= '9';
|
|
--# assert begIdx >= 1 and begIdx <= length and endIdx >= begIdx and endIdx <= length
|
|
--# and EndIdx = EndIdx%
|
|
--# and ((ContainsOnlyNumbers = true) ->
|
|
--# (for all J in integer range BegIdx..I => (S(J) >= '0' AND S(J) <= '9')));
|
|
ContainsDecimalNumbers := ContainsDecimalNumbers or (S(I) >= '0' AND S(I) <= '9');
|
|
containsHexNumbers := containsHexNumbers or Ada.Characters.Handling.Is_Hexadecimal_Digit(S(I));
|
|
ContainsOnlyLetters := ContainsOnlyLetters AND Ada.Characters.Handling.Is_Letter(S(I));
|
|
containsLetters := containsLetters or Ada.Characters.Handling.Is_Letter(S(I));
|
|
ContainsPeriod := ContainsPeriod or S(I) = '.';
|
|
ContainsColon := ContainsColon or S(I) = ':';
|
|
end loop;
|
|
|
|
--figure out what we've got
|
|
IF S(BegIdx) = COMMENT_CHAR then
|
|
T := Rr_Type.Comment;
|
|
elsIF S(BegIdx) = CONTROL_CHAR then
|
|
T := Rr_Type.Control;
|
|
elsIF S(BegIdx) = L_PAREN THEN
|
|
T := Rr_Type.LParen;
|
|
elsIF S(BegIdx) = R_PAREN THEN
|
|
T := Rr_Type.RParen;
|
|
--@ counts as a domain name, will be replaced with $ORIGIN
|
|
--. counts as domain name, could appear as value of $ORIGIN
|
|
elsIf (S(BegIdx) = ORIGIN_CHAR or S(BegIdx) = '.') and BegIdx = EndIdx then
|
|
T := Rr_Type.DomainNameOrTimeSpec;
|
|
elsif ContainsOnlyNumbers then
|
|
T := Rr_Type.Number;
|
|
elsif containsDecimalNumbers and containsPeriod and not containsLetters and not containsColon then
|
|
T := Rr_Type.Ipv4;
|
|
elsif containsHexNumbers and containsColon and not containsPeriod then
|
|
T := Rr_Type.Ipv6;
|
|
elsif containsOnlyLetters and isClass(s,begIdx,endIdx) then
|
|
T := rr_Type.Class;
|
|
elsif containsOnlyLetters and isRecord(s,begIdx,endIdx) then
|
|
T := rr_Type.RecordIndicator;
|
|
elsif containsLetters then
|
|
T := Rr_Type.DomainNameOrTimeSpec;
|
|
elsif BegIdx = Length then --this means blank line, treated as a comment
|
|
T := rr_type.Comment;
|
|
else --error of some sort, e.g. invalid class or record type
|
|
T := Rr_Type.Other;
|
|
end if;
|
|
END FindNextToken;
|
|
|
|
+++ Flow analysis of subprogram findNextToken
|
|
performed: no errors found.
|
|
|
|
|
|
--true if Char is s,m,h,d,w or uppercase equivalent
|
|
function IsMult(Char: in Character) return Boolean
|
|
is
|
|
C : Character;
|
|
retVal : boolean;
|
|
begin
|
|
C := Ada.Characters.Handling.To_Upper(Char);
|
|
if C = 'S' or C = 'M' or C = 'H' or C = 'D' or C = 'W' then
|
|
RetVal := True;
|
|
else
|
|
RetVal := False;
|
|
end if;
|
|
return retVal;
|
|
end IsMult;
|
|
|
|
+++ Flow analysis of subprogram IsMult performed: no
|
|
errors found.
|
|
|
|
|
|
procedure convert8BitUnsigned(value: out Unsigned_Types.Unsigned8;
|
|
ZoneFileLine : in rr_type.LineFromFileType;
|
|
BegIdx : in rr_type.LineLengthIndex;
|
|
EndIdx : in rr_type.LineLengthIndex;
|
|
Success : in out boolean)
|
|
is
|
|
digitVal : natural;
|
|
tmpVal : natural;
|
|
begin
|
|
tmpVal := 0;
|
|
value := 0;
|
|
for i in integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and tmpVal <= unsigned_types.MAX_8BIT_VAL;
|
|
digitVal := Character'Pos(zoneFileLine(I)) - Character'Pos('0');
|
|
TmpVal := 10*TmpVal + DigitVal;
|
|
exit when tmpVal > unsigned_types.MAX_8BIT_VAL;
|
|
end loop;
|
|
--make sure it's not too big
|
|
if tmpVal > unsigned_types.MAX_8BIT_VAL then
|
|
success := false;
|
|
else --have a valid preference value
|
|
value := unsigned_types.Unsigned8(tmpVal);
|
|
end if;
|
|
end convert8BitUnsigned;
|
|
|
|
+++ Flow analysis of subprogram convert8BitUnsigned
|
|
performed: no errors found.
|
|
|
|
|
|
procedure convert16BitUnsigned(value: out Unsigned_Types.Unsigned16;
|
|
ZoneFileLine : in rr_type.LineFromFileType;
|
|
BegIdx : in rr_type.LineLengthIndex;
|
|
EndIdx : in rr_type.LineLengthIndex;
|
|
Success : in out boolean)
|
|
is
|
|
digitVal : natural;
|
|
tmpVal : natural;
|
|
begin
|
|
tmpVal := 0;
|
|
value := 0;
|
|
for i in integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and tmpVal <= unsigned_types.MAX_16BIT_VAL;
|
|
digitVal := Character'Pos(zoneFileLine(I)) - Character'Pos('0');
|
|
TmpVal := 10*TmpVal + digitVal;
|
|
exit when tmpVal > unsigned_types.MAX_16BIT_VAL;
|
|
end loop;
|
|
--make sure it's not too big
|
|
if tmpVal > unsigned_types.MAX_16BIT_VAL then
|
|
success := false;
|
|
else --have a valid 16-bit value
|
|
value := unsigned_types.Unsigned16(tmpVal);
|
|
end if;
|
|
end Convert16BitUnsigned;
|
|
|
|
+++ Flow analysis of subprogram convert16BitUnsigned
|
|
performed: no errors found.
|
|
|
|
|
|
procedure convert32BitUnsigned(value: out Unsigned_Types.Unsigned32;
|
|
ZoneFileLine : in rr_type.LineFromFileType;
|
|
BegIdx : in rr_type.LineLengthIndex;
|
|
EndIdx : in rr_type.LineLengthIndex;
|
|
Success : in out boolean)
|
|
is
|
|
digitVal : long_long_integer;
|
|
tmpVal : long_long_integer;
|
|
begin
|
|
tmpVal := 0;
|
|
value := 0;
|
|
for i in integer range begIdx..endIdx loop
|
|
--# assert begIdx >= 1 and tmpVal >= 0 and tmpVal <= unsigned_types.MAX_32BIT_VAL;
|
|
digitVal := Character'Pos(zoneFileLine(I)) - Character'Pos('0');
|
|
TmpVal := 10*TmpVal + digitVal;
|
|
exit when tmpVal > unsigned_types.MAX_32BIT_VAL;
|
|
end loop;
|
|
--make sure it's not too big
|
|
if tmpVal > unsigned_types.MAX_32BIT_VAL then
|
|
success := false;
|
|
else --have a valid 32-bit value
|
|
value := unsigned_types.Unsigned32(tmpVal);
|
|
end if;
|
|
end convert32BitUnsigned;
|
|
|
|
+++ Flow analysis of subprogram convert32BitUnsigned
|
|
performed: no errors found.
|
|
|
|
|
|
--converts the time specifier at s(begIdx..endIdx) into a time value in seconds, returned in RetVal.
|
|
--a time specifier is either a Num or one or more Blobs. A Num is a string of decimal digits.
|
|
--A Blob is a Num followed by a Mult. A Mult is one of {s,m,h,w,d} and their upper-case equivalents.
|
|
--Sets Success to false if the time specifier is invalid
|
|
procedure ConvertTimeSpec(S : in Rr_Type.LineFromFileType; begIdx: in rr_type.LineLengthIndex;
|
|
EndIdx: in Rr_Type.LineLengthIndex; RetVal : out Unsigned_Types.Unsigned32; Success: in out Boolean)
|
|
is
|
|
Tmp : Long_Long_Integer := 0;
|
|
Blob : Long_Long_Integer := 0;
|
|
CurrentChar : Character;
|
|
|
|
function MultValue(Char : in Character) return natural
|
|
--# pre isMult(Char);
|
|
--# return Value => Value >= 0 and Value <= 60*60*24*7;
|
|
is
|
|
C : Character;
|
|
retVal : natural;
|
|
begin
|
|
C := Ada.Characters.Handling.To_Upper(Char);
|
|
case C is
|
|
when 'S' =>
|
|
RetVal := 1;
|
|
when 'M' =>
|
|
RetVal := SecondsInAMinute;
|
|
when 'H' =>
|
|
RetVal := SecondsInAMinute*MinutesInAnHour;
|
|
when 'D' =>
|
|
RetVal := (SecondsInAMinute*MinutesInAnHour)*HoursInADay;
|
|
when 'W' =>
|
|
RetVal := ((SecondsInAMinute*MinutesInAnHour)*HoursInADay)*DaysInAWeek;
|
|
when others =>
|
|
RetVal := 0; --will never happen if precondition is met
|
|
end case;
|
|
return RetVal;
|
|
end MultValue;
|
|
|
|
+++ Flow analysis of subprogram MultValue performed:
|
|
no errors found.
|
|
|
|
|
|
begin
|
|
for I in Integer range BegIdx..EndIdx loop
|
|
--#assert Blob >= 0 and Blob <= Rr_Type.SOA_Record_Type.MAX_TIME_VAL
|
|
--#and Tmp >= 0 and Tmp <= Rr_Type.SOA_Record_Type.MAX_TIME_VAL;
|
|
CurrentChar := s(I);
|
|
if CurrentChar >= '0' and CurrentChar <= '9' then
|
|
Blob := 10*Blob + (Character'Pos(CurrentChar)-Character'Pos('0'));
|
|
if Blob > Rr_Type.SOA_Record_Type.MAX_TIME_VAL then
|
|
Success := False;
|
|
end if;
|
|
elsif IsMult(CurrentChar) then
|
|
if (Blob = 0) then
|
|
Success := False;
|
|
else
|
|
Blob := Blob*long_long_integer(MultValue(CurrentChar));
|
|
Tmp := Tmp + Blob;
|
|
if Blob > Rr_Type.Soa_Record_Type.MAX_TIME_VAL or Tmp > Rr_Type.Soa_Record_Type.MAX_TIME_VAL then
|
|
Success := False;
|
|
end if;
|
|
Blob := 0;
|
|
end if;
|
|
else
|
|
Success := False;
|
|
end if;
|
|
exit when Success = False;
|
|
end loop;
|
|
if not Success then
|
|
Tmp := 0;
|
|
elsif Tmp = 0 then --handle case when time specifier is just a number (no mult)
|
|
Tmp := Blob;
|
|
end if;
|
|
retVal := unsigned_types.unsigned32(Tmp);
|
|
end ConvertTimeSpec;
|
|
|
|
+++ Flow analysis of subprogram ConvertTimeSpec
|
|
performed: no errors found.
|
|
|
|
|
|
procedure ConvertTimeString(TimeVal : out Unsigned_Types.Unsigned32;
|
|
TimeString: in Rr_Type.Rrsig_Record_Type.TimeStringType;
|
|
Success : in out boolean)
|
|
is
|
|
Year : Natural := 0;
|
|
Month : Natural:= 0;
|
|
Day : Natural := 0;
|
|
Hour: Natural := 0;
|
|
Minute : Natural := 0;
|
|
Second : Natural := 0;
|
|
Num : Natural;
|
|
begin
|
|
for I in Rr_Type.Rrsig_Record_Type.TimeStringTypeIndex loop
|
|
--help the prover show these values remain in type
|
|
--#assert year <= rr_type.rrsig_record_type.MAX_YEAR and month <= 12 and day <= 31
|
|
--# and hour <= 23 and minute <= 59 and second <= 59;
|
|
Num := Character'Pos(TimeString(I))- Character'Pos('0');
|
|
if (I <= 4) then
|
|
Year := 10*Year + Num;
|
|
elsif (I <= 6) then
|
|
Month := 10*Month + Num;
|
|
elsif (I <= 8) then
|
|
Day:= 10*Day + Num;
|
|
elsif (I <= 10) then
|
|
Hour := 10*Hour + Num;
|
|
elsif (I <= 12) then
|
|
Minute:= 10*Minute + Num;
|
|
elsif (I <= 14) then --flagged, but leave as is in case TimeStringTypeIndex ever changed
|
|
Second := 10*Second + Num;
|
|
end if;
|
|
exit when Year > Rr_Type.Rrsig_Record_Type.MAX_YEAR or Month > MonthsInAYear
|
|
or Day > MaxDaysInAMonth or Hour >= HoursInADay or Minute >= MinutesInAnHour
|
|
or Second >= SecondsInAMinute;
|
|
end loop;
|
|
if (Year > Rr_Type.Rrsig_Record_Type.MAX_YEAR or Month > MonthsInAYear
|
|
or Day > MaxDaysInAMonth or Hour >= HoursInADay or Minute >= MinutesInAnHour
|
|
or Second >= SecondsInAMinute) then
|
|
Success := False;
|
|
timeVal := 0;
|
|
else
|
|
timeVal := Non_Spark_Stuff.Time_Of(Year,Month,Day,Hour,Minute,Second);
|
|
end if;
|
|
end ConvertTimeString;
|
|
|
|
+++ Flow analysis of subprogram ConvertTimeString
|
|
performed: no errors found.
|
|
|
|
|
|
procedure AddToKeyR(RRSIG_Rec : in out rr_type.RRSIG_Record_type.rrsigrecordtype;
|
|
s: in Rr_Type.LineFromFileType;
|
|
Length : in Rr_Type.LineLengthIndex;
|
|
AllDone : out boolean; --this is needed because line might terminate with ')'
|
|
success : in out boolean)
|
|
is
|
|
BegIdx : Rr_Type.LineLengthIndex;
|
|
EndIdx : Rr_Type.LineLengthIndex;
|
|
returnedType : rr_type.rrItemType;
|
|
begin
|
|
--find start of key fragment
|
|
BegIdx := 1;
|
|
while begIdx < length and then (s(begIdx) = BLANK or s(begIdx) = TAB) loop
|
|
--# assert begIdx >= 1 and begIdx < length;
|
|
begIdx := begIdx + 1;
|
|
end loop;
|
|
|
|
--find end of key fragment
|
|
EndIdx := BegIdx;
|
|
while EndIdx < length and then (s(EndIdx) /= BLANK and s(EndIdx) /= TAB) loop
|
|
--# assert begIdx >= 1 and begIdx <= endIdx and endIdx >= 1 and endIdx < length;
|
|
endIdx:= endIdx + 1;
|
|
end loop;
|
|
|
|
--check if key too long
|
|
if RRSIG_Rec.SignatureLength + ((EndIdx-BegIdx)+1) > Rr_Type.RRSIG_Record_Type.MaxRRSigLength then
|
|
Success := False;
|
|
else
|
|
--add key fragment on to key field of record
|
|
for I in Integer range BegIdx..EndIdx loop
|
|
--# assert BegIdx = begIdx% and EndIdx = EndIdx% and I >= BegIdx and I <= EndIdx
|
|
--# and BegIdx >= 1
|
|
--# and RRSIG_Rec.SignatureLength + ((EndIdx-BegIdx)+1) <= Rr_Type.RRSIG_Record_Type.MaxRRSigLength;
|
|
RRSIG_Rec.Signature(RRSIG_Rec.SignatureLength+((I-BegIdx)+1)) := S(I);
|
|
end loop;
|
|
--update signature length
|
|
RRSIG_Rec.SignatureLength := RRSIG_Rec.SignatureLength + ((endIdx-begIdx) + 1);
|
|
end if;
|
|
|
|
--SPARK caught runtime error if no ')', nice!
|
|
if EndIdx < Length then
|
|
--if line ends with right paren then all done
|
|
begIdx := endIdx + 1;
|
|
FindNextToken(s, Length, BegIdx, EndIdx, ReturnedType);
|
|
|
|
--if ')' found, record complete, can insert in table
|
|
--begIdx <= endIdx always true, makes flow errors go away
|
|
if ReturnedType = Rr_Type.RParen and BegIdx <= EndIdx then
|
|
AllDone := True;
|
|
else
|
|
AllDone := False; --makes flow error go away
|
|
end if;
|
|
else --nothing after the key fragment, need to keep going
|
|
AllDone := False;
|
|
end if;
|
|
end AddToKeyR;
|
|
|
|
+++ Flow analysis of subprogram AddToKeyR performed:
|
|
no errors found.
|
|
|
|
|
|
procedure AddToKey(DNSKEY_Rec : in out rr_type.dnskey_record_type.DNSKeyRecordType;
|
|
s: in Rr_Type.LineFromFileType;
|
|
Length : in Rr_Type.LineLengthIndex;
|
|
success : in out boolean)
|
|
is
|
|
BegIdx : Rr_Type.LineLengthIndex;
|
|
endIdx : rr_type.LineLengthIndex;
|
|
begin
|
|
--find start of key fragment
|
|
BegIdx := 1;
|
|
while begIdx < length and then (s(begIdx) = BLANK or s(begIdx) = TAB) loop
|
|
--# assert begIdx >= 1 and begIdx < length;
|
|
begIdx := begIdx + 1;
|
|
end loop;
|
|
|
|
--find end of key fragment
|
|
EndIdx := BegIdx;
|
|
while EndIdx < length and then (s(EndIdx) /= BLANK and s(EndIdx) /= TAB) loop
|
|
--# assert begIdx >= 1 and begIdx <= endIdx and endIdx >= 1 and endIdx < length;
|
|
endIdx:= endIdx + 1;
|
|
end loop;
|
|
|
|
--check if key too long
|
|
if DNSKEY_Rec.KeyLength + ((EndIdx-BegIdx)+1) > Rr_Type.Dnskey_Record_Type.MaxDNSKeyLength then
|
|
Success := False;
|
|
else
|
|
--add key fragment on to key field of record
|
|
for I in Integer range BegIdx..EndIdx loop
|
|
--# assert BegIdx = begIdx% and EndIdx = EndIdx% and I >= BegIdx and I <= EndIdx
|
|
--# and BegIdx >= 1
|
|
--# and DNSKEY_Rec.KeyLength + ((EndIdx-BegIdx)+1) <= Rr_Type.Dnskey_Record_Type.MaxDNSKeyLength;
|
|
DNSKEY_Rec.Key(DNSKEY_Rec.KeyLength+((I-BegIdx)+1)) := S(I);
|
|
end loop;
|
|
--update key length
|
|
DNSKEY_Rec.KeyLength := DNSKEY_Rec.KeyLength + ((EndIdx-BegIdx) + 1);
|
|
end if;
|
|
end AddToKey;
|
|
|
|
+++ Flow analysis of subprogram AddToKey performed:
|
|
no errors found.
|
|
|
|
|
|
--convert ipv6 address at s(begIdx..endIdx) into 8 unsigned 16-bit integers
|
|
--expects eight valid 16-bit hex numbers separated by colons
|
|
--returns INVALID_IPV6_ADDR if conversion unsuccessful
|
|
function convertIpv6(s : in rr_type.LineFromFileType;
|
|
begIdx: in rr_type.LineLengthIndex;
|
|
endIdx: in rr_type.LineLengthIndex) RETURN rr_type.aaaa_record_type.IPV6AddrType
|
|
is
|
|
NUM_FIELDS: constant Natural := 8;
|
|
REQ_NUM_SEPARATORS : constant Natural := NUM_FIELDS-1;
|
|
FIELD_SEPARATOR : constant Character := ':';
|
|
subtype SeparatorIndexType is Integer range 1..REQ_NUM_SEPARATORS+1; --could go one higher if processing bad ip
|
|
type SeparatorIndexArrayType is array(SeparatorIndexType) of Rr_Type.LineLengthIndex;
|
|
|
|
MAX_DIGITS_IN_FIELD: constant Natural := 4;
|
|
IPV6_RADIX : constant unsigned_types.unsigned16 := 16;
|
|
|
|
SeparatorIndexArray : SeparatorIndexArrayType := SeparatorIndexArrayType'(others => 1);
|
|
Ctr : Rr_Type.LineLengthIndex;
|
|
NumSeparators : Natural;
|
|
fieldTotal : unsigned_types.unsigned16;
|
|
numDigitsInField : Natural;
|
|
|
|
RetVal : Rr_Type.Aaaa_Record_Type.IPV6AddrType := Rr_Type.Aaaa_Record_Type.INVALID_IPV6_ADDR;
|
|
|
|
function SeparatorsOK(Line : in Rr_Type.LineFromFileType; SArray : in SeparatorIndexArrayType) return Boolean is
|
|
retVal : boolean := true;
|
|
begin
|
|
--no need to check the last entry, that will have been detected elsewhere
|
|
for I in integer range SeparatorIndexType'First..SeparatorIndexType'last-1 loop
|
|
--# assert true;
|
|
if line(SArray(I)) /= FIELD_SEPARATOR or SArray(I) = SArray(I+1) - 1 then
|
|
RetVal := false;
|
|
exit;
|
|
end if;
|
|
end loop;
|
|
return retVal;
|
|
end SeparatorsOK;
|
|
|
|
+++ Flow analysis of subprogram SeparatorsOK
|
|
performed: no errors found.
|
|
|
|
|
|
begin
|
|
Ctr := BegIdx;
|
|
NumSeparators := 0;
|
|
FieldTotal := 0;
|
|
NumDigitsInField := 0;
|
|
|
|
while Ctr < EndIdx and then (NumSeparators <= REQ_NUM_SEPARATORS and NumDigitsInField <= MAX_DIGITS_IN_FIELD) loop
|
|
--# assert ctr < endIdx and numSeparators <= REQ_NUM_SEPARATORS and numDigitsInField <= MAX_DIGITS_IN_FIELD;
|
|
if Ada.Characters.Handling.Is_Decimal_Digit(S(Ctr)) then
|
|
fieldTotal := IPV6_RADIX*fieldTotal + (Character'Pos(S(Ctr))-Character'Pos('0'));
|
|
NumDigitsInField := NumDigitsInField +1;
|
|
elsif Ada.Characters.Handling.Is_Hexadecimal_Digit(S(Ctr)) then
|
|
FieldTotal := IPV6_RADIX*FieldTotal + (Character'Pos(Ada.Characters.Handling.To_Upper(S(Ctr)))-Character'Pos('A'))+10;
|
|
NumDigitsInField := NumDigitsInField +1;
|
|
else
|
|
NumSeparators := NumSeparators+1;
|
|
SeparatorIndexArray(NumSeparators) := Ctr;
|
|
retVal(numSeparators) := fieldTotal;
|
|
fieldTotal := 0;
|
|
numDigitsInField := 0;
|
|
end if;
|
|
ctr := ctr + 1;
|
|
end loop;
|
|
--endIdx might be the maximum value possible, so must catch last character here
|
|
if Ctr = EndIdx and numSeparators <= REQ_NUM_SEPARATORS then
|
|
if Ada.Characters.Handling.Is_Decimal_Digit(S(Ctr)) then
|
|
fieldTotal := IPV6_RADIX*fieldTotal + (Character'Pos(S(Ctr))-Character'Pos('0'));
|
|
NumDigitsInField := NumDigitsInField +1;
|
|
retVal(numSeparators+1) := fieldTotal;
|
|
elsif Ada.Characters.Handling.Is_Hexadecimal_Digit(S(Ctr)) then
|
|
FieldTotal := IPV6_RADIX*FieldTotal + (Character'Pos(Ada.Characters.Handling.To_Upper(S(Ctr)))-Character'Pos('A'))+10;
|
|
NumDigitsInField := NumDigitsInField +1;
|
|
retVal(numSeparators+1) := fieldTotal;
|
|
else --if last character is anything but an integer, force an error
|
|
NumSeparators := NUM_FIELDS;
|
|
end if;
|
|
end if;
|
|
|
|
if not (SeparatorsOK(s, SeparatorIndexArray) and numSeparators = REQ_NUM_SEPARATORS and numDigitsInField <= MAX_DIGITS_IN_FIELD) then
|
|
RetVal := Rr_Type.Aaaa_Record_Type.INVALID_IPV6_ADDR;
|
|
end if;
|
|
|
|
return retVal;
|
|
end ConvertIpv6;
|
|
|
|
+++ Flow analysis of subprogram convertIpv6
|
|
performed: no errors found.
|
|
|
|
|
|
--convert ipv4 address at s(begIdx..endIdx) into a 32-bit number
|
|
--returns 0 if conversion unsuccessful
|
|
function convertIpv4(s : in rr_type.LineFromFileType;
|
|
begIdx: in rr_type.LineLengthIndex;
|
|
endIdx: in rr_type.LineLengthIndex) return unsigned_types.unsigned32
|
|
is
|
|
NUM_BYTES : constant Natural := 4;
|
|
REQ_NUM_SEPARATORS : constant Natural := NUM_BYTES-1;
|
|
BYTE_SEPARATOR : constant Character := '.';
|
|
subtype SeparatorIndexType is Integer range 1..REQ_NUM_SEPARATORS+1; --could go one higher if processing bad ip
|
|
type SeparatorIndexArrayType is array(SeparatorIndexType) of Rr_Type.LineLengthIndex;
|
|
|
|
MAX_BYTE_VALUE : CONSTANT unsigned_types.unsigned32 := 255;
|
|
MAX_DIGITS_PER_BYTE : constant Natural := 3;
|
|
IPV4_RADIX : constant unsigned_types.unsigned32:= 10;
|
|
|
|
SeparatorIndexArray : SeparatorIndexArrayType := SeparatorIndexArrayType'(others => 1);
|
|
|
|
Ctr : Rr_Type.LineLengthIndex;
|
|
NumSeparators : Natural;
|
|
ByteTotal : unsigned_types.unsigned32;
|
|
numDigitsInByte : Natural;
|
|
GrandTotal : unsigned_types.unsigned32;
|
|
RetVal : Unsigned_Types.Unsigned32;
|
|
|
|
function SeparatorsOK(Line : in Rr_Type.LineFromFileType; SArray : in SeparatorIndexArrayType) return Boolean is
|
|
retVal : boolean ;
|
|
begin
|
|
if Line(SArray(1)) = BYTE_SEPARATOR and Line(SArray(2)) = BYTE_SEPARATOR and Line(SArray(3)) = BYTE_SEPARATOR
|
|
and Sarray(1) /= Sarray(2)-1 and Sarray(2) /= Sarray(3)-1 then
|
|
retVal := true;
|
|
else
|
|
retVal := False;
|
|
end if;
|
|
return retVal;
|
|
end SeparatorsOK;
|
|
|
|
+++ Flow analysis of subprogram SeparatorsOK
|
|
performed: no errors found.
|
|
|
|
|
|
begin
|
|
Ctr := BegIdx;
|
|
NumSeparators := 0;
|
|
ByteTotal := 0;
|
|
numDigitsInByte := 0;
|
|
GrandTotal := 0;
|
|
while Ctr < endIdx and then (NumSeparators <= REQ_NUM_SEPARATORS and ByteTotal <= MAX_BYTE_VALUE
|
|
and numDigitsInByte <= MAX_DIGITS_PER_BYTE) loop
|
|
--# assert ctr < endIdx and numSeparators <= REQ_NUM_SEPARATORS and numDigitsInByte <= MAX_DIGITS_PER_BYTE;
|
|
if Ada.Characters.Handling.Is_Digit(S(Ctr)) then
|
|
ByteTotal := IPV4_RADIX*ByteTotal + (Character'Pos(S(Ctr))-Character'Pos('0'));
|
|
numDigitsinbyte := numDigitsInByte+1;
|
|
else
|
|
NumSeparators := NumSeparators+1;
|
|
SeparatorIndexArray(NumSeparators) := Ctr;
|
|
grandTotal := (MAX_BYTE_VALUE+1)*grandTotal + byteTotal;
|
|
ByteTotal := 0;
|
|
numDigitsInByte := 0;
|
|
end if;
|
|
ctr := ctr+1;
|
|
end loop;
|
|
|
|
--endIdx might be the maximum value possible, so must catch last character here
|
|
if Ctr = EndIdx then
|
|
if Ada.Characters.Handling.Is_Digit(S(Ctr)) then
|
|
ByteTotal := 10*ByteTotal + (Character'Pos(S(Ctr))-Character'Pos('0'));
|
|
NumDigitsinbyte := NumDigitsInByte+1;
|
|
grandTotal := (MAX_BYTE_VALUE+1)*grandTotal + byteTotal;
|
|
else --if last character is anything but an integer, force an error
|
|
NumSeparators := NUM_BYTES;
|
|
end if;
|
|
end if;
|
|
if SeparatorsOK(s, separatorIndexArray) and NumSeparators = REQ_NUM_SEPARATORS and NumDigitsInByte <= MAX_DIGITS_PER_BYTE
|
|
and ByteTotal <= MAX_BYTE_VALUE then
|
|
RetVal := grandTotal;
|
|
else
|
|
RetVal := rr_type.a_record_type.INVALID_IPV4_ADDR;
|
|
end if;
|
|
return retVal;
|
|
end ConvertIpv4;
|
|
|
|
+++ Flow analysis of subprogram convertIpv4
|
|
performed: no errors found.
|
|
|
|
|
|
|
|
|
|
END Parser_Utilities;
|
|
|
|
|
|
--End of file--------------------------------------------------
|