1010 lines
79 KiB
Plaintext
1010 lines
79 KiB
Plaintext
dns_network.adb:--# hide DNS_Network;
|
|
dns_network.adb: --# global in out Network;
|
|
dns_network.adb: --# derives Network from *;
|
|
dns_network.ads:--# inherit DNS_Types,System;
|
|
dns_network.ads:--# own protected Network : Network_Type;
|
|
dns_network.ads: --# type Network_Type is abstract;
|
|
dns_network.ads: --# global in out Network;
|
|
dns_network.ads: --# derives Network from Network;
|
|
dns_network.ads: --# global in out Network;
|
|
dns_network.ads: --# derives Network from Network;
|
|
dns_network.ads: --# global in out Network;
|
|
dns_network.ads: --# derives Network from * & Socket from Network;
|
|
dns_network.ads: --# global in out Network;
|
|
dns_network.ads: --# derives Network, Packet, Number_Bytes, Failure from Network, Socket;
|
|
dns_network.ads: --# global in out Network;
|
|
dns_network.ads: --# derives Failure,Network from Network, Packet, Number_Bytes, Socket &
|
|
dns_network.ads: --# Packet from Network;
|
|
dns_network.ads: --# pre Integer(Number_Bytes) > DNS_Types.Header_Bits/8;
|
|
dns_network.ads: --# post System.Default_Bit_Order=System.High_Order_First -> Packet = Packet~;
|
|
dns_network.ads: --# global in out Network;
|
|
dns_network.ads: --# derives Network, Packet, Number_Bytes, Reply_Address, Failure from Network;
|
|
dns_network.ads: --# global in out Network;
|
|
dns_network.ads: --# derives Failure,Network from Network, Packet, Number_Bytes, To_Address &
|
|
dns_network.ads: --# Packet from Network;
|
|
dns_network.ads: --# pre Integer(Number_Bytes) > DNS_Types.Header_Bits/8;
|
|
dns_network.ads: --# post System.Default_Bit_Order=System.High_Order_First -> Packet = Packet~;
|
|
dns_network.ads: --# global in out Network;
|
|
dns_network.ads: --# derives Network from *, Socket;
|
|
dns_network.ads: --# hide DNS_Network
|
|
dns_network_receive.ads:--# inherit DNS_Types,DNS_Network;
|
|
dns_network_receive.ads: --# global in out DNS_Network.Network;
|
|
dns_network_receive.ads: --# derives DNS_Network.Network, Packet, Number_Bytes, Failure from DNS_Network.Network, Socket;
|
|
dns_network_receive.ads: --# post (not Failure) -> (Number_Bytes >= DNS_Types.Packet_Length_Range(1+DNS_Types.Header_Bits/8)
|
|
dns_network_receive.ads: --# and Number_Bytes <= DNS_Network.MAX_QUERY_SIZE);
|
|
dns_network_receive.ads: --# global in out DNS_Network.Network;
|
|
dns_network_receive.ads: --# derives DNS_Network.Network, Packet, Number_Bytes, Reply_Address, Failure from DNS_Network.Network;
|
|
dns_network_receive.ads: --# post (not Failure) -> (Number_Bytes >= DNS_Types.Packet_Length_Range(1+DNS_Types.Header_Bits/8)
|
|
dns_network_receive.ads: --# and Number_Bytes <= DNS_Network.MAX_QUERY_SIZE);
|
|
dns_table_pkg.adb: --# assert true;
|
|
dns_table_pkg.adb: --#assert true;
|
|
dns_table_pkg.adb: --# assert val <= (i-1)*Character'Pos(Character'Last)
|
|
dns_table_pkg.adb: --# and (for all Q in rr_type.WireStringTypeIndex =>
|
|
dns_table_pkg.adb: --# (character'pos(domainname(Q))<=255 and
|
|
dns_table_pkg.adb: --# character'pos(domainname(Q))>=0));
|
|
dns_table_pkg.adb: --# global in ARecordTable, ARecordKeys;
|
|
dns_table_pkg.adb: --# derives howMany from ARecordKeys, domainName &
|
|
dns_table_pkg.adb: --# returnedRecords from ARecordKeys, ARecordTable, domainName;
|
|
dns_table_pkg.adb: --# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
dns_table_pkg.adb: --# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
dns_table_pkg.adb: --# end accept;
|
|
dns_table_pkg.adb: --# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
dns_table_pkg.adb: --# global in AAAARecordTable, AAAARecordKeys;
|
|
dns_table_pkg.adb: --# derives howMany from AAAARecordKeys, domainName &
|
|
dns_table_pkg.adb: --# returnedRecords from AAAARecordKeys, AAAARecordTable, domainName;
|
|
dns_table_pkg.adb: --# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
dns_table_pkg.adb: --# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
dns_table_pkg.adb: --# end accept;
|
|
dns_table_pkg.adb: --# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
dns_table_pkg.adb: --# global in CNAMERecordTable, CNAMERecordKeys;
|
|
dns_table_pkg.adb: --# derives howMany from CNAMERecordKeys, domainName &
|
|
dns_table_pkg.adb: --# returnedRecords from CNAMERecordKeys, CNAMERecordTable, domainName;
|
|
dns_table_pkg.adb: --# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
dns_table_pkg.adb: --# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
dns_table_pkg.adb: --# end accept;
|
|
dns_table_pkg.adb: --# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
dns_table_pkg.adb: --# global in DNSKEYRecordTable, DNSKEYRecordKeys;
|
|
dns_table_pkg.adb: --# derives howMany from DNSKEYRecordKeys, domainName &
|
|
dns_table_pkg.adb: --# returnedRecords from DNSKEYRecordKeys, DNSKEYRecordTable, domainName;
|
|
dns_table_pkg.adb: --# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
dns_table_pkg.adb: --# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
dns_table_pkg.adb: --# end accept;
|
|
dns_table_pkg.adb: --# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
dns_table_pkg.adb: --# global in MXRecordTable, MXRecordKeys;
|
|
dns_table_pkg.adb: --# derives howMany from MXRecordKeys, domainName &
|
|
dns_table_pkg.adb: --# returnedRecords from MXRecordKeys, MXRecordTable, domainName;
|
|
dns_table_pkg.adb: --# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
dns_table_pkg.adb: --# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
dns_table_pkg.adb: --# end accept;
|
|
dns_table_pkg.adb: --# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
dns_table_pkg.adb: --# global in NSRecordTable, NSRecordKeys;
|
|
dns_table_pkg.adb: --# derives howMany from NSRecordKeys, domainName &
|
|
dns_table_pkg.adb: --# returnedRecords from NSRecordKeys, NSRecordTable, domainName;
|
|
dns_table_pkg.adb: --# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
dns_table_pkg.adb: --# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
dns_table_pkg.adb: --# end accept;
|
|
dns_table_pkg.adb: --# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
dns_table_pkg.adb: --# global in NSECRecordTable, NSECRecordKeys;
|
|
dns_table_pkg.adb: --# derives howMany from NSECRecordKeys, domainName &
|
|
dns_table_pkg.adb: --# returnedRecords from NSECRecordKeys, NSECRecordTable, domainName;
|
|
dns_table_pkg.adb: --# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
dns_table_pkg.adb: --# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
dns_table_pkg.adb: --# end accept;
|
|
dns_table_pkg.adb: --# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
dns_table_pkg.adb: --# global in PTRRecordTable, PTRRecordKeys;
|
|
dns_table_pkg.adb: --# derives howMany from PTRRecordKeys, domainName &
|
|
dns_table_pkg.adb: --# returnedRecords from PTRRecordKeys, PTRRecordTable, domainName;
|
|
dns_table_pkg.adb: --# assert howMany >= 0 and howMany < ctr
|
|
dns_table_pkg.adb: --# and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
dns_table_pkg.adb: --# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
dns_table_pkg.adb: --# end accept;
|
|
dns_table_pkg.adb: --# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
dns_table_pkg.adb: --# global in RRSIGRecordTable, RRSIGRecordKeys;
|
|
dns_table_pkg.adb: --# derives howMany from RRSIGRecordKeys, domainName &
|
|
dns_table_pkg.adb: --# returnedRecords from RRSIGRecordKeys, RRSIGRecordTable, domainName;
|
|
dns_table_pkg.adb: --# assert howMany >= 0 and howMany < ctr and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
dns_table_pkg.adb: --# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
dns_table_pkg.adb: --# end accept;
|
|
dns_table_pkg.adb: --# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
dns_table_pkg.adb: --# global in SOARecordTable, SOARecordKeys;
|
|
dns_table_pkg.adb: --# derives howMany from SOARecordKeys, domainName &
|
|
dns_table_pkg.adb: --# returnedRecords from SOARecordKeys, SOARecordTable, domainName;
|
|
dns_table_pkg.adb: --# assert howMany >= 0 and howMany < ctr
|
|
dns_table_pkg.adb: --# and bucket >= 1 and bucket <= rr_type.NumBuckets;
|
|
dns_table_pkg.adb: --# accept Flow, 23, returnedRecords, "assigning to uninitialized array is OK";
|
|
dns_table_pkg.adb: --# end accept;
|
|
dns_table_pkg.adb: --# accept Flow, 602, returnedRecords, returnedRecords, "fills as much of array as needed";
|
|
dns_table_pkg.adb: --# global in out ARecordTable, ARecordKeys;
|
|
dns_table_pkg.adb: --# derives ARecordTable from *, ARecordKeys, theRecord, Key &
|
|
dns_table_pkg.adb: --# ARecordKeys from *, Key &
|
|
dns_table_pkg.adb: --# success from ARecordKeys, Key;
|
|
dns_table_pkg.adb: --# assert true;
|
|
dns_table_pkg.adb: --# global in out AAAARecordTable, AAAARecordKeys;
|
|
dns_table_pkg.adb: --# derives AAAARecordTable from *, AAAARecordKeys, theRecord, Key &
|
|
dns_table_pkg.adb: --# AAAARecordKeys from *, Key &
|
|
dns_table_pkg.adb: --# success from AAAARecordKeys, Key;
|
|
dns_table_pkg.adb: --# assert true;
|
|
dns_table_pkg.adb: --# global in out CNAMERecordTable, CNAMERecordKeys;
|
|
dns_table_pkg.adb: --# derives CNAMERecordTable from *, CNAMERecordKeys, theRecord, Key &
|
|
dns_table_pkg.adb: --# CNAMERecordKeys from *, Key &
|
|
dns_table_pkg.adb: --# success from CNAMERecordKeys, Key;
|
|
dns_table_pkg.adb: --# assert true;
|
|
dns_table_pkg.adb: --# global in out DNSKEYRecordTable, DNSKEYRecordKeys;
|
|
dns_table_pkg.adb: --# derives DNSKEYRecordTable from *, DNSKEYRecordKeys, theRecord, Key &
|
|
dns_table_pkg.adb: --# DNSKEYRecordKeys from *, Key &
|
|
dns_table_pkg.adb: --# success from DNSKEYRecordKeys, Key;
|
|
dns_table_pkg.adb: --# assert true;
|
|
dns_table_pkg.adb: --# global in out MXRecordTable, MXRecordKeys;
|
|
dns_table_pkg.adb: --# derives MXRecordTable from *, MXRecordKeys, theRecord, Key &
|
|
dns_table_pkg.adb: --# MXRecordKeys from *, Key &
|
|
dns_table_pkg.adb: --# success from MXRecordKeys, Key;
|
|
dns_table_pkg.adb: --# assert true;
|
|
dns_table_pkg.adb: --# global in out NSRecordTable, NSRecordKeys;
|
|
dns_table_pkg.adb: --# derives NSRecordTable from *, NSRecordKeys, theRecord, Key &
|
|
dns_table_pkg.adb: --# NSRecordKeys from *, Key &
|
|
dns_table_pkg.adb: --# success from NSRecordKeys, Key;
|
|
dns_table_pkg.adb: --# assert true;
|
|
dns_table_pkg.adb: --# global in out NSECRecordTable, NSECRecordKeys;
|
|
dns_table_pkg.adb: --# derives NSECRecordTable from *, NSECRecordKeys, theRecord, Key &
|
|
dns_table_pkg.adb: --# NSECRecordKeys from *, Key &
|
|
dns_table_pkg.adb: --# success from NSECRecordKeys, Key;
|
|
dns_table_pkg.adb: --# assert true;
|
|
dns_table_pkg.adb: --# global in out PTRRecordTable, PTRRecordKeys;
|
|
dns_table_pkg.adb: --# derives PTRRecordTable from *, PTRRecordKeys, theRecord, Key &
|
|
dns_table_pkg.adb: --# PTRRecordKeys from *, Key &
|
|
dns_table_pkg.adb: --# success from PTRRecordKeys, Key;
|
|
dns_table_pkg.adb: --# assert true;
|
|
dns_table_pkg.adb: --# global in out rrsigRecordTable, rrsigRecordKeys;
|
|
dns_table_pkg.adb: --# derives rrsigRecordTable from *, rrsigRecordKeys, theRecord, Key &
|
|
dns_table_pkg.adb: --# rrsigRecordKeys from *, Key &
|
|
dns_table_pkg.adb: --# success from rrsigRecordKeys, Key;
|
|
dns_table_pkg.adb: --# assert true;
|
|
dns_table_pkg.adb: --# global in out SOARecordTable, SOARecordKeys;
|
|
dns_table_pkg.adb: --# derives SOARecordTable from *, SOARecordKeys, theRecord, Key &
|
|
dns_table_pkg.adb: --# SOARecordKeys from *, Key &
|
|
dns_table_pkg.adb: --# success from SOARecordKeys, Key;
|
|
dns_table_pkg.adb: --# accept Flow, 10, ReturnedSOARecords, "only care if there are any";
|
|
dns_table_pkg.adb: --# end accept;
|
|
dns_table_pkg.adb: --# assert true;
|
|
dns_table_pkg.adb: --# accept Flow, 33, ReturnedSOARecords, "only care if there are any";
|
|
dns_table_pkg.ads:--# inherit System, Ada.Characters.Handling, unsigned_types, dns_types, rr_type, rr_type.a_record_type, rr_type.aaaa_record_type,
|
|
dns_table_pkg.ads:--# rr_type.cname_record_type, rr_type.dnskey_record_type, rr_type.mx_record_type,
|
|
dns_table_pkg.ads:--# rr_type.ns_record_type, rr_type.nsec_record_type, rr_type.ptr_record_type,
|
|
dns_table_pkg.ads:--# rr_type.rrsig_record_type, rr_type.soa_record_type;
|
|
dns_table_pkg.ads:--# own protected DNS_Table : DNS_Table_Type (priority => 0);
|
|
dns_table_pkg.ads: --# global in out DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives DNS_Table_Type from *, theRecord, Key &
|
|
dns_table_pkg.ads: --# success from DNS_Table_Type, key;
|
|
dns_table_pkg.ads: --# global in out DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives DNS_Table_Type from *, theRecord, Key &
|
|
dns_table_pkg.ads: --# success from DNS_Table_Type, key;
|
|
dns_table_pkg.ads: --# global in out DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives DNS_Table_Type from *, theRecord, Key &
|
|
dns_table_pkg.ads: --# success from DNS_Table_Type, key;
|
|
dns_table_pkg.ads: --# global in out DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives DNS_Table_Type from *, theRecord, Key &
|
|
dns_table_pkg.ads: --# success from DNS_Table_Type, key;
|
|
dns_table_pkg.ads: --# global in out DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives DNS_Table_Type from *, theRecord, Key &
|
|
dns_table_pkg.ads: --# success from DNS_Table_Type, key;
|
|
dns_table_pkg.ads: --# global in out DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives DNS_Table_Type from *, theRecord, Key &
|
|
dns_table_pkg.ads: --# success from DNS_Table_Type, key;
|
|
dns_table_pkg.ads: --# global in out DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives DNS_Table_Type from *, theRecord, Key &
|
|
dns_table_pkg.ads: --# success from DNS_Table_Type, key;
|
|
dns_table_pkg.ads: --# global in out DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives DNS_Table_Type from *, theRecord, Key &
|
|
dns_table_pkg.ads: --# success from DNS_Table_Type, key;
|
|
dns_table_pkg.ads: --# global in out DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives DNS_Table_Type from *, theRecord, Key &
|
|
dns_table_pkg.ads: --# success from DNS_Table_Type, key;
|
|
dns_table_pkg.ads: --# global in out DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives DNS_Table_Type from *, theRecord, Key &
|
|
dns_table_pkg.ads: --# success from DNS_Table_Type, key;
|
|
dns_table_pkg.ads: --# global in DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives returnedRecords from DNS_Table_Type, domainName &
|
|
dns_table_pkg.ads: --# howMany from DNS_Table_Type, domainName;
|
|
dns_table_pkg.ads: --# global in DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives returnedRecords from DNS_Table_Type, domainName &
|
|
dns_table_pkg.ads: --# howMany from DNS_Table_Type, domainName;
|
|
dns_table_pkg.ads: --# global in DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives returnedRecords from DNS_Table_Type, domainName &
|
|
dns_table_pkg.ads: --# howMany from DNS_Table_Type, domainName;
|
|
dns_table_pkg.ads: --# global in DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives returnedRecords, howMany from DNS_Table_Type, domainName;
|
|
dns_table_pkg.ads: --# global in DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives returnedRecords from DNS_Table_Type, domainName &
|
|
dns_table_pkg.ads: --# howMany from DNS_Table_Type, domainName;
|
|
dns_table_pkg.ads: --# global in DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives returnedRecords from DNS_Table_Type, domainName &
|
|
dns_table_pkg.ads: --# howMany from DNS_Table_Type, domainName;
|
|
dns_table_pkg.ads: --# global in DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives returnedRecords from DNS_Table_Type, domainName &
|
|
dns_table_pkg.ads: --# howMany from DNS_Table_Type, domainName;
|
|
dns_table_pkg.ads: --# global in DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives returnedRecords from DNS_Table_Type, domainName &
|
|
dns_table_pkg.ads: --# howMany from DNS_Table_Type, domainName;
|
|
dns_table_pkg.ads: --# global in DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives returnedRecords, howMany from DNS_Table_Type, domainName;
|
|
dns_table_pkg.ads: --# global in DNS_Table_Type;
|
|
dns_table_pkg.ads: --# derives returnedRecords from DNS_Table_Type, domainName &
|
|
dns_table_pkg.ads: --# howMany from DNS_Table_Type, domainName;
|
|
dns_types.adb: --# hide Byte_Swap_US
|
|
dns_types.ads:--# inherit System;
|
|
dns_types.ads: --# assert Packet_Length_Range'Base is Integer;
|
|
dns_types.ads: --# assert Packet_Bytes_Range'Base is Integer;
|
|
dns_types.ads: --# accept Warning, 2, "representation clause ok";
|
|
dns_types.ads: --# end accept;
|
|
dns_types.ads: --# assert Unsigned_Short'Base is Integer;
|
|
dns_types.ads: --# accept Warning, 2, "representation clause ok";
|
|
dns_types.ads: --# end accept;
|
|
dns_types.ads: --# accept Warning, 2, "representation clause ok";
|
|
dns_types.ads: --# end accept;
|
|
dns_types.ads: --# accept Warning, 2, "representation clause ok";
|
|
dns_types.ads: --# end accept;
|
|
dns_types.ads: --# accept Warning, 2, "representation clause ok";
|
|
dns_types.ads: --# end accept;
|
|
dns_types.ads: --# accept Warning, 3, "Inline ok";
|
|
dns_types.ads: --# end accept;
|
|
dns_types.ads: --# derives H from H;
|
|
dns_types.ads: --# post H = H~[MessageID => Byte_Swap_US(H~.MessageID);
|
|
dns_types.ads: --# QDCount => Byte_Swap_US(H~.QDCount);
|
|
dns_types.ads: --# ANCount => Byte_Swap_US(H~.ANCount);
|
|
dns_types.ads: --# NSCount => Byte_Swap_US(H~.NSCount);
|
|
dns_types.ads: --# ARCount => Byte_Swap_US(H~.ARCount)];
|
|
dns_types.ads: --# accept Warning, 2, "representation clause ok";
|
|
dns_types.ads: --# end accept;
|
|
dns_types.ads: --# accept Warning, 2, "representation clause ok";
|
|
dns_types.ads: --# end accept;
|
|
error_msgs.adb:--# hide error_msgs
|
|
error_msgs.ads:--# inherit rr_type, unsigned_types, Rr_Type.Dnskey_Record_Type;
|
|
error_msgs.ads: --# derives null from currentLine, length, lineCount;
|
|
error_msgs.ads: --# derives null from currentLine, length, lineCount;
|
|
error_msgs.ads: --# derives null from currentLine, length, lineCount;
|
|
error_msgs.ads: --# derives null from currentLine, length, lineCount;
|
|
error_msgs.ads: --# derives null from currentLine, length, lineCount;
|
|
error_msgs.ads: --# derives null from currentLine, length, lineCount;
|
|
error_msgs.ads: --# derives null from currentLine, length, lineCount;
|
|
error_msgs.ads: --# derives null from currentLine, begIdx, endIdx;
|
|
error_msgs.ads: --# derives null from currentLine, begIdx, endIdx;
|
|
error_msgs.ads: --# derives null from currentLine, lineCount;
|
|
error_msgs.ads: --# derives null from currentLine, length, lineCount;
|
|
error_msgs.ads: --# derives ;
|
|
multitask_process_dns_request.adb: --# hide Multitask_Process_Dns_Request;
|
|
multitask_process_dns_request.adb: --# global in out Protected_SPARK_IO_05.SPARK_IO_PO;
|
|
multitask_process_dns_request.adb: --# in out DNS_Network.Network;
|
|
multitask_process_dns_request.adb: --# derives DNS_Network.Network from DNS_Network.Network, Reply_Socket &
|
|
multitask_process_dns_request.adb: --# Protected_SPARK_IO_05.SPARK_IO_PO from *, DNS_Network.Network, Reply_Socket;
|
|
multitask_process_dns_request.ads:--# inherit DNS_types, DNS_Table_Pkg, DNS_Network, System, Protected_SPARK_IO_05, Process_DNS_Request;
|
|
multitask_process_dns_request.ads: --# global in out Protected_SPARK_IO_05.SPARK_IO_PO;
|
|
multitask_process_dns_request.ads: --# in DNS_Table_Pkg.DNS_Table;
|
|
multitask_process_dns_request.ads: --# in out DNS_Network.Network;
|
|
multitask_process_dns_request.ads: --# derives DNS_Network.Network from DNS_Network.Network, Reply_Socket,
|
|
multitask_process_dns_request.ads: --# DNS_Table_Pkg.DNS_Table &
|
|
multitask_process_dns_request.ads: --# Protected_SPARK_IO_05.SPARK_IO_PO from *, DNS_Network.Network, Reply_Socket,
|
|
multitask_process_dns_request.ads: --# DNS_Table_Pkg.DNS_Table;
|
|
non_spark_stuff.adb: --# hide non_spark_stuff
|
|
non_spark_stuff.ads:--# inherit unsigned_types;
|
|
parser_utilities.adb: --# pre begIdx <= endIdx;
|
|
parser_utilities.adb: --# assert true;
|
|
parser_utilities.adb: --# assert begIdx >= 1 and begIdx < length;
|
|
parser_utilities.adb: --# assert begIdx >= 1 and begIdx <= length and
|
|
parser_utilities.adb: --# endIdx >= begIdx and endIdx < length;
|
|
parser_utilities.adb: --# assert begIdx >= 1 and begIdx <= length and
|
|
parser_utilities.adb: --# endIdx >= begIdx and endIdx <= length;
|
|
parser_utilities.adb: --# assert begIdx < length;
|
|
parser_utilities.adb: --# assert begIdx <= length and
|
|
parser_utilities.adb: --# endIdx >= begIdx and endIdx < length;
|
|
parser_utilities.adb: --# assert begIdx >= 1 and begIdx <= length and endIdx >= begIdx and endIdx <= length
|
|
parser_utilities.adb: --# and EndIdx = EndIdx%
|
|
parser_utilities.adb: --# and ((ContainsOnlyNumbers = true) ->
|
|
parser_utilities.adb: --# (for all J in integer range BegIdx..I => (S(J) >= '0' AND S(J) <= '9')));
|
|
parser_utilities.adb: --# assert begIdx >= 1 and tmpVal <= unsigned_types.MAX_8BIT_VAL;
|
|
parser_utilities.adb: --# assert begIdx >= 1 and tmpVal <= unsigned_types.MAX_16BIT_VAL;
|
|
parser_utilities.adb: --# assert begIdx >= 1 and tmpVal >= 0 and tmpVal <= unsigned_types.MAX_32BIT_VAL;
|
|
parser_utilities.adb: --# pre isMult(Char);
|
|
parser_utilities.adb: --# return Value => Value >= 0 and Value <= 60*60*24*7;
|
|
parser_utilities.adb: --#assert Blob >= 0 and Blob <= Rr_Type.SOA_Record_Type.MAX_TIME_VAL
|
|
parser_utilities.adb: --#and Tmp >= 0 and Tmp <= Rr_Type.SOA_Record_Type.MAX_TIME_VAL;
|
|
parser_utilities.adb: --#assert year <= rr_type.rrsig_record_type.MAX_YEAR and month <= 12 and day <= 31
|
|
parser_utilities.adb: --# and hour <= 23 and minute <= 59 and second <= 59;
|
|
parser_utilities.adb: --# assert begIdx >= 1 and begIdx < length;
|
|
parser_utilities.adb: --# assert begIdx >= 1 and begIdx <= endIdx and endIdx >= 1 and endIdx < length;
|
|
parser_utilities.adb: --# assert BegIdx = begIdx% and EndIdx = EndIdx% and I >= BegIdx and I <= EndIdx
|
|
parser_utilities.adb: --# and BegIdx >= 1
|
|
parser_utilities.adb: --# and RRSIG_Rec.SignatureLength + ((EndIdx-BegIdx)+1) <= Rr_Type.RRSIG_Record_Type.MaxRRSigLength;
|
|
parser_utilities.adb: --# assert begIdx >= 1 and begIdx < length;
|
|
parser_utilities.adb: --# assert begIdx >= 1 and begIdx <= endIdx and endIdx >= 1 and endIdx < length;
|
|
parser_utilities.adb: --# assert BegIdx = begIdx% and EndIdx = EndIdx% and I >= BegIdx and I <= EndIdx
|
|
parser_utilities.adb: --# and BegIdx >= 1
|
|
parser_utilities.adb: --# and DNSKEY_Rec.KeyLength + ((EndIdx-BegIdx)+1) <= Rr_Type.Dnskey_Record_Type.MaxDNSKeyLength;
|
|
parser_utilities.adb: --# assert true;
|
|
parser_utilities.adb: --# assert ctr < endIdx and numSeparators <= REQ_NUM_SEPARATORS and numDigitsInField <= MAX_DIGITS_IN_FIELD;
|
|
parser_utilities.adb: --# assert ctr < endIdx and numSeparators <= REQ_NUM_SEPARATORS and numDigitsInByte <= MAX_DIGITS_PER_BYTE;
|
|
parser_utilities.ads:--# inherit dns_types, Ada.Characters.Latin_1, Ada.Characters.Handling, error_msgs, rr_type, rr_type.a_record_type,
|
|
parser_utilities.ads:--# rr_type.aaaa_record_type, rr_type.dnskey_record_type, rr_type.rrsig_Record_Type,
|
|
parser_utilities.ads:--# rr_type.soa_record_type, unsigned_types, non_spark_stuff;
|
|
parser_utilities.ads: --# derives target, success from target, origin, success
|
|
parser_utilities.ads: --# & null from currentLine, lastPos, lineCount;
|
|
parser_utilities.ads: --# derives success from name, success;
|
|
parser_utilities.ads: --# derives T from s, length;
|
|
parser_utilities.ads: --# derives begIdx, endIdx, T from s, length, begIdx;
|
|
parser_utilities.ads: --# pre begIdx <= length;
|
|
parser_utilities.ads: --# post begIdx <= endIdx and begIdx <= length and endIdx <= length
|
|
parser_utilities.ads: --# and ((T = rr_type.Number) ->
|
|
parser_utilities.ads: --# (for all I in integer range begIdx..endIdx => (S(I) >= '0' and S(I) <= '9')));
|
|
parser_utilities.ads: --# derives value from zoneFileLine, begIdx, endIdx & success from zoneFileLine, begIdx, endIdx, success;
|
|
parser_utilities.ads: --# pre for all I in integer range BegIdx..EndIdx => (ZoneFileLine(I) >= '0' and ZoneFileLine(I) <= '9');
|
|
parser_utilities.ads: --# derives value from zoneFileLine, begIdx, endIdx & success from zoneFileLine, begIdx, endIdx, success;
|
|
parser_utilities.ads: --# pre for all I in integer range BegIdx..EndIdx => (ZoneFileLine(I) >= '0' and ZoneFileLine(I) <= '9');
|
|
parser_utilities.ads: --# derives value from zoneFileLine, begIdx, endIdx & success from zoneFileLine, begIdx, endIdx, success;
|
|
parser_utilities.ads: --# pre for all I in integer range BegIdx..EndIdx => (ZoneFileLine(I) >= '0' and ZoneFileLine(I) <= '9');
|
|
parser_utilities.ads: --# derives retVal,success from S, begIdx, endIdx, success;
|
|
parser_utilities.ads: --# derives timeVal from timeString & success from timeString, success;
|
|
parser_utilities.ads: --# pre for all I in Rr_Type.Rrsig_Record_Type.TimeStringTypeIndex => (timeString(I) >= '0' and timeString(I) <= '9');
|
|
parser_utilities.ads: --# derives RRSIG_Rec from RRSIG_Rec, S, Length & AllDone from S, Length
|
|
parser_utilities.ads: --# & Success from RRSIG_Rec, S, Length, Success;
|
|
parser_utilities.ads: --# derives DNSKEY_Rec from DNSKEY_Rec, S, Length & Success from DNSKEY_Rec, S, Length, Success;
|
|
parser_utilities.ads: --# pre begIdx <= endIdx;
|
|
process_dns_request.adb: --# assert Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-6)-DNS_Types.Packet_Bytes_Range(Current_Name_Length) and
|
|
process_dns_request.adb: --# i>=RR_Type.WireStringTypeIndex'First and i<= RR_Type.WireStringTypeIndex'Last;
|
|
process_dns_request.adb: --# assert Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-6)-DNS_Types.Packet_Bytes_Range(Current_Name_Length) and
|
|
process_dns_request.adb: --# i>=RR_Type.WireStringTypeIndex'First and i<= RR_Type.WireStringTypeIndex'Last;
|
|
process_dns_request.adb: --# assert Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-8)-DNS_Types.Packet_Bytes_Range(Current_Name_Length) and
|
|
process_dns_request.adb: --# i>=RR_Type.WireStringTypeIndex'First and i<= RR_Type.WireStringTypeIndex'Last;
|
|
process_dns_request.adb: --# assert Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-20)-
|
|
process_dns_request.adb: --# DNS_Types.Packet_Bytes_Range(Mailbox_Name_Length+Nameserver_Name_Length) and
|
|
process_dns_request.adb: --# i>=RR_Type.WireStringTypeIndex'First and i<= RR_Type.WireStringTypeIndex'Last;
|
|
process_dns_request.adb: --# assert Current_Byte>=1 and Current_Byte <= (DNS_Types.Packet_Bytes_Range'Last-20)-
|
|
process_dns_request.adb: --# DNS_Types.Packet_Bytes_Range(Mailbox_Name_Length) and
|
|
process_dns_request.adb: --# i>=RR_Type.WireStringTypeIndex'First and i<= RR_Type.WireStringTypeIndex'Last;
|
|
process_dns_request.adb: --# assert I>=RR_Type.WireStringType'First and I < RR_Type.WireStringType'Last and
|
|
process_dns_request.adb: --# Byte >= DNS_Types.Packet_Bytes_Range'First and Integer(Byte) <= Integer(Input_Bytes-5);
|
|
process_dns_request.adb: --# accept Warning, 12, type_To_Natural, "unchecked conversions ok";
|
|
process_dns_request.adb: --# end accept;
|
|
process_dns_request.adb: --# accept Warning, 12, To_Type, "unchecked conversions ok";
|
|
process_dns_request.adb: --# end accept;
|
|
process_dns_request.adb: --# accept Warning, 12, class_To_Natural, "unchecked conversions ok";
|
|
process_dns_request.adb: --# end accept;
|
|
process_dns_request.adb: --# accept Warning, 12, To_Class, "unchecked conversions ok";
|
|
process_dns_request.adb: --# end accept;
|
|
process_dns_request.adb: --# assert Response_Counter >=1 and Response_Counter <= NumFound
|
|
process_dns_request.adb: --# and Answer_Count = Answer_Count~
|
|
process_dns_request.adb: --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords)
|
|
process_dns_request.adb: --# and Current_Byte = Start_Byte +
|
|
process_dns_request.adb: --# DNS_Types.Packet_Bytes_Range(28*(Response_Counter-1))
|
|
process_dns_request.adb: --# and Integer(Current_Byte) < DNS_Types.Packet_Size-(28+DNS_Types.Header_Bits/8)
|
|
process_dns_request.adb: --# and numfound <= rr_type.MaxNumRecords ;
|
|
process_dns_request.adb: --# assert Response_Counter >=1 and Response_Counter <= NumFound
|
|
process_dns_request.adb: --# and Integer(Start_Byte) <= DNS_Types.Packet_Size
|
|
process_dns_request.adb: --# and Answer_Count = Answer_Count~
|
|
process_dns_request.adb: --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords)
|
|
process_dns_request.adb: --# and Current_Byte = Start_Byte +
|
|
process_dns_request.adb: --# DNS_Types.Packet_Bytes_Range(16*(Response_Counter-1))
|
|
process_dns_request.adb: --# and Integer(Current_Byte) < DNS_Types.Packet_Size-(16+DNS_Types.Header_Bits/8)
|
|
process_dns_request.adb: --# and numfound <= rr_type.MaxNumRecords ;
|
|
process_dns_request.adb: --# assert Response_Counter >=1 and Response_Counter <= Num_Found
|
|
process_dns_request.adb: --# and current_name_length >=1 and current_name_length<=rr_type.WireStringTypeIndex'last
|
|
process_dns_request.adb: --# and Num_Found <= rr_type.MaxNumRecords
|
|
process_dns_request.adb: --# and Integer(Start_Byte) <= DNS_Types.Packet_Size
|
|
process_dns_request.adb: --# and Answer_Count = Answer_Count~
|
|
process_dns_request.adb: --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords)
|
|
process_dns_request.adb: --# and Integer(Current_Byte) < (DNS_Types.Packet_Size-(12+DNS_Types.Header_Bits/8))-
|
|
process_dns_request.adb: --# (Current_Name_Length)
|
|
process_dns_request.adb: --# and Current_Byte >= 0;
|
|
process_dns_request.adb: --# assert Response_Counter >=1 and Response_Counter <= Num_Found
|
|
process_dns_request.adb: --# and current_name_length >=1 and current_name_length<=rr_type.WireStringTypeIndex'last
|
|
process_dns_request.adb: --# and Num_Found <= rr_type.MaxNumRecords
|
|
process_dns_request.adb: --# and Integer(Start_Byte) <= DNS_Types.Packet_Size
|
|
process_dns_request.adb: --# and Answer_Count = Answer_Count~
|
|
process_dns_request.adb: --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords)
|
|
process_dns_request.adb: --# and Integer(Current_Byte) < (DNS_Types.Packet_Size-(12+DNS_Types.Header_Bits/8))-
|
|
process_dns_request.adb: --# (Current_Name_Length)
|
|
process_dns_request.adb: --# and Current_Byte >= 0;
|
|
process_dns_request.adb: --# assert Response_Counter >=1 and Response_Counter <= Num_Found
|
|
process_dns_request.adb: --# and current_name_length >=1 and current_name_length<=rr_type.WireStringTypeIndex'last
|
|
process_dns_request.adb: --# and Num_Found <= rr_type.MaxNumRecords
|
|
process_dns_request.adb: --# and Integer(Start_Byte) <= DNS_Types.Packet_Size
|
|
process_dns_request.adb: --# and Answer_Count = Answer_Count~
|
|
process_dns_request.adb: --# and Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords)
|
|
process_dns_request.adb: --# and Integer(Current_Byte) < (DNS_Types.Packet_Size-(14+DNS_Types.Header_Bits/8))-
|
|
process_dns_request.adb: --# (Current_Name_Length)
|
|
process_dns_request.adb: --# and Current_Byte >= 0;
|
|
process_dns_request.adb: --# assert I<RR_Type.WireStringTypeIndex'Last and
|
|
process_dns_request.adb: --# I<=Name_Length and
|
|
process_dns_request.adb: --# Output_Packet.Header.ANCount = 0 and
|
|
process_dns_request.adb: --# Current_Byte >= Start_Byte and
|
|
process_dns_request.adb: --# Integer(Current_Byte)+DNS_Types.Header_Bits/8<DNS_Types.Packet_Size;
|
|
process_dns_request.adb: --# assert I+Zone_Length<=RR_Type.WireStringTypeIndex'Last and I>=1 and
|
|
process_dns_request.adb: --# zone_length = natural(character'pos(domainname(domainname'first))+1);
|
|
process_dns_request.adb: --# assert Answer_Count=0 and Amount_Trimmed>=0 and Amount_Trimmed<RR_Type.WireStringType'Last
|
|
process_dns_request.adb: --# and Output_Bytes <= DNS_Types.Packet_Length_Range'Last
|
|
process_dns_request.adb: --# and Current_Qname_Location <= DNS_Types.QNAME_PTR_RANGE(Output_Bytes);
|
|
process_dns_request.adb: --# accept Flow, 10, Output_Packet.Header.QR,
|
|
process_dns_request.adb: --# "The rest of the header fields retain their newly assigned values";
|
|
process_dns_request.adb: --# accept Flow, 10, Output_Packet.Header.ANCOUNT,
|
|
process_dns_request.adb: --# "The rest of the header fields retain their newly assigned values";
|
|
process_dns_request.adb: --# accept Flow, 10, Output_Packet.Header.AA,
|
|
process_dns_request.adb: --# "The rest of the header fields retain their newly assigned values";
|
|
process_dns_request.adb: --# end accept;
|
|
process_dns_request.adb: --# end accept;
|
|
process_dns_request.adb: --# end accept;
|
|
process_dns_request.adb: --# assert Integer(Input_Bytes) >=DNS_Types.Header_Bits/8+1
|
|
process_dns_request.adb: --# and Qname_Location >=0 and Qname_Location < 16384
|
|
process_dns_request.adb: --# and Integer(Input_Bytes) < 312;
|
|
process_dns_request.adb: --# assert Integer(Input_Bytes) >=DNS_Types.Header_Bits/8
|
|
process_dns_request.adb: --# and Qname_Location >=0 and Qname_Location < 16384
|
|
process_dns_request.adb: --# and Integer(Input_Bytes) < 312
|
|
process_dns_request.adb: --# and Start_Byte <= DNS_Types.Packet_Bytes_Range(Input_Bytes) and Start_Byte >= 4;
|
|
process_dns_request.adb:--# accept Flow, 10, MX_Replies, "not needed for ANY query";
|
|
process_dns_request.adb:--# accept Flow, 10, Qname_Locations, "not needed for ANY query";
|
|
process_dns_request.adb:--# accept Flow, 10, NumFound, "not needed for any query";
|
|
process_dns_request.adb:--# end accept;
|
|
process_dns_request.adb:--# end accept;
|
|
process_dns_request.adb:--# end accept;
|
|
process_dns_request.adb:--# accept Flow, 10, NS_Replies, "not needed for ANY query";
|
|
process_dns_request.adb:--# accept Flow, 10, Qname_Locations, "not needed for ANY query";
|
|
process_dns_request.adb:--# accept Flow, 10, NumFound, "not needed for any query";
|
|
process_dns_request.adb:--# end accept;
|
|
process_dns_request.adb:--# end accept;
|
|
process_dns_request.adb:--# end accept;
|
|
process_dns_request.adb: --# assert Counter >= 1 and Counter<=NumFound and
|
|
process_dns_request.adb: --# Answer_Count >=0 and Answer_Count <= 65535 and
|
|
process_dns_request.adb: --# Additional_Count >= 0 and
|
|
process_dns_request.adb: --# (for all Z in RR_Type.ReturnedRecordsIndexType =>
|
|
process_dns_request.adb: --# (Qname_Locations(Z) >= 0 and Qname_Locations(Z) < 16384)) and
|
|
process_dns_request.adb: --# Qname_Location >=0 and Qname_Location <= 16383 and
|
|
process_dns_request.adb: --# Additional_Count < DNS_Types.Unsigned_Short'Last-DNS_Types.Unsigned_Short(
|
|
process_dns_request.adb: --# 2*Rr_Type.MaxNumRecords) and
|
|
process_dns_request.adb: --# NumFound >= 0 and NumFound <= rr_type.MaxNumRecords and
|
|
process_dns_request.adb: --# Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and
|
|
process_dns_request.adb: --# Integer(Output_Bytes) <= DNS_Types.Packet_Size;
|
|
process_dns_request.adb: --# assert Counter >= 1 and Counter<=NumFound and
|
|
process_dns_request.adb: --# (for all Z in RR_Type.ReturnedRecordsIndexType =>
|
|
process_dns_request.adb: --# (Qname_Locations(Z) >= 0 and Qname_Locations(Z) < 16384)) and
|
|
process_dns_request.adb: --# Qname_Location >=0 and Qname_Location <= 16383 and
|
|
process_dns_request.adb: --# Answer_Count >=0 and Answer_Count <= 65535 and
|
|
process_dns_request.adb: --# Additional_Count >= 0 and
|
|
process_dns_request.adb: --# Additional_Count < DNS_Types.Unsigned_Short'Last-DNS_Types.Unsigned_Short(
|
|
process_dns_request.adb: --# 2*Rr_Type.MaxNumRecords) and
|
|
process_dns_request.adb: --# NumFound >= 0 and NumFound <= rr_type.MaxNumRecords and
|
|
process_dns_request.adb: --# Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and
|
|
process_dns_request.adb: --# Integer(Output_Bytes) <= DNS_Types.Packet_Size;
|
|
process_dns_request.adb: --# assert
|
|
process_dns_request.adb: --# Answer_Count >=0 and Answer_Count <= 65535 and
|
|
process_dns_request.adb: --# Qname_Location >=0 and Qname_Location < 16384 and
|
|
process_dns_request.adb: --# Additional_Count >= 0 and
|
|
process_dns_request.adb: --# NumFound >= 0 and NumFound <= rr_type.MaxNumRecords and
|
|
process_dns_request.adb: --# Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and
|
|
process_dns_request.adb: --# Integer(Output_Bytes) <= DNS_Types.Packet_Size;
|
|
process_dns_request.adb: --# assert
|
|
process_dns_request.adb: --# Answer_Count >=0 and Answer_Count <= 65535 and
|
|
process_dns_request.adb: --# Qname_Location >=0 and Qname_Location < 16384 and
|
|
process_dns_request.adb: --# Additional_Count >= 0 and
|
|
process_dns_request.adb: --# NumFound >= 0 and NumFound <= rr_type.MaxNumRecords and
|
|
process_dns_request.adb: --# Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and
|
|
process_dns_request.adb: --# Integer(Max_Transmit) <= DNS_Types.Packet_Size and Max_Transmit >= DNS_Types.UDP_Max_Size and
|
|
process_dns_request.adb: --# Integer(Output_Bytes) <= DNS_Types.Packet_Size;
|
|
process_dns_request.adb: --# accept Flow, 23, Output_Packet.Rest, "init not needed";
|
|
process_dns_request.adb: --# accept Flow, 10, Max_Transmit, "only needed for UDP";
|
|
process_dns_request.adb: --# end accept;
|
|
process_dns_request.adb: --# end accept;
|
|
process_dns_request.adb: --# accept Flow, 22,
|
|
process_dns_request.adb: --# "allow use of static expression for portability across platforms";
|
|
process_dns_request.adb: --# end accept;
|
|
process_dns_request.adb: --# accept Flow, 602, DNS_Network.Network, Output_Packet.Rest, "initialization is unneeded";
|
|
process_dns_request.adb: --# accept Flow, 602, Protected_SPARK_IO_05.SPARK_IO_PO, Output_Packet.Rest, "initialization is unneeded";
|
|
process_dns_request.adb: --# accept Flow, 33, Max_Transmit, "Max_Transmit only for UDP";
|
|
process_dns_request.ads:--# inherit DNS_types, DNS_Network, DNS_Network_Receive, System, Protected_SPARK_IO_05,
|
|
process_dns_request.ads:--# RR_Type, RR_Type.a_record_type, RR_Type.aaaa_record_type,
|
|
process_dns_request.ads:--# RR_Type.cname_record_type, RR_Type.ns_record_type,
|
|
process_dns_request.ads:--# RR_type.mx_record_type, RR_Type.ptr_record_type,
|
|
process_dns_request.ads:--# RR_type.soa_record_type,
|
|
process_dns_request.ads:--# DNS_Table_Pkg, Unsigned_Types, ada.Unchecked_Conversion;
|
|
process_dns_request.ads: --# global in out Protected_SPARK_IO_05.SPARK_IO_PO;
|
|
process_dns_request.ads: --# in out DNS_Network.Network;
|
|
process_dns_request.ads: --# in DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# derives DNS_Network.Network from DNS_Table_Pkg.DNS_Table, DNS_Network.Network, Reply_Socket &
|
|
process_dns_request.ads: --# Protected_SPARK_IO_05.SPARK_IO_PO from *, DNS_Table_Pkg.DNS_Table, DNS_Network.Network, Reply_Socket;
|
|
process_dns_request.ads: --# global in DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# in out Protected_SPARK_IO_05.SPARK_IO_PO;
|
|
process_dns_request.ads: --# derives Output_Packet from *, DNS_Table_Pkg.DNS_Table, Input_Packet, Input_Bytes &
|
|
process_dns_request.ads: --# Output_Bytes from Output_Packet, Input_Bytes, Input_Packet, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Protected_SPARK_IO_05.SPARK_IO_PO from *, DNS_Table_Pkg.DNS_Table, Input_Packet, Input_Bytes &
|
|
process_dns_request.ads: --# Max_Transmit from DNS_Table_Pkg.DNS_Table, Input_Packet, Input_Bytes;
|
|
process_dns_request.ads: --# pre Integer(Input_Bytes) >=DNS_Types.Header_Bits/8+1
|
|
process_dns_request.ads: --# and Integer(Input_Bytes) < 312;
|
|
process_dns_request.ads: --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Integer(Max_Transmit) <= DNS_Types.Packet_Size and Max_Transmit >= DNS_Types.UDP_Max_Size;
|
|
process_dns_request.ads: --# derives Bytes from *, Start_Byte, Value;
|
|
process_dns_request.ads: --# pre Start_Byte <= DNS_Types.Packet_Bytes_Range'Last-3;
|
|
process_dns_request.ads: --# derives Bytes from *, Start_Byte, Value;
|
|
process_dns_request.ads: --# pre Start_Byte <= DNS_Types.Packet_Bytes_Range'Last-1;
|
|
process_dns_request.ads: --# derives Domainname from Input_Packet,Input_Bytes &
|
|
process_dns_request.ads: --# Query_Type from Input_Packet,Input_Bytes &
|
|
process_dns_request.ads: --# Query_Class from Input_Packet,Input_Bytes &
|
|
process_dns_request.ads: --# End_Byte from Input_Packet,Input_Bytes;
|
|
process_dns_request.ads: --# pre Input_Bytes >=DNS_Types.Header_Bits/8+1 and Input_Bytes < 1000;
|
|
process_dns_request.ads: --# post Integer(End_Byte) <= Integer(Input_Bytes) and End_Byte >= 4;
|
|
process_dns_request.ads: --# derives Bytes from *, Start_Byte, A_Record;
|
|
process_dns_request.ads: --# pre Start_Byte <= DNS_Types.Packet_Bytes_Range'Last-10;
|
|
process_dns_request.ads: --# derives Bytes from *, Start_Byte, AAAA_Record;
|
|
process_dns_request.ads: --# pre Start_Byte <= DNS_Types.Packet_Bytes_Range'Last-22;
|
|
process_dns_request.ads: --# derives Bytes from *, Start_Byte, NS_Record, Current_Name_Length;
|
|
process_dns_request.ads: --# pre Current_Name_Length >= 0 and Current_Name_Length<=RR_Type.WireStringTypeIndex'Last and
|
|
process_dns_request.ads: --# Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-6)-DNS_Types.Packet_Bytes_Range(Current_Name_Length);
|
|
process_dns_request.ads: --# derives Bytes from *, Start_Byte, PTR_Record, Current_Name_Length;
|
|
process_dns_request.ads: --# pre Current_Name_Length >= 0 and Current_Name_Length<=RR_Type.WireStringTypeIndex'Last and
|
|
process_dns_request.ads: --# Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-6)-DNS_Types.Packet_Bytes_Range(Current_Name_Length);
|
|
process_dns_request.ads: --# derives Bytes from *, Start_Byte, MX_Record, Current_Name_Length;
|
|
process_dns_request.ads: --# pre Current_Name_Length >= 0 and Current_Name_Length<=RR_Type.WireStringTypeIndex'Last and
|
|
process_dns_request.ads: --# Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-8)-DNS_Types.Packet_Bytes_Range(Current_Name_Length);
|
|
process_dns_request.ads: --# derives Bytes from *, Start_Byte, SOA_Record, Nameserver_Name_Length, Mailbox_Name_Length;
|
|
process_dns_request.ads: --# pre Nameserver_Name_Length >= 0 and Nameserver_Name_Length<=RR_Type.WireStringTypeIndex'Last and
|
|
process_dns_request.ads: --# Mailbox_Name_Length >= 0 and Mailbox_Name_Length<=RR_Type.WireStringTypeIndex'Last and
|
|
process_dns_request.ads: --# Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-26)-
|
|
process_dns_request.ads: --# DNS_Types.Packet_Bytes_Range(Nameserver_Name_Length+Mailbox_Name_Length);
|
|
process_dns_request.ads: --# derives Output_Packet from *, Start_Byte, Input_Packet, Input_Bytes, Query_End_Byte &
|
|
process_dns_request.ads: --# Output_Bytes from Start_Byte, Input_Packet, Input_Bytes, Query_End_Byte &
|
|
process_dns_request.ads: --# Max_Transmit from Start_Byte, Input_Bytes, Input_Packet, Query_End_Byte &
|
|
process_dns_request.ads: --# DNSSEC from Start_Byte, Input_Bytes, Input_Packet, Query_End_Byte &
|
|
process_dns_request.ads: --# Additional_Count from *, Input_Packet, Start_Byte, Input_Bytes, Query_End_Byte;
|
|
process_dns_request.ads: --# pre Additional_Count < DNS_Types.Unsigned_Short'Last;
|
|
process_dns_request.ads: --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Output_Bytes <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Additional_Count >= Additional_Count~ and Additional_Count <= Additional_Count~+1 and
|
|
process_dns_request.ads: --# Max_Transmit >= DNS_Types.UDP_Max_Size and Max_Transmit <= DNS_Types.Packet_Size;
|
|
process_dns_request.ads: --# global in DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# derives Output_Packet from *, Qname_Location, Start_Byte, Domainname, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Output_Bytes from Domainname, Start_Byte, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Answer_Count from *, Domainname, DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# pre Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords)
|
|
process_dns_request.ads: --# and Integer(Start_Byte) <= DNS_Types.Packet_Size;
|
|
process_dns_request.ads: --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Answer_Count <= Answer_Count~+DNS_Types.Unsigned_Short(rr_type.MaxNumRecords);
|
|
process_dns_request.ads: --# global in DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# derives Output_Packet from *, Qname_Location, Start_Byte, Domainname, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Output_Bytes from Domainname, Qname_Location, Start_Byte, DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size;
|
|
process_dns_request.ads: --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size;
|
|
process_dns_request.ads: --# global in DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# derives Output_Packet from *, Start_Byte, Qname_Location, Domainname, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Output_Bytes from Domainname, Start_Byte, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Answer_Count from *, Domainname, DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords);
|
|
process_dns_request.ads: --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Answer_Count <= Answer_Count~ + DNS_Types.Unsigned_Short(rr_type.MaxNumRecords);
|
|
process_dns_request.ads: --# derives Domainname from Cnames &
|
|
process_dns_request.ads: --# Qname_Location from Start_Byte &
|
|
process_dns_request.ads: --# Output_Packet from *, Qname_Location, Start_Byte, Cnames &
|
|
process_dns_request.ads: --# Output_Bytes from Cnames, Start_Byte;
|
|
process_dns_request.ads: --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size
|
|
process_dns_request.ads: --# and Output_Packet.Header.ANCount = 0;
|
|
process_dns_request.ads: --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Output_Packet.Header.ANCount <= 1;
|
|
process_dns_request.ads: --# derives Output_Packet from * &
|
|
process_dns_request.ads: --# Output_Bytes from Input_Bytes;
|
|
process_dns_request.ads: --# post Output_Bytes = Input_Bytes;
|
|
process_dns_request.ads: --# global in DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# derives Output_Packet from *, Start_Byte, Qname_Location, Domainname, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Output_Bytes from Domainname, Start_Byte, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Num_Found from DNS_Table_Pkg.DNS_Table, Domainname &
|
|
process_dns_request.ads: --# Replies from DNS_Table_Pkg.DNS_Table, Domainname &
|
|
process_dns_request.ads: --# Answer_Count from *, Domainname, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Qname_Locations from Start_Byte, DNS_Table_Pkg.DNS_Table, Domainname ;
|
|
process_dns_request.ads: --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords);
|
|
process_dns_request.ads: --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Answer_Count <= Answer_Count~+DNS_Types.Unsigned_Short(rr_type.MaxNumRecords);
|
|
process_dns_request.ads: --# global in DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# derives Output_Packet from *, Start_Byte, Qname_Location, Domainname, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Output_Bytes from Domainname, Start_Byte, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Answer_Count from *, Domainname, DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords);
|
|
process_dns_request.ads: --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Answer_Count <= Answer_Count~+DNS_Types.Unsigned_Short(rr_type.MaxNumRecords);
|
|
process_dns_request.ads: --# global in DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# derives Output_Packet from *, Start_Byte, Qname_Location, Domainname, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Output_Bytes from Domainname, Start_Byte, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Num_Found from DNS_Table_Pkg.DNS_Table, Domainname &
|
|
process_dns_request.ads: --# Replies from DNS_Table_Pkg.DNS_Table, Domainname &
|
|
process_dns_request.ads: --# Answer_Count from *, Domainname, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Qname_Locations from Start_Byte, DNS_Table_Pkg.DNS_Table, Domainname ;
|
|
process_dns_request.ads: --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords);
|
|
process_dns_request.ads: --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Answer_Count <= Answer_Count~+DNS_Types.Unsigned_Short(rr_type.MaxNumRecords);
|
|
process_dns_request.ads: --# global in DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# derives Output_Packet from *, Start_Byte, Qname_Location, Domainname, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Output_Bytes from Domainname, Start_Byte, DNS_Table_Pkg.DNS_Table &
|
|
process_dns_request.ads: --# Answer_Count from *, Domainname, DNS_Table_Pkg.DNS_Table;
|
|
process_dns_request.ads: --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords);
|
|
process_dns_request.ads: --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
|
|
process_dns_request.ads: --# Answer_Count <= Answer_Count~+DNS_Types.Unsigned_Short(rr_type.MaxNumRecords);
|
|
process_dns_request.ads: --# derives Trimmed_Name from Domainname &
|
|
process_dns_request.ads: --# New_Qname_Location from Domainname, Qname_Location;
|
|
process_dns_request.ads: --# pre Qname_Location <= DNS_Types.QNAME_PTR_RANGE(DNS_Types.Packet_Length_Range'Last);
|
|
process_first_line_of_record.ads:--# inherit Dns_Types, dns_table_pkg, error_msgs, parser_utilities, rr_type.a_record_type,
|
|
process_first_line_of_record.ads:--# rr_type.aaaa_record_type, rr_type.cname_record_type, rr_type.dnskey_record_type, rr_type.mx_record_type,
|
|
process_first_line_of_record.ads:--# rr_type.ns_record_type, rr_type.nsec_record_type, rr_type.ptr_record_type, rr_type.rrsig_record_type,
|
|
process_first_line_of_record.ads:--# spark.ada.text_io, unsigned_types, rr_type, zone_file_parser;
|
|
process_first_line_of_record.ads: --# global in out dns_table_pkg.DNS_Table;
|
|
process_first_line_of_record.ads: --# derives dns_table_pkg.DNS_Table from dns_table_pkg.DNS_Table, currentRecordType,
|
|
process_first_line_of_record.ads: --# currentOrigin, currentOwner, currentTTL, CurrentClass, currentLine, lastPos, success
|
|
process_first_line_of_record.ads: --# & inMultilineRecord, lineInRecordCtr from currentRecordType
|
|
process_first_line_of_record.ads: --# & currentNameServer, currentEmail from currentOrigin, currentRecordType, currentLine, lastPos, success
|
|
process_first_line_of_record.ads: --# & DNSKEY_Rec from currentRecordType, currentLine, lastPos, success
|
|
process_first_line_of_record.ads: --# & RRSIG_Rec from currentRecordType, currentLine, lastPos, success
|
|
process_first_line_of_record.ads: --# & recordSuccessfullyInserted from dns_table_pkg.DNS_Table, currentRecordType,
|
|
process_first_line_of_record.ads: --# currentOrigin, currentOwner, currentLine, lastPos, success
|
|
process_first_line_of_record.ads: --# & success from currentRecordType, currentOrigin, currentLine, lastPos, success
|
|
process_first_line_of_record.ads: --# & null from lineCount;
|
|
process_first_line_of_record.ads: --# pre lastPos >= 1 and lastPos <= rr_type.lineLengthIndex'last;
|
|
protected_spark_io_05.adb: --# hide Protected_SPARK_IO_05;
|
|
protected_spark_io_05.adb: --# hide SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# own protected SPARK_IO_PO : SPARK_IO_05(Priority=>0);
|
|
protected_spark_io_05.ads: --# global in SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives File,
|
|
protected_spark_io_05.ads: --# Status from Form_Of_File,
|
|
protected_spark_io_05.ads: --# Name_Of_File,
|
|
protected_spark_io_05.ads: --# SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# global in SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives File,
|
|
protected_spark_io_05.ads: --# Status from Form_Of_File,
|
|
protected_spark_io_05.ads: --# Name_Length,
|
|
protected_spark_io_05.ads: --# Name_Of_File,
|
|
protected_spark_io_05.ads: --# SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# global in SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives File,
|
|
protected_spark_io_05.ads: --# Status from Form_Of_File,
|
|
protected_spark_io_05.ads: --# Mode_Of_File,
|
|
protected_spark_io_05.ads: --# Name_Of_File,
|
|
protected_spark_io_05.ads: --# SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives File,
|
|
protected_spark_io_05.ads: --# SPARK_IO_05,
|
|
protected_spark_io_05.ads: --# Status from Form_Of_File,
|
|
protected_spark_io_05.ads: --# Mode_Of_File,
|
|
protected_spark_io_05.ads: --# Name_Length,
|
|
protected_spark_io_05.ads: --# Name_Of_File,
|
|
protected_spark_io_05.ads: --# SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05,
|
|
protected_spark_io_05.ads: --# Status from File,
|
|
protected_spark_io_05.ads: --# SPARK_IO_05 &
|
|
protected_spark_io_05.ads: --# File from ;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05,
|
|
protected_spark_io_05.ads: --# Status from File,
|
|
protected_spark_io_05.ads: --# SPARK_IO_05 &
|
|
protected_spark_io_05.ads: --# File from ;
|
|
protected_spark_io_05.ads: --# derives File,
|
|
protected_spark_io_05.ads: --# Status from File,
|
|
protected_spark_io_05.ads: --# Mode_Of_File;
|
|
protected_spark_io_05.ads: --# derives Name_Of_File,
|
|
protected_spark_io_05.ads: --# Stop from File;
|
|
protected_spark_io_05.ads: --# derives Form_Of_File,
|
|
protected_spark_io_05.ads: --# Stop from File;
|
|
protected_spark_io_05.ads: --# global SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05 from *,
|
|
protected_spark_io_05.ads: --# File,
|
|
protected_spark_io_05.ads: --# Spacing;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05 from *,
|
|
protected_spark_io_05.ads: --# File,
|
|
protected_spark_io_05.ads: --# Spacing;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05 from *,
|
|
protected_spark_io_05.ads: --# File;
|
|
protected_spark_io_05.ads: --# global SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# global SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05 from *,
|
|
protected_spark_io_05.ads: --# File,
|
|
protected_spark_io_05.ads: --# Posn;
|
|
protected_spark_io_05.ads: --# pre Mode (File) = In_File;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05 from *,
|
|
protected_spark_io_05.ads: --# File,
|
|
protected_spark_io_05.ads: --# Posn;
|
|
protected_spark_io_05.ads: --# pre Mode( File ) = Out_File or
|
|
protected_spark_io_05.ads: --# Mode (File) = Append_File;
|
|
protected_spark_io_05.ads: --# global SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# pre Mode (File) = In_File;
|
|
protected_spark_io_05.ads: --# global SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# pre Mode (File) = Out_File or
|
|
protected_spark_io_05.ads: --# Mode (File) = Append_File;
|
|
protected_spark_io_05.ads: --# global SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# pre Mode (File) = In_File;
|
|
protected_spark_io_05.ads: --# global SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# pre Mode (File) = Out_File or
|
|
protected_spark_io_05.ads: --# Mode (File) = Append_File;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05,
|
|
protected_spark_io_05.ads: --# Item from File,
|
|
protected_spark_io_05.ads: --# SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05 from *,
|
|
protected_spark_io_05.ads: --# File,
|
|
protected_spark_io_05.ads: --# Item;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05,
|
|
protected_spark_io_05.ads: --# Item,
|
|
protected_spark_io_05.ads: --# Status from File,
|
|
protected_spark_io_05.ads: --# SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05,
|
|
protected_spark_io_05.ads: --# Item,
|
|
protected_spark_io_05.ads: --# Stop from File,
|
|
protected_spark_io_05.ads: --# SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05 from *,
|
|
protected_spark_io_05.ads: --# File,
|
|
protected_spark_io_05.ads: --# Item,
|
|
protected_spark_io_05.ads: --# Stop;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05,
|
|
protected_spark_io_05.ads: --# Item,
|
|
protected_spark_io_05.ads: --# Stop from File,
|
|
protected_spark_io_05.ads: --# SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05 from *,
|
|
protected_spark_io_05.ads: --# File,
|
|
protected_spark_io_05.ads: --# Item,
|
|
protected_spark_io_05.ads: --# Stop;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05,
|
|
protected_spark_io_05.ads: --# Item,
|
|
protected_spark_io_05.ads: --# Read from File,
|
|
protected_spark_io_05.ads: --# SPARK_IO_05,
|
|
protected_spark_io_05.ads: --# Width;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05 from *,
|
|
protected_spark_io_05.ads: --# Base,
|
|
protected_spark_io_05.ads: --# File,
|
|
protected_spark_io_05.ads: --# Item,
|
|
protected_spark_io_05.ads: --# Width;
|
|
protected_spark_io_05.ads: --# derives Item,
|
|
protected_spark_io_05.ads: --# Stop from Source,
|
|
protected_spark_io_05.ads: --# Start_Pos;
|
|
protected_spark_io_05.ads: --# derives Dest from *,
|
|
protected_spark_io_05.ads: --# Base,
|
|
protected_spark_io_05.ads: --# Item,
|
|
protected_spark_io_05.ads: --# Start_Pos;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05,
|
|
protected_spark_io_05.ads: --# Item,
|
|
protected_spark_io_05.ads: --# Read from File,
|
|
protected_spark_io_05.ads: --# SPARK_IO_05,
|
|
protected_spark_io_05.ads: --# Width;
|
|
protected_spark_io_05.ads: --# global in out SPARK_IO_05;
|
|
protected_spark_io_05.ads: --# derives SPARK_IO_05 from *,
|
|
protected_spark_io_05.ads: --# Aft,
|
|
protected_spark_io_05.ads: --# Exp,
|
|
protected_spark_io_05.ads: --# File,
|
|
protected_spark_io_05.ads: --# Fore,
|
|
protected_spark_io_05.ads: --# Item;
|
|
protected_spark_io_05.ads: --# derives Item,
|
|
protected_spark_io_05.ads: --# Stop from Source,
|
|
protected_spark_io_05.ads: --# Start_Pos;
|
|
protected_spark_io_05.ads: --# derives Dest from *,
|
|
protected_spark_io_05.ads: --# Aft,
|
|
protected_spark_io_05.ads: --# Exp,
|
|
protected_spark_io_05.ads: --# Item,
|
|
protected_spark_io_05.ads: --# Start_Pos;
|
|
protected_spark_io_05.ads: --# hide Protected_SPARK_IO_05;
|
|
rr_type-a_record_type.ads:--# inherit Unsigned_Types, rr_type;
|
|
rr_type-aaaa_record_type.ads:--# inherit Unsigned_Types, rr_type;
|
|
rr_type-cname_record_type.ads:--#inherit rr_type;
|
|
rr_type-dnskey_record_type.ads:--#inherit rr_type, unsigned_types;
|
|
rr_type-mx_record_type.ads:--#inherit rr_type, unsigned_types;
|
|
rr_type-ns_record_type.ads:--#inherit rr_type;
|
|
rr_type-nsec_record_type.ads:--#inherit rr_type;
|
|
rr_type-ptr_record_type.ads:--#inherit rr_type;
|
|
rr_type-rrsig_record_type.ads:--#inherit rr_type, unsigned_types, dns_types;
|
|
rr_type-soa_record_type.ads:--#inherit rr_type, unsigned_types;
|
|
rr_type.adb: --# assert Index<MaxDomainNameLength and
|
|
rr_type.adb: --# (for all Q in DomainNameStringTypeIndex range 1..Index+1 => (Name(Q)/= ' '));
|
|
rr_type.adb: --# assert lengthL >= DomainNameStringTypeIndex'First
|
|
rr_type.adb: --# and lengthL < DomainNameStringTypeIndex'Last
|
|
rr_type.adb: --# and ((LengthL + 1) + LengthR) <= MaxDomainNameLength
|
|
rr_type.adb: --# and lengthR% = lengthR;
|
|
rr_type.adb: --# assert Index<MaxDomainNameLength+1 and
|
|
rr_type.adb: --# (for all Q in WireStringTypeIndex range 1..Index => (Name(Q)/=Character'Val(0)));
|
|
rr_type.adb: --# assert true;
|
|
rr_type.adb: --# assert Result >= Position and Result < LineLengthIndex'Last;
|
|
rr_type.adb: --# assert LengthOfDomainName>=1 and LengthOfDomainName<=MaxDomainNameLength;
|
|
rr_type.ads:--# inherit Unsigned_Types;
|
|
rr_type.ads: --# derives Left from Left, Right, Success & Success from Left,Right,Success;
|
|
rr_type.ads: --# return Length => Length=MaxDomainNameLength+1 or (Name(Length)=Character'Val(0) and
|
|
rr_type.ads: --# (for all Q in DomainNameStringTypeIndex range 1..Length-1 => (Name(Q)/=Character'Val(0))));
|
|
rr_type.ads: --# return Length => (Length=1 and (Name(1)=' ' or Name(2)=' ')) or
|
|
rr_type.ads: --# Length=MaxDomainNameLength or (Name(Length+1)=' ' and
|
|
rr_type.ads: --# (for all Q in DomainNameStringTypeIndex range 1..Length => (Name(Q)/= ' ')));
|
|
rr_type.ads: --# pre S'length <= MaxDomainNameLength;
|
|
rr_type.ads: --# pre S'length <= MaxDomainNameLength;
|
|
socket_timeout.adb:--# hide Socket_Timeout;
|
|
socket_timeout.ads: --# derives null from Socket, Milliseconds;
|
|
socket_timeout.ads: --# hide Socket_Timeout;
|
|
socket_timeout_linux.adb:--# hide Socket_Timeout;
|
|
spark_ada_command_line.adb: --# hide SPARK_Ada_Command_Line;
|
|
spark_ada_command_line.ads:--# inherit Spark.Ada.Text_IO;
|
|
spark_ada_command_line.ads:--# own State;
|
|
spark_ada_command_line.ads:--# initializes State;
|
|
spark_ada_command_line.ads: --# global State;
|
|
spark_ada_command_line.ads: --# global State;
|
|
spark_ada_command_line.ads: --# derives file from number, State;
|
|
spark_ada_command_line.ads: --# derives null from Code;
|
|
spark_dns_main.adb:--# inherit udp_dns_package, dns_table_pkg, Tcp_Dns_Package, Protected_SPARK_IO_05,
|
|
spark_dns_main.adb:--# DNS_Network, zone_file_io, Spark_Ada_Command_Line, Spark.Ada.Text_IO;
|
|
spark_dns_main.adb:--# main_program
|
|
spark_dns_main.adb:--# global in out DNS_Network.Network;
|
|
spark_dns_main.adb:--# in out Protected_SPARK_IO_05.SPARK_IO_PO;
|
|
spark_dns_main.adb:--# in out Udp_Dns_Package.Startup_Suspension;
|
|
spark_dns_main.adb:--# in out Tcp_Dns_Package.Startup_Suspension;
|
|
spark_dns_main.adb:--# in out DNS_Table_Pkg.DNS_Table;
|
|
spark_dns_main.adb:--# in Spark_Ada_Command_Line.State;
|
|
spark_dns_main.adb:--# derives DNS_Network.Network from *, tcp_dns_package.startup_suspension,
|
|
spark_dns_main.adb:--# udp_dns_package.startup_suspension, dns_table_pkg.dns_table, spark_ada_command_line.state &
|
|
spark_dns_main.adb:--# Protected_SPARK_IO_05.SPARK_IO_PO from *, DNS_Network.Network, udp_dns_package.startup_suspension,
|
|
spark_dns_main.adb:--# tcp_dns_package.startup_suspension, spark_ada_command_line.state, dns_table_pkg.dns_table &
|
|
spark_dns_main.adb:--# Udp_Dns_Package.Startup_Suspension from * &
|
|
spark_dns_main.adb:--# Tcp_Dns_Package.Startup_Suspension from * &
|
|
spark_dns_main.adb:--# DNS_Table_Pkg.DNS_Table from *, Spark_Ada_Command_Line.State;
|
|
spark_dns_main.adb:--# global out Tcp_Dns_Package.Startup_Suspension;
|
|
spark_dns_main.adb:--# out Udp_Dns_Package.Startup_Suspension;
|
|
spark_dns_main.adb:--# in out DNS_Table_Pkg.DNS_Table;
|
|
spark_dns_main.adb:--# in Spark_Ada_Command_Line.State;
|
|
spark_dns_main.adb:--# derives tcp_dns_package.startup_suspension from &
|
|
spark_dns_main.adb:--# DNS_Table_Pkg.DNS_Table from *, Spark_Ada_Command_Line.State &
|
|
spark_dns_main.adb:--# udp_dns_package.startup_suspension from;
|
|
spark_dns_main.adb:--# declare delay;
|
|
spark_dns_main.adb:--# accept Flow, 10, zoneFile, "done with file after this call";
|
|
spark_dns_main.adb:--# end accept;
|
|
task_limit.adb: --# global in out Task_Count;
|
|
task_limit.adb: --# derives Task_Count from * &
|
|
task_limit.adb: --# Success from Task_Count;
|
|
task_limit.adb: --# pre Task_Count >= 0 and Task_Count <= MAX_TASKS;
|
|
task_limit.adb: --# post Task_Count >= 0 and Task_Count <= MAX_TASKS and
|
|
task_limit.adb: --# (((Task_Count~ = MAX_TASKS) -> ((Task_Count = Task_Count~) and (Success=False))) and
|
|
task_limit.adb: --# ((Task_Count~ < MAX_TASKS) -> ((Task_Count = Task_Count~ + 1) and Success)));
|
|
task_limit.adb: --# global in out Task_Count;
|
|
task_limit.adb: --# derives Task_Count from *;
|
|
task_limit.adb: --# pre Task_Count >= 0 and Task_Count <= MAX_TASKS;
|
|
task_limit.adb: --# post Task_Count >= 0 and Task_Count <= MAX_TASKS and
|
|
task_limit.adb: --# (Task_Count~ > 0 -> (Task_Count = Task_Count~ - 1)) and
|
|
task_limit.adb: --# (Task_Count~ = 0 -> (Task_Count = Task_Count~));
|
|
task_limit.ads: --# global in out Task_Count_Type;
|
|
task_limit.ads: --# derives Task_Count_Type from * &
|
|
task_limit.ads: --# Success from Task_Count_Type;
|
|
task_limit.ads: --# global in out Task_Count_Type;
|
|
task_limit.ads: --# derives Task_Count_Type from *;
|
|
tcp_dns_package.adb: --# assert true;
|
|
tcp_dns_package.ads:--# inherit DNS_Types, DNS_Network, multitask_process_dns_request, Protected_SPARK_IO_05,
|
|
tcp_dns_package.ads:--# Ada.Synchronous_Task_Control, DNS_Table_Pkg;
|
|
tcp_dns_package.ads:--# own protected Startup_Suspension (Suspendable);
|
|
tcp_dns_package.ads:--# task The_Task : Tcp_Dns_Task;
|
|
tcp_dns_package.ads: --# global out Startup_Suspension;
|
|
tcp_dns_package.ads: --# derives Startup_Suspension from ;
|
|
tcp_dns_package.ads:--# global in out DNS_Network.Network;
|
|
tcp_dns_package.ads:--# in out Protected_SPARK_IO_05.SPARK_IO_PO;
|
|
tcp_dns_package.ads:--# in DNS_Table_Pkg.DNS_Table;
|
|
tcp_dns_package.ads:--# out Startup_Suspension;
|
|
tcp_dns_package.ads:--# derives DNS_Network.Network from DNS_Network.Network, DNS_Table_Pkg.DNS_Table &
|
|
tcp_dns_package.ads:--# Protected_SPARK_IO_05.SPARK_IO_PO from *, DNS_Table_Pkg.DNS_Table, DNS_Network.Network &
|
|
tcp_dns_package.ads:--# Startup_Suspension from ;
|
|
tcp_dns_package.ads:--# declare suspends => Startup_Suspension;
|
|
udp_dns_package.adb: --# assert true;
|
|
udp_dns_package.ads:--# inherit DNS_Types, DNS_Table_Pkg, DNS_Network_Receive, DNS_Network,
|
|
udp_dns_package.ads:--# Protected_SPARK_IO_05,
|
|
udp_dns_package.ads:--# process_dns_request,
|
|
udp_dns_package.ads:--# Ada.Synchronous_Task_Control;
|
|
udp_dns_package.ads:--# own protected Startup_Suspension (Suspendable);
|
|
udp_dns_package.ads:--# task The_Task : Udp_Dns_Task;
|
|
udp_dns_package.ads: --# global out Startup_Suspension;
|
|
udp_dns_package.ads: --# derives Startup_Suspension from ;
|
|
udp_dns_package.ads:--# global in out DNS_Network.Network;
|
|
udp_dns_package.ads:--# in out Protected_SPARK_IO_05.SPARK_IO_PO;
|
|
udp_dns_package.ads:--# in DNS_Table_Pkg.DNS_Table;
|
|
udp_dns_package.ads:--# out Startup_Suspension;
|
|
udp_dns_package.ads:--# derives DNS_Network.Network from DNS_Table_Pkg.DNS_Table, DNS_Network.Network &
|
|
udp_dns_package.ads:--# Protected_SPARK_IO_05.SPARK_IO_PO from *, DNS_Table_Pkg.DNS_Table, DNS_Network.Network &
|
|
udp_dns_package.ads:--# Startup_Suspension from ;
|
|
udp_dns_package.ads:--# declare suspends => Startup_Suspension;
|
|
zone_file_io.adb: --# assert true;
|
|
zone_file_io.adb: --#assert I >= 1;
|
|
zone_file_io.ads:--# inherit dns_table_pkg, dns_types, error_msgs, parser_utilities, process_first_line_of_record,
|
|
zone_file_io.ads:--# rr_type, rr_type.a_record_type, rr_type.aaaa_record_type, rr_type.cname_record_type,
|
|
zone_file_io.ads:--# rr_type.dnskey_record_type, rr_type.mx_record_type, rr_type.ns_record_type, rr_type.nsec_record_type,
|
|
zone_file_io.ads:--# rr_type.ptr_record_type, Rr_type.rrsig_record_type, rr_type.SOA_record_type,
|
|
zone_file_io.ads:--# Spark.Ada.Text_IO, unsigned_types, zone_file_parser, ada.characters.handling;
|
|
zone_file_io.ads: --# global in out dns_table_pkg.DNS_Table;
|
|
zone_file_io.ads: --# derives dns_table_pkg.DNS_Table, success from dns_table_pkg.DNS_Table, zoneFile
|
|
zone_file_io.ads: --# & zoneFile from zoneFile, dns_table_pkg.DNS_Table;
|
|
zone_file_io.ads: --# declare delay;
|
|
zone_file_parser.adb: --# assert endIdx < zlength;
|
|
zone_file_parser.adb: --# assert begIdx = begIdx% and endIdx = endIdx% and zLength = zlength%
|
|
zone_file_parser.adb: --# and endIdx <= zLength
|
|
zone_file_parser.adb: --# and endIdx-begIdx = rr_type.rrsig_record_type.timeStringLength-1
|
|
zone_file_parser.adb: --# and I <= Rr_Type.Rrsig_Record_Type.TimeStringTypeIndex'Last;
|
|
zone_file_parser.adb: --# assert for all J in Integer range 1..I-1 => (TimeString(J) >= '0' and TimeString(J) <= '9');
|
|
zone_file_parser.adb: --# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
zone_file_parser.adb: --# and endIdx = endIdx%;
|
|
zone_file_parser.adb: --# assert endIdx >= 1;
|
|
zone_file_parser.adb: --# derives RRSIG_Rec from RRSIG_Rec, zoneFileLine, zLength, endIDx, success
|
|
zone_file_parser.adb: --# & endIdx, success from zoneFileLine, zLength, endIdx, success;
|
|
zone_file_parser.adb: --# assert endIdx < zlength;
|
|
zone_file_parser.adb: --# assert begIdx = begIdx% and endIdx = endIdx% and zLength = zlength%
|
|
zone_file_parser.adb: --# and endIdx <= zLength
|
|
zone_file_parser.adb: --# and endIdx-begIdx = rr_type.rrsig_record_type.timeStringLength-1
|
|
zone_file_parser.adb: --# and I <= Rr_Type.Rrsig_Record_Type.TimeStringTypeIndex'Last;
|
|
zone_file_parser.adb: --# assert for all J in Integer range 1..I-1 => (TimeString(J) >= '0' and TimeString(J) <= '9');
|
|
zone_file_parser.adb: --# assert endIdx < zlength;
|
|
zone_file_parser.adb: --# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
zone_file_parser.adb: --# and endIdx = endIdx%;
|
|
zone_file_parser.adb: --# assert endIdx >= 1;
|
|
zone_file_parser.adb: --# assert endIdx < zlength;
|
|
zone_file_parser.adb: --# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
zone_file_parser.adb: --# and endIdx = endIdx%;
|
|
zone_file_parser.adb: --# assert endIdx >= 1;
|
|
zone_file_parser.adb: --# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
zone_file_parser.adb: --# and endIdx = endIdx%;
|
|
zone_file_parser.adb: --# assert endIdx >= begIdx;
|
|
zone_file_parser.adb: --# assert begIdx >= 1 and begIdx <= endIdx;
|
|
zone_file_parser.adb: --# assert begIdx >= 1 and begIdx <= endIdx;
|
|
zone_file_parser.adb: --# assert begIdx >= 1 and tmpVal >= 0 and tmpVal <= rr_type.SOA_record_type.MAX_SERIAL_VAL;
|
|
zone_file_parser.adb: --# assert endIdx < zlength;
|
|
zone_file_parser.adb: --# assert begIdx >= 1 and tmpVal <= rr_type.mx_record_type.MAX_PREF_VAL;
|
|
zone_file_parser.adb: --# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
zone_file_parser.adb: --# and endIdx = endIdx%;
|
|
zone_file_parser.adb: --# assert endIdx >= 1;
|
|
zone_file_parser.adb: --# assert endIdx < zlength;
|
|
zone_file_parser.adb: --# assert endIdx < zlength;
|
|
zone_file_parser.adb: --# assert endIdx < zlength;
|
|
zone_file_parser.adb: --# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
zone_file_parser.adb: --# and endIdx = endIdx%;
|
|
zone_file_parser.adb: --# assert endIdx >= 1;
|
|
zone_file_parser.adb: --# assert begIdx >= 1 and endIdx-begIdx+1 <= rr_type.MaxDomainNameLength
|
|
zone_file_parser.adb: --# and endIdx = endIdx%;
|
|
zone_file_parser.adb: --# assert endIdx >= 1;
|
|
zone_file_parser.adb: --# assert begIdx >= 1 and begIdx <= endIdx;
|
|
zone_file_parser.adb: --# assert lengthOfToken = lengthOfToken%
|
|
zone_file_parser.adb: --# and lengthOfToken < rr_type.MaxDomainNameLength;
|
|
zone_file_parser.adb: --# assert begIdx <= endIdx;
|
|
zone_file_parser.adb: --# assert begIdx >= 1 and begIdx <= endIdx;
|
|
zone_file_parser.ads:--# inherit Ada.Characters.Handling, Ada.Characters.Latin_1, dns_types, error_msgs,
|
|
zone_file_parser.ads:--# parser_utilities, rr_type, rr_type.aaaa_record_type, rr_type.dnskey_record_type,
|
|
zone_file_parser.ads:--# rr_type.mx_record_type, rr_type.rrsig_record_type, rr_type.soa_record_type,
|
|
zone_file_parser.ads:--# Spark.Ada.Strings.Maps, unsigned_types;
|
|
zone_file_parser.ads: --# derives DNSKEY_Rec, success from zoneFileLine, zLength, success;
|
|
zone_file_parser.ads: --# derives RRSIG_Rec, success from zoneFileLine, zLength, success;
|
|
zone_file_parser.ads: --# derives RRSIG_Rec, success from zoneFileLine, zLength, success;
|
|
zone_file_parser.ads: --# derives newOrigin from newOrigin, zoneFileLine, zLength
|
|
zone_file_parser.ads: --# & newTTL from newTTL, zoneFileLine, zLength, success
|
|
zone_file_parser.ads: --# & success from success, zoneFileLine, zLength;
|
|
zone_file_parser.ads: --# derives newDomainName from zoneFileLine, zLength
|
|
zone_file_parser.ads: --# & success from success, zoneFileLine, zLength;
|
|
zone_file_parser.ads: --# derives newDomainName, RRString from zoneFileLine, zLength
|
|
zone_file_parser.ads: --# & success from success, zoneFileLine, zLength;
|
|
zone_file_parser.ads: --# derives newIpv4 from zoneFileLine, zLength
|
|
zone_file_parser.ads: --# & success from success, zoneFileLine, zLength;
|
|
zone_file_parser.ads: --# derives newIpv6 from zoneFileLine, zLength
|
|
zone_file_parser.ads: --# & success from success, zoneFileLine, zLength;
|
|
zone_file_parser.ads: --# derives newPref, newDomainName from zoneFileLine, zlength
|
|
zone_file_parser.ads: --# & success from success, zoneFileLine, zLength;
|
|
zone_file_parser.ads: --# derives newNameServer, newEMail from zoneFileLine, zlength
|
|
zone_file_parser.ads: --# & success from success, zoneFileLine, zLength;
|
|
zone_file_parser.ads: --# derives newSerialNumber from zoneFileLine, zLength
|
|
zone_file_parser.ads: --# & success from success, zoneFileLine, zLength;
|
|
zone_file_parser.ads: --# derives newTimeSpec from zoneFileLine, zLength, success
|
|
zone_file_parser.ads: --# & success from success, zoneFileLine, zLength;
|
|
zone_file_parser.ads: --# derives newOwner from newOwner, zoneFileLine, zLength
|
|
zone_file_parser.ads: --# & newTTL from newTTL, zoneFileLine, zLength, success
|
|
zone_file_parser.ads: --# & newClass from newClass, zoneFileLine, zLength, success
|
|
zone_file_parser.ads: --# & newType from newType, zoneFileLine, zLength, success
|
|
zone_file_parser.ads: --# & success from success, zoneFileLine, zLength;
|