810 lines
37 KiB
Plaintext
810 lines
37 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;
|
|
--In case debugging IO needed
|
|
--with Ada.Text_IO;
|
|
package body Dns_Table_Pkg
|
|
|
|
is
|
|
|
|
protected body Dns_Table_Type is
|
|
--UTILITIES
|
|
function To_Lower(DomainName : in Rr_Type.WireStringType) return Rr_Type.WireStringType is
|
|
LowerCaseVersion : Rr_Type.WireStringType := Rr_Type.BlankWire;
|
|
length : rr_type.wireStringTypeIndex;
|
|
begin
|
|
Length := Rr_Type.WireNameLength(domainName);
|
|
for I in Integer range 1..Length loop
|
|
--# assert true;
|
|
LowerCaseVersion(I) := Ada.Characters.Handling.to_lower(domainName(I));
|
|
end loop;
|
|
return lowerCaseVersion;
|
|
end To_Lower;
|
|
|
|
+++ Flow analysis of subprogram To_Lower performed:
|
|
no errors found.
|
|
|
|
|
|
function Same(X,Y : in RR_Type.WireStringType) return Boolean is
|
|
Length : Rr_Type.WireStringTypeIndex;
|
|
result : boolean;
|
|
begin
|
|
result := true;
|
|
Length := Rr_Type.WireNameLength(x);
|
|
for I in Integer range 1..Length loop
|
|
--#assert true;
|
|
if X(I)/=Y(I) then
|
|
Result := False;
|
|
exit;
|
|
end if;
|
|
end loop;
|
|
return result;
|
|
end Same;
|
|
|
|
+++ Flow analysis of subprogram Same performed: no
|
|
errors found.
|
|
|
|
|
|
function hash(domainName : in rr_type.WireStringType)
|
|
return Rr_Type.NumBucketsIndexType
|
|
--return val => (1 <= val and val <= rr_type.NumBuckets);
|
|
is
|
|
NumCharsInHashFunction : constant Natural := 4;
|
|
val : natural := 0;
|
|
begin
|
|
for i in integer range 1..NumCharsInHashFunction loop
|
|
--# assert val <= (i-1)*Character'Pos(Character'Last)
|
|
--# and (for all Q in rr_type.WireStringTypeIndex =>
|
|
--# (character'pos(domainname(Q))<=255 and
|
|
--# character'pos(domainname(Q))>=0));
|
|
val := val + Character'Pos(domainName(i));
|
|
end loop;
|
|
return (val mod rr_type.NumBuckets) + 1;
|
|
end hash;
|
|
|
|
+++ Flow analysis of subprogram hash performed: no
|
|
errors found.
|
|
|
|
|
|
--QUERY PROCEDURES
|
|
procedure queryARecords(
|
|
domainName : in rr_type.WireStringType;
|
|
returnedRecords : out rr_type.a_record_type.ARecordBucketType;
|
|
howMany : out rr_type.NumberOfRecordsType)
|
|
--# global in ARecordTable, ARecordKeys;
|
|
--# derives howMany from ARecordKeys, domainName &
|
|
--# returnedRecords from ARecordKeys, ARecordTable, domainName;
|
|
is
|
|
Bucket : Rr_Type.NumBucketsIndexType;
|
|
Lower_DomainName : rr_type.WireStringType;
|
|
begin
|
|
-- must initialize the whole array to make flow error go away
|
|
-- returnedRecords := rr_type.a_record_type.ARecordBucketType'(
|
|
-- others => rr_type.a_record_type.blankARecord);
|
|
Lower_Domainname := To_Lower(DomainName);
|
|
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(DomainName);
|
|
howMany := 0;
|
|
for ctr in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
exit when ARecordKeys(Bucket)(Ctr)(1) = ASCII.NUL;
|
|
--if To_Lower(ARecordTable(Bucket)(Ctr).Owner) = Lower_domainName then
|
|
if Same(ARecordKeys(Bucket)(Ctr),Lower_domainName) then
|
|
HowMany := HowMany+1;
|
|
--# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
returnedRecords(howMany) := ARecordTable(bucket)(ctr);
|
|
--# end accept;
|
|
end if;
|
|
end loop;
|
|
--# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
end QueryARecords;
|
|
|
|
+++ Flow analysis of subprogram queryARecords
|
|
performed: no errors found.
|
|
|
|
|
|
procedure queryAAAARecords(
|
|
domainName : in rr_type.WireStringType;
|
|
returnedRecords : out rr_type.aaaa_record_type.AAAARecordBucketType;
|
|
howMany : out rr_type.NumberOfRecordsType)
|
|
--# global in AAAARecordTable, AAAARecordKeys;
|
|
--# derives howMany from AAAARecordKeys, domainName &
|
|
--# returnedRecords from AAAARecordKeys, AAAARecordTable, domainName;
|
|
is
|
|
bucket : rr_type.NumBucketsIndexType;
|
|
Lower_Domainname : rr_Type.WireStringType;
|
|
begin
|
|
Lower_Domainname := To_Lower(Domainname);
|
|
-- must initialize the whole array to make flow error go away
|
|
-- returnedRecords := rr_type.aaaa_record_type.AAAARecordBucketType'(
|
|
-- others => rr_type.aaaa_record_type.blankAAAARecord);
|
|
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_DomainName);
|
|
howMany := 0;
|
|
for ctr in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
exit when AAAARecordKeys(Bucket)(Ctr)(1) = ASCII.NUL;
|
|
-- if To_Lower(AAAARecordTable(Bucket)(Ctr).Owner) = Lower_domainName then
|
|
if Same(AaaaRecordKeys(Bucket)(Ctr),Lower_domainName) then
|
|
howMany := howMany+1;
|
|
--# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
returnedRecords(howMany) := AAAARecordTable(bucket)(ctr);
|
|
--# end accept;
|
|
end if;
|
|
end loop;
|
|
--# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
end queryAAAARecords;
|
|
|
|
+++ Flow analysis of subprogram queryAAAARecords
|
|
performed: no errors found.
|
|
|
|
|
|
|
|
procedure queryCNAMERecords(domainName : in rr_type.WireStringType;
|
|
returnedRecords : out rr_type.cname_record_type.CNAMERecordBucketType;
|
|
howMany : out rr_type.NumberOfRecordsType)
|
|
--# global in CNAMERecordTable, CNAMERecordKeys;
|
|
--# derives howMany from CNAMERecordKeys, domainName &
|
|
--# returnedRecords from CNAMERecordKeys, CNAMERecordTable, domainName;
|
|
is
|
|
Bucket : Rr_Type.NumBucketsIndexType;
|
|
Lower_Domainname : rr_Type.WireStringType;
|
|
begin
|
|
Lower_Domainname := To_Lower(Domainname);
|
|
-- must initialize the whole array to make flow error go away
|
|
-- returnedRecords := rr_type.cname_record_type.CNAMERecordBucketType'(
|
|
-- others => Rr_Type.Cname_Record_Type.BlankCNAMERecord);
|
|
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Domainname);
|
|
howMany := 0;
|
|
for ctr in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
exit when CNAMERecordKeys(bucket)(ctr)(1) = ASCII.NUL;
|
|
if Same(CNAMERecordKeys(Bucket)(Ctr),Lower_domainName) then
|
|
howMany := howMany+1;
|
|
--# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
returnedRecords(howMany) := CNAMERecordTable(bucket)(ctr);
|
|
--# end accept;
|
|
end if;
|
|
end loop;
|
|
--# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
END QueryCNAMERecords;
|
|
|
|
+++ Flow analysis of subprogram queryCNAMERecords
|
|
performed: no errors found.
|
|
|
|
|
|
procedure queryDNSKEYRecords(domainName : in rr_type.WireStringType;
|
|
returnedRecords : out rr_type.DNSKEY_record_type.DNSKEYRecordBucketType;
|
|
howMany : out rr_type.NumberOfRecordsType)
|
|
--# global in DNSKEYRecordTable, DNSKEYRecordKeys;
|
|
--# derives howMany from DNSKEYRecordKeys, domainName &
|
|
--# returnedRecords from DNSKEYRecordKeys, DNSKEYRecordTable, domainName;
|
|
is
|
|
Bucket : Rr_Type.NumBucketsIndexType;
|
|
Lower_Domainname : rr_Type.WireStringType;
|
|
begin
|
|
Lower_Domainname := To_Lower(Domainname);
|
|
-- must initialize the whole array to make flow error go away
|
|
-- returnedRecords := rr_type.DNSKEY_record_type.DNSKEYRecordBucketType'(
|
|
-- others => Rr_Type.DNSKEY_Record_Type.BlankDNSKEYRecord);
|
|
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Domainname);
|
|
howMany := 0;
|
|
for ctr in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
exit when DNSKEYRecordKeys(bucket)(ctr)(1) = ASCII.NUL;
|
|
if Same(DNSKEYRecordKeys(Bucket)(Ctr),Lower_domainName) then
|
|
howMany := howMany+1;
|
|
--# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
returnedRecords(howMany) := DNSKEYRecordTable(bucket)(ctr);
|
|
--# end accept;
|
|
end if;
|
|
end loop;
|
|
--# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
END QueryDNSKEYRecords;
|
|
|
|
+++ Flow analysis of subprogram queryDNSKEYRecords
|
|
performed: no errors found.
|
|
|
|
|
|
procedure queryMXRecords(
|
|
domainName : in rr_type.WireStringType;
|
|
returnedRecords : out rr_type.mx_record_type.MXRecordBucketType;
|
|
howMany : out rr_type.NumberOfRecordsType)
|
|
--# global in MXRecordTable, MXRecordKeys;
|
|
--# derives howMany from MXRecordKeys, domainName &
|
|
--# returnedRecords from MXRecordKeys, MXRecordTable, domainName;
|
|
is
|
|
Bucket : Rr_Type.NumBucketsIndexType;
|
|
Lower_Domainname : rr_Type.WireStringType;
|
|
begin
|
|
Lower_Domainname := To_Lower(Domainname);
|
|
-- must initialize the whole array to make flow error go away
|
|
-- returnedRecords := rr_type.mx_record_type.MXRecordBucketType'(
|
|
-- others => rr_Type.mx_Record_Type.BlankMXRecord);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Domainname);
|
|
|
|
howMany := 0;
|
|
for ctr in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
exit when MXRecordKeys(bucket)(ctr)(1) = ASCII.NUL;
|
|
if Same(MXRecordKeys(Bucket)(Ctr),Lower_domainName) then
|
|
howMany := howMany+1;
|
|
--# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
returnedRecords(howMany) := MXRecordTable(bucket)(ctr);
|
|
--# end accept;
|
|
end if;
|
|
end loop;
|
|
--# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
END queryMXRecords;
|
|
|
|
+++ Flow analysis of subprogram queryMXRecords
|
|
performed: no errors found.
|
|
|
|
|
|
procedure queryNSRecords(
|
|
domainName : in rr_type.WireStringType;
|
|
returnedRecords : out rr_type.ns_record_type.NSRecordBucketType;
|
|
howMany : out rr_type.NumberOfRecordsType)
|
|
--# global in NSRecordTable, NSRecordKeys;
|
|
--# derives howMany from NSRecordKeys, domainName &
|
|
--# returnedRecords from NSRecordKeys, NSRecordTable, domainName;
|
|
is
|
|
Bucket : Rr_Type.NumBucketsIndexType;
|
|
Lower_Domainname : rr_Type.WireStringType;
|
|
begin
|
|
Lower_Domainname := To_Lower(Domainname);
|
|
-- must initialize the whole array to make flow error go away
|
|
-- returnedRecords := rr_type.NS_record_type.NSRecordBucketType'(
|
|
-- others => Rr_Type.NS_Record_Type.BlankNSRecord);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Domainname);
|
|
|
|
howMany := 0;
|
|
for ctr in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
exit when NSRecordKeys(bucket)(ctr)(1) = ASCII.NUL;
|
|
if Same(NSRecordKeys(Bucket)(Ctr),Lower_domainName) then
|
|
howMany := howMany+1;
|
|
--# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
returnedRecords(howMany) := NSRecordTable(bucket)(ctr);
|
|
--# end accept;
|
|
end if;
|
|
end loop;
|
|
--# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
end QueryNSRecords;
|
|
|
|
+++ Flow analysis of subprogram queryNSRecords
|
|
performed: no errors found.
|
|
|
|
|
|
procedure queryNSECRecords(
|
|
domainName : in rr_type.WireStringType;
|
|
returnedRecords : out rr_type.nsec_record_type.NSECRecordBucketType;
|
|
howMany : out rr_type.NumberOfRecordsType)
|
|
--# global in NSECRecordTable, NSECRecordKeys;
|
|
--# derives howMany from NSECRecordKeys, domainName &
|
|
--# returnedRecords from NSECRecordKeys, NSECRecordTable, domainName;
|
|
is
|
|
Bucket : Rr_Type.NumBucketsIndexType;
|
|
Lower_Domainname : rr_Type.WireStringType;
|
|
begin
|
|
Lower_Domainname := To_Lower(Domainname);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Domainname);
|
|
howMany := 0;
|
|
for ctr in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
exit when NSECRecordKeys(bucket)(ctr)(1) = ASCII.NUL;
|
|
if Same(NSECRecordKeys(Bucket)(Ctr),Lower_domainName) then
|
|
howMany := howMany+1;
|
|
--# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
returnedRecords(howMany) := NSECRecordTable(bucket)(ctr);
|
|
--# end accept;
|
|
end if;
|
|
end loop;
|
|
--# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
end queryNSECRecords;
|
|
|
|
+++ Flow analysis of subprogram queryNSECRecords
|
|
performed: no errors found.
|
|
|
|
|
|
|
|
procedure queryPTRRecords(
|
|
domainName : in rr_type.WireStringType;
|
|
returnedRecords : out rr_type.PTR_record_type.PTRRecordBucketType;
|
|
howMany : out rr_type.NumberOfRecordsType)
|
|
--# global in PTRRecordTable, PTRRecordKeys;
|
|
--# derives howMany from PTRRecordKeys, domainName &
|
|
--# returnedRecords from PTRRecordKeys, PTRRecordTable, domainName;
|
|
is
|
|
Bucket : Rr_Type.NumBucketsIndexType;
|
|
Lower_Domainname : rr_Type.WireStringType;
|
|
begin
|
|
Lower_Domainname := To_Lower(Domainname);
|
|
-- must initialize the whole array to make flow error go away
|
|
-- returnedRecords := rr_type.ptr_record_type.PTRRecordBucketType'(
|
|
-- others => Rr_Type.ptr_Record_Type.BlankPTRRecord);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Domainname);
|
|
|
|
howMany := 0;
|
|
for ctr in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert howMany >= 0 and howMany < ctr
|
|
--# and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
exit when PTRRecordKeys(bucket)(ctr)(1) = ASCII.NUL;
|
|
if Same(PTRRecordKeys(Bucket)(Ctr),Lower_domainName) then
|
|
howMany := howMany+1;
|
|
--# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
returnedRecords(howMany) := PTRRecordTable(bucket)(ctr);
|
|
--# end accept;
|
|
end if;
|
|
end loop;
|
|
--# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
END QueryPTRRecords;
|
|
|
|
+++ Flow analysis of subprogram queryPTRRecords
|
|
performed: no errors found.
|
|
|
|
|
|
procedure queryRRSIGRecords(domainName : in rr_type.WireStringType;
|
|
returnedRecords : out rr_type.RRSIG_record_type.RRSIGRecordBucketType;
|
|
howMany : out rr_type.NumberOfRecordsType)
|
|
--# global in RRSIGRecordTable, RRSIGRecordKeys;
|
|
--# derives howMany from RRSIGRecordKeys, domainName &
|
|
--# returnedRecords from RRSIGRecordKeys, RRSIGRecordTable, domainName;
|
|
is
|
|
Bucket : Rr_Type.NumBucketsIndexType;
|
|
Lower_Domainname : rr_Type.WireStringType;
|
|
begin
|
|
Lower_Domainname := To_Lower(Domainname);
|
|
-- must initialize the whole array to make flow error go away
|
|
-- returnedRecords := rr_type.RRSIG_record_type.RRSIGRecordBucketType'(
|
|
-- others => Rr_Type.RRSIG_Record_Type.BlankRRSIGRecord);
|
|
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Domainname);
|
|
howMany := 0;
|
|
for ctr in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
exit when RRSIGRecordKeys(bucket)(ctr)(1) = ASCII.NUL;
|
|
if Same(RRSIGRecordKeys(Bucket)(Ctr),Lower_domainName) then
|
|
howMany := howMany+1;
|
|
--# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
returnedRecords(howMany) := RRSIGRecordTable(bucket)(ctr);
|
|
--# end accept;
|
|
end if;
|
|
end loop;
|
|
--# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
END QueryRRSIGRecords;
|
|
|
|
+++ Flow analysis of subprogram queryRRSIGRecords
|
|
performed: no errors found.
|
|
|
|
|
|
procedure querySOARecords(
|
|
domainName : in rr_type.WireStringType;
|
|
returnedRecords : out rr_type.SOA_record_type.SOARecordBucketType;
|
|
howMany : out rr_type.NumberOfRecordsType)
|
|
--# global in SOARecordTable, SOARecordKeys;
|
|
--# derives howMany from SOARecordKeys, domainName &
|
|
--# returnedRecords from SOARecordKeys, SOARecordTable, domainName;
|
|
is
|
|
Bucket : Rr_Type.NumBucketsIndexType;
|
|
Lower_Domainname : rr_Type.WireStringType;
|
|
begin
|
|
Lower_Domainname := To_Lower(Domainname);
|
|
-- must initialize the whole array to make flow error go away
|
|
-- returnedRecords := rr_type.soa_record_type.soaRecordBucketType'(
|
|
-- others => Rr_Type.soa_Record_Type.BlankSOARecord);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Domainname);
|
|
|
|
howMany := 0;
|
|
for ctr in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert howMany >= 0 and howMany < ctr
|
|
--# and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
exit when SOARecordKeys(bucket)(ctr)(1) = ASCII.NUL;
|
|
if Same(soarecordKeys(Bucket)(Ctr),Lower_domainName) then
|
|
howMany := howMany+1;
|
|
--# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
ReturnedRecords(HowMany) := SOARecordTable(Bucket)(Ctr);
|
|
--# end accept;
|
|
end if;
|
|
end loop;
|
|
--# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
END QuerySOARecords;
|
|
|
|
+++ Flow analysis of subprogram querySOARecords
|
|
performed: no errors found.
|
|
|
|
|
|
--INSERT PROCEDURES
|
|
procedure InsertARecord(Key : in Rr_Type.WireStringType;
|
|
theRecord : in rr_type.a_record_type.ARecordType;
|
|
success : out boolean)
|
|
--# global in out ARecordTable, ARecordKeys;
|
|
--# derives ARecordTable from *, ARecordKeys, theRecord, Key &
|
|
--# ARecordKeys from *, Key &
|
|
--# success from ARecordKeys, Key;
|
|
is
|
|
bucket : rr_type.NumBucketsIndexType;
|
|
Lower_Key : RR_Type.WireStringType;
|
|
begin
|
|
Lower_Key := To_Lower(Key);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Key);
|
|
|
|
success := false;
|
|
for i in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert true;
|
|
if ARecordKeys(bucket)(i) = rr_type.BlankOwner then
|
|
ARecordKeys(bucket)(i) := Lower_Key;
|
|
ARecordTable(bucket)(i) := theRecord;
|
|
success := true;
|
|
end if;
|
|
exit when success;
|
|
end loop;
|
|
END InsertARecord;
|
|
|
|
+++ Flow analysis of subprogram insertARecord
|
|
performed: no errors found.
|
|
|
|
|
|
procedure insertAAAARecord(Key : in Rr_Type.WireStringType;
|
|
theRecord : in rr_type.aaaa_record_type.AAAARecordType;
|
|
success : out boolean)
|
|
--# global in out AAAARecordTable, AAAARecordKeys;
|
|
--# derives AAAARecordTable from *, AAAARecordKeys, theRecord, Key &
|
|
--# AAAARecordKeys from *, Key &
|
|
--# success from AAAARecordKeys, Key;
|
|
is
|
|
Bucket : Rr_Type.NumBucketsIndexType;
|
|
Lower_Key : RR_Type.WireStringType;
|
|
begin
|
|
Lower_Key := To_Lower(Key);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Key);
|
|
|
|
success := false;
|
|
for i in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert true;
|
|
if AAAARecordKeys(bucket)(i) = rr_type.BlankOwner then
|
|
AAAARecordKeys(bucket)(i) := Lower_Key;
|
|
AAAARecordTable(bucket)(i) := theRecord;
|
|
success := true;
|
|
end if;
|
|
exit when success;
|
|
end loop;
|
|
END InsertAAAARecord;
|
|
|
|
+++ Flow analysis of subprogram insertAAAARecord
|
|
performed: no errors found.
|
|
|
|
|
|
procedure InsertCNAMERecord(Key : in Rr_Type.WireStringType;
|
|
theRecord : in rr_type.cname_record_type.CNAMERecordType;
|
|
success : out boolean)
|
|
--# global in out CNAMERecordTable, CNAMERecordKeys;
|
|
--# derives CNAMERecordTable from *, CNAMERecordKeys, theRecord, Key &
|
|
--# CNAMERecordKeys from *, Key &
|
|
--# success from CNAMERecordKeys, Key;
|
|
is
|
|
bucket : rr_type.NumBucketsIndexType;
|
|
Lower_Key : RR_Type.WireStringType;
|
|
begin
|
|
Lower_Key := To_Lower(Key);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Key);
|
|
|
|
success := false;
|
|
for i in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert true;
|
|
if CNAMERecordKeys(bucket)(i) = rr_type.BlankOwner then
|
|
CNAMERecordKeys(bucket)(i) := Lower_Key;
|
|
CNAMERecordTable(bucket)(i) := theRecord;
|
|
success := true;
|
|
end if;
|
|
exit when success;
|
|
end loop;
|
|
END InsertCNAMERecord;
|
|
|
|
+++ Flow analysis of subprogram insertCNAMERecord
|
|
performed: no errors found.
|
|
|
|
|
|
procedure InsertDNSKEYRecord(Key : in Rr_Type.WireStringType;
|
|
theRecord : in rr_type.DNSKEY_record_type.DNSKEYRecordType;
|
|
success : out boolean)
|
|
--# global in out DNSKEYRecordTable, DNSKEYRecordKeys;
|
|
--# derives DNSKEYRecordTable from *, DNSKEYRecordKeys, theRecord, Key &
|
|
--# DNSKEYRecordKeys from *, Key &
|
|
--# success from DNSKEYRecordKeys, Key;
|
|
is
|
|
bucket : rr_type.NumBucketsIndexType;
|
|
Lower_Key : RR_Type.WireStringType;
|
|
begin
|
|
Lower_Key := To_Lower(Key);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Key);
|
|
|
|
success := false;
|
|
for i in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert true;
|
|
if DNSKEYRecordKeys(bucket)(i) = rr_type.BlankOwner then
|
|
DNSKEYRecordKeys(bucket)(i) := Lower_Key;
|
|
DNSKEYRecordTable(bucket)(i) := theRecord;
|
|
success := true;
|
|
end if;
|
|
exit when success;
|
|
end loop;
|
|
END InsertDNSKEYRecord;
|
|
|
|
+++ Flow analysis of subprogram InsertDNSKEYRecord
|
|
performed: no errors found.
|
|
|
|
|
|
|
|
procedure insertMXRecord(Key : in Rr_Type.WireStringType;
|
|
theRecord : in rr_type.mx_record_type.MXRecordType;
|
|
success : out boolean)
|
|
--# global in out MXRecordTable, MXRecordKeys;
|
|
--# derives MXRecordTable from *, MXRecordKeys, theRecord, Key &
|
|
--# MXRecordKeys from *, Key &
|
|
--# success from MXRecordKeys, Key;
|
|
is
|
|
bucket : rr_type.NumBucketsIndexType;
|
|
Lower_Key : RR_Type.WireStringType;
|
|
begin
|
|
Lower_Key := To_Lower(Key);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Key);
|
|
|
|
success := false;
|
|
for i in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert true;
|
|
if MXRecordKeys(bucket)(i) = rr_type.BlankOwner then
|
|
MXRecordKeys(bucket)(i) := Lower_Key;
|
|
MXRecordTable(bucket)(i) := theRecord;
|
|
success := true;
|
|
end if;
|
|
exit when success;
|
|
end loop;
|
|
END InsertMXRecord;
|
|
|
|
+++ Flow analysis of subprogram insertMXRecord
|
|
performed: no errors found.
|
|
|
|
|
|
procedure insertNSRecord(Key : in Rr_Type.WireStringType;
|
|
theRecord : in rr_type.ns_record_type.NSRecordType;
|
|
success : out boolean)
|
|
--# global in out NSRecordTable, NSRecordKeys;
|
|
--# derives NSRecordTable from *, NSRecordKeys, theRecord, Key &
|
|
--# NSRecordKeys from *, Key &
|
|
--# success from NSRecordKeys, Key;
|
|
is
|
|
bucket : rr_type.NumBucketsIndexType;
|
|
Lower_Key : RR_Type.WireStringType;
|
|
begin
|
|
Lower_Key := To_Lower(Key);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Key);
|
|
|
|
success := false;
|
|
for i in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert true;
|
|
if NSRecordKeys(bucket)(i) = rr_type.BlankOwner then
|
|
NSRecordKeys(bucket)(i) := Lower_Key;
|
|
NSRecordTable(bucket)(i) := theRecord;
|
|
success := true;
|
|
end if;
|
|
exit when success;
|
|
end loop;
|
|
END InsertNSRecord;
|
|
|
|
+++ Flow analysis of subprogram insertNSRecord
|
|
performed: no errors found.
|
|
|
|
|
|
procedure insertNSECRecord(Key : in Rr_Type.WireStringType;
|
|
theRecord : in rr_type.nsec_record_type.NSECRecordType;
|
|
success : out boolean)
|
|
--# global in out NSECRecordTable, NSECRecordKeys;
|
|
--# derives NSECRecordTable from *, NSECRecordKeys, theRecord, Key &
|
|
--# NSECRecordKeys from *, Key &
|
|
--# success from NSECRecordKeys, Key;
|
|
is
|
|
bucket : rr_type.NumBucketsIndexType;
|
|
Lower_Key : RR_Type.WireStringType;
|
|
begin
|
|
Lower_Key := To_Lower(Key);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Key);
|
|
|
|
success := false;
|
|
for i in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert true;
|
|
if NSECRecordKeys(bucket)(i) = rr_type.BlankOwner then
|
|
NSECRecordKeys(bucket)(i) := Lower_Key;
|
|
NSECRecordTable(bucket)(i) := theRecord;
|
|
success := true;
|
|
end if;
|
|
exit when success;
|
|
end loop;
|
|
END InsertNSECRecord;
|
|
|
|
+++ Flow analysis of subprogram insertNSECRecord
|
|
performed: no errors found.
|
|
|
|
|
|
procedure insertPTRRecord(Key : in Rr_Type.WireStringType;
|
|
theRecord : in rr_type.PTR_record_type.PTRRecordType;
|
|
success : out boolean)
|
|
--# global in out PTRRecordTable, PTRRecordKeys;
|
|
--# derives PTRRecordTable from *, PTRRecordKeys, theRecord, Key &
|
|
--# PTRRecordKeys from *, Key &
|
|
--# success from PTRRecordKeys, Key;
|
|
is
|
|
bucket : rr_type.NumBucketsIndexType;
|
|
Lower_Key : RR_Type.WireStringType;
|
|
begin
|
|
Lower_Key := To_Lower(Key);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Key);
|
|
|
|
success := false;
|
|
for i in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert true;
|
|
if PTRRecordKeys(bucket)(i) = rr_type.BlankOwner then
|
|
PTRRecordKeys(bucket)(i) := Lower_Key;
|
|
PTRRecordTable(bucket)(i) := theRecord;
|
|
success := true;
|
|
end if;
|
|
exit when success;
|
|
end loop;
|
|
END InsertPTRRecord;
|
|
|
|
+++ Flow analysis of subprogram insertPTRRecord
|
|
performed: no errors found.
|
|
|
|
|
|
procedure InsertRRSIGRecord(Key : in Rr_Type.WireStringType;
|
|
theRecord : in rr_type.rrsig_record_type.rrsigRecordType;
|
|
success : out boolean)
|
|
--# global in out rrsigRecordTable, rrsigRecordKeys;
|
|
--# derives rrsigRecordTable from *, rrsigRecordKeys, theRecord, Key &
|
|
--# rrsigRecordKeys from *, Key &
|
|
--# success from rrsigRecordKeys, Key;
|
|
is
|
|
bucket : rr_type.NumBucketsIndexType;
|
|
Lower_Key : RR_Type.WireStringType;
|
|
begin
|
|
Lower_Key := To_Lower(Key);
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Key);
|
|
|
|
success := false;
|
|
for i in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert true;
|
|
if rrsigRecordKeys(bucket)(i) = rr_type.BlankOwner then
|
|
rrsigRecordKeys(bucket)(i) := Lower_Key;
|
|
rrsigRecordTable(bucket)(i) := theRecord;
|
|
success := true;
|
|
end if;
|
|
exit when success;
|
|
end loop;
|
|
END InsertRRSIGRecord;
|
|
|
|
+++ Flow analysis of subprogram InsertRRSIGRecord
|
|
performed: no errors found.
|
|
|
|
|
|
procedure insertSOARecord(Key : in Rr_Type.WireStringType;
|
|
theRecord : in rr_type.SOA_record_type.SOARecordType;
|
|
success : out boolean)
|
|
--# global in out SOARecordTable, SOARecordKeys;
|
|
--# derives SOARecordTable from *, SOARecordKeys, theRecord, Key &
|
|
--# SOARecordKeys from *, Key &
|
|
--# success from SOARecordKeys, Key;
|
|
is
|
|
Bucket : Rr_Type.NumBucketsIndexType;
|
|
ReturnedSOARecords : Rr_Type.SOA_Record_Type.SOARecordBucketType;
|
|
NumFound : natural;
|
|
Lower_Key : RR_Type.WireStringType;
|
|
begin
|
|
Lower_Key := To_Lower(Key);
|
|
--# accept Flow, 10, ReturnedSOARecords, "only care if there are any";
|
|
--ReturnedSOARecords := Rr_Type.SOA_Record_Type.SOARecordBucketType'(others => rr_type.soa_record_type.BlanksoaRecord);
|
|
--SOA records are special, can only have one per domain. Enforce that here.
|
|
QuerySOARecords(Lower_Key, ReturnedSOARecords, NumFound);
|
|
--# end accept;
|
|
if NumFound > 0 then
|
|
Success := False;
|
|
else
|
|
--queries must be case-insensitive, so hash on Lower case version
|
|
Bucket := Hash(Lower_Key);
|
|
|
|
success := false;
|
|
for i in rr_type.ReturnedRecordsIndexType loop
|
|
--# assert true;
|
|
if SOARecordKeys(bucket)(i) = rr_type.BlankOwner then
|
|
SOARecordKeys(bucket)(i) := Lower_Key;
|
|
SOARecordTable(bucket)(i) := theRecord;
|
|
success := true;
|
|
end if;
|
|
exit when success;
|
|
end loop;
|
|
end if;
|
|
--# accept Flow, 33, ReturnedSOARecords, "only care if there are any";
|
|
END InsertSOARecord;
|
|
|
|
+++ Flow analysis of subprogram InsertSOARecord
|
|
performed: no errors found.
|
|
|
|
|
|
end Dns_Table_Type;
|
|
|
|
end dns_table_pkg;
|
|
|
|
Expected messages marked with the accept annotation
|
|
Type Msg Lines Reason Match
|
|
No. From To No. Line
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 10 only care if there are any 1
|
|
Flow 33 end only care if there are any 1
|
|
|
|
|
|
|
|
|
|
--End of file--------------------------------------------------
|