1302 lines
35 KiB
Plaintext
1302 lines
35 KiB
Plaintext
|
|
C:\Users\martin.carlisle\Documents\DARPA-DNS\svn\trunk>spark @files.txt
|
|
*******************************************************
|
|
Examiner GPL Edition
|
|
|
|
*******************************************************
|
|
|
|
|
|
|
|
Reading default switch file ...
|
|
|
|
Reading target configuration file ...
|
|
|
|
type Address is private;
|
|
|
|
--- Note : 3: The deferred constant Null_Address has been
|
|
implicitly defined here.
|
|
|
|
subtype Priority is Any_Priority range 0 .. 30;
|
|
|
|
--- Note : 4: The constant Default_Priority, of type Priority,
|
|
has been implicitly defined here.
|
|
|
|
Examining the specification of package DNS_Types ...
|
|
|
|
Examining the specification of package DNS_Network ...
|
|
|
|
WITH Gnat.Sockets;
|
|
^
|
|
--- Warning :391: If the identifier Gnat represents a package
|
|
which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
end DNS_Network;
|
|
|
|
--- Warning : 10: The private part of package DNS_Network is
|
|
hidden - hidden text is ignored by the Examiner.
|
|
|
|
Examining the body of package DNS_Network ...
|
|
|
|
with Ada.Streams;
|
|
^
|
|
--- Warning : 1: The identifier Ada is either undeclared or not
|
|
visible at this point.
|
|
|
|
with Socket_Timeout;
|
|
^
|
|
--- Warning :391: If the identifier Socket_Timeout represents a
|
|
package which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
with Ada.Unchecked_Conversion;
|
|
^
|
|
--- Warning : 1: The identifier Ada is either undeclared or not
|
|
visible at this point.
|
|
|
|
end DNS_Network;
|
|
|
|
--- Warning : 10: The body of package DNS_Network is hidden -
|
|
hidden text is ignored by the Examiner.
|
|
|
|
Generating listing file dns_network.lsb ...
|
|
|
|
Examining the specification of package Dns_Network_Receive ...
|
|
|
|
Examining the body of package Dns_Network_Receive ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
Receive_DNS_Packet_TCP performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Receive_DNS_Packet
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
Generating listing file dns_network_receive.lsb ...
|
|
|
|
Examining the specification of package Handling ...
|
|
|
|
Examining the specification of package Unsigned_Types ...
|
|
|
|
Examining the specification of package Rr_Type ...
|
|
|
|
Examining the specification of package A_Record_Type ...
|
|
|
|
Examining the specification of package Aaaa_Record_Type ...
|
|
|
|
Examining the specification of package Cname_Record_Type ...
|
|
|
|
Examining the specification of package Dnskey_Record_Type ...
|
|
|
|
Examining the specification of package Mx_Record_Type ...
|
|
|
|
Examining the specification of package Ns_Record_Type ...
|
|
|
|
Examining the specification of package Nsec_Record_Type ...
|
|
|
|
Examining the specification of package Ptr_Record_Type ...
|
|
|
|
Examining the specification of package Rrsig_Record_Type ...
|
|
|
|
Examining the specification of package Soa_Record_Type ...
|
|
|
|
Examining the specification of package dns_table_pkg ...
|
|
|
|
Examining the body of package Dns_Table_Pkg ...
|
|
|
|
+++ Flow analysis of subprogram To_Lower performed:
|
|
no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Same performed: no
|
|
errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram hash performed: no
|
|
errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram queryARecords
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram queryAAAARecords
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram queryCNAMERecords
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram queryDNSKEYRecords
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram queryMXRecords
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram queryNSRecords
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram queryNSECRecords
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram queryPTRRecords
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram queryRRSIGRecords
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram querySOARecords
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram insertARecord
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram insertAAAARecord
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram insertCNAMERecord
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram InsertDNSKEYRecord
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram insertMXRecord
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram insertNSRecord
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram insertNSECRecord
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram insertPTRRecord
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram InsertRRSIGRecord
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram InsertSOARecord
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
Generating listing file dns_table_pkg.lsb ...
|
|
|
|
Examining the body of package DNS_Types ...
|
|
|
|
with Gnat.Byte_Swapping;
|
|
^
|
|
--- Warning :391: If the identifier Gnat represents a package
|
|
which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
end Byte_Swap_US;
|
|
|
|
--- Warning : 10: The body of subprogram Byte_Swap_US is hidden -
|
|
hidden text is ignored by the Examiner.
|
|
|
|
+++ Flow analysis of subprogram Byte_Swap performed:
|
|
no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
Generating listing file dns_types.lsb ...
|
|
|
|
Examining the specification of package Error_Msgs ...
|
|
|
|
Examining the body of package Error_Msgs ...
|
|
|
|
with Ada.Text_IO, Ada.Integer_Text_IO;
|
|
^
|
|
--- Warning : 1: The identifier Ada is either undeclared or not
|
|
visible at this point.
|
|
^
|
|
--- Warning : 1: The identifier Ada is either undeclared or not
|
|
visible at this point.
|
|
|
|
end error_msgs;
|
|
|
|
--- Warning : 10: The body of package Error_Msgs is hidden -
|
|
hidden text is ignored by the Examiner.
|
|
|
|
Generating listing file error_msgs.lsb ...
|
|
|
|
Examining the specification of package Protected_SPARK_IO_05 ...
|
|
|
|
with Ada.Text_IO;
|
|
^
|
|
--- Warning : 1: The identifier Ada is either undeclared or not
|
|
visible at this point.
|
|
|
|
end Protected_SPARK_IO_05;
|
|
|
|
--- Warning : 10: The private part of package
|
|
Protected_SPARK_IO_05 is hidden - hidden text is ignored by the
|
|
Examiner.
|
|
|
|
Examining the specification of package Process_Dns_Request ...
|
|
|
|
Examining the specification of package Multitask_Process_Dns_Request ...
|
|
|
|
Examining the body of package Multitask_Process_Dns_Request ...
|
|
|
|
with Task_Limit;
|
|
^
|
|
--- Warning :391: If the identifier Task_Limit represents a
|
|
package which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
end Multitask_Process_Dns_Request;
|
|
|
|
--- Warning : 10: The body of package
|
|
Multitask_Process_Dns_Request is hidden - hidden text is ignored by
|
|
the Examiner.
|
|
|
|
Generating listing file multitask_process_dns_request.lsb ...
|
|
|
|
Examining the specification of package Non_Spark_Stuff ...
|
|
|
|
Examining the body of package Non_Spark_Stuff ...
|
|
|
|
with Ada.Calendar;
|
|
^
|
|
--- Warning : 1: The identifier Ada is either undeclared or not
|
|
visible at this point.
|
|
|
|
end Non_Spark_Stuff;
|
|
|
|
--- Warning : 10: The body of package Non_Spark_Stuff is hidden -
|
|
hidden text is ignored by the Examiner.
|
|
|
|
Generating listing file non_spark_stuff.lsb ...
|
|
|
|
Examining the specification of package Parser_Utilities ...
|
|
|
|
Examining the body of package Parser_Utilities ...
|
|
|
|
+++ Flow analysis of subprogram isClass performed:
|
|
no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram isRecord performed:
|
|
no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram getRecordType
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram CheckAndAppendOrigin
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram checkValidHostName
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram findFirstToken
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram findNextToken
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram IsMult performed: no
|
|
errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram convert8BitUnsigned
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram convert16BitUnsigned
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram convert32BitUnsigned
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram MultValue performed:
|
|
no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram ConvertTimeSpec
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram ConvertTimeString
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram AddToKeyR performed:
|
|
no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram AddToKey performed:
|
|
no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram SeparatorsOK
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram convertIpv6
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram SeparatorsOK
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram convertIpv4
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
Generating listing file parser_utilities.lsb ...
|
|
|
|
Examining the body of package Process_Dns_Request ...
|
|
|
|
with Ada.Text_Io;
|
|
^
|
|
--- Warning :391: If the identifier Text_Io represents a package
|
|
which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
+++ Flow analysis of subprogram Set_Unsigned_32
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Set_Unsigned_16
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Set_TTL_Data_IP
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
Set_TTL_Data_NS_Response performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
Set_TTL_Data_PTR_Response performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
Set_TTL_Data_MX_Response performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
Set_TTL_Data_SOA_Response performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Set_TTL_Data_AAAA_IP
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
for i in rr_type.aaaa_record_type.IPV6AddrTypeIndex loop
|
|
|
|
--- Warning :402: Default assertion planted to cut loop.
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
Get_Query_Name_Type_Class performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
Create_Response_Error performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Create_Response_AAAA
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Create_Response_A
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Create_Response_NS
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Create_Response_PTR
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Create_Response_MX
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Create_Response_SOA
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
Process_Response_Cname performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Trim_Name performed:
|
|
no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
Create_NXDOMAIN_Response performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
EDNS_Rec.Code := To_Query_Type(DNS_Types.Unsigned_Short(
|
|
^
|
|
--- Warning : 12: Function To_Query_Type is an instantiation of
|
|
Unchecked_Conversion.
|
|
|
|
From_Query_Type(DNS_Types.OPT) mod 256);
|
|
^
|
|
--- Warning : 12: Function From_Query_Type is an instantiation of
|
|
Unchecked_Conversion.
|
|
|
|
+++ Flow analysis of subprogram Create_Response_EDNS
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Create_Response
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Process_Request_Tcp
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
Generating listing file process_dns_request.lsb ...
|
|
|
|
Examining the specification of package SPARK ...
|
|
|
|
Examining the specification of package Ada ...
|
|
|
|
Examining the specification of package Text_IO ...
|
|
|
|
with Ada.Text_IO;
|
|
^
|
|
--- Warning : 1: The identifier Ada is either undeclared or not
|
|
visible at this point.
|
|
|
|
end SPARK.Ada.Text_IO;
|
|
|
|
--- Warning : 10: The private part of package Text_IO is hidden -
|
|
hidden text is ignored by the Examiner.
|
|
|
|
Examining the specification of package Strings ...
|
|
|
|
Examining the specification of package Maps ...
|
|
|
|
with Ada.Strings.Maps;
|
|
^
|
|
--- Warning : 1: The identifier Ada is either undeclared or not
|
|
visible at this point.
|
|
|
|
end SPARK.Ada.Strings.Maps;
|
|
|
|
--- Warning : 10: The private part of package Maps is hidden -
|
|
hidden text is ignored by the Examiner.
|
|
|
|
Examining the specification of package Zone_File_Parser ...
|
|
|
|
Examining the specification of package process_first_line_of_record ...
|
|
|
|
Examining the body of package process_first_line_of_record ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
ProcessFirstLineOfRecord performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
Generating listing file process_first_line_of_record.lsb ...
|
|
|
|
Examining the body of package Protected_Spark_Io_05 ...
|
|
|
|
with Text_IO;
|
|
^
|
|
--- Warning :391: If the identifier Text_IO represents a package
|
|
which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
with Unchecked_Deallocation;
|
|
^
|
|
--- Warning :391: If the identifier Unchecked_Deallocation
|
|
represents a package which contains a task or an interrupt handler
|
|
then the partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
end Protected_Spark_Io_05;
|
|
|
|
--- Warning : 10: The body of package Protected_Spark_Io_05 is
|
|
hidden - hidden text is ignored by the Examiner.
|
|
|
|
Generating listing file protected_spark_io_05.lsb ...
|
|
|
|
Examining the body of package Rr_Type ...
|
|
|
|
+++ Flow analysis of subprogram DomainNameLength
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram AppendDomainNames
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram WireNameLength
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
ConvertStringToDomainName performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram FindPeriod
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
ConvertDomainNameToWire performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram ConvertStringToWire
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
Generating listing file rr_type.lsb ...
|
|
|
|
Examining the specification of package Socket_Timeout ...
|
|
|
|
WITH Gnat.Sockets;
|
|
^
|
|
--- Warning :391: If the identifier Gnat represents a package
|
|
which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
end Socket_Timeout;
|
|
|
|
--- Warning : 10: The private part of package Socket_Timeout is
|
|
hidden - hidden text is ignored by the Examiner.
|
|
^
|
|
--- Warning :394: Variables of type Socket_Type cannot be
|
|
initialized using the facilities of this package.
|
|
|
|
Examining the body of package Socket_Timeout ...
|
|
|
|
with Gnat.Sockets.Thin;
|
|
^
|
|
--- Warning :391: If the identifier Gnat represents a package
|
|
which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
with Interfaces;
|
|
^
|
|
--- Warning :391: If the identifier Interfaces represents a
|
|
package which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
with Interfaces.C;
|
|
^
|
|
--- Warning :391: If the identifier Interfaces represents a
|
|
package which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
with Ada.Unchecked_Conversion;
|
|
^
|
|
--- Warning : 1: The identifier Ada is either undeclared or not
|
|
visible at this point.
|
|
|
|
with Gnat.Sockets.Constants;
|
|
^
|
|
--- Warning :391: If the identifier Gnat represents a package
|
|
which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
with ada.text_io;
|
|
^
|
|
--- Warning : 1: The identifier ada is either undeclared or not
|
|
visible at this point.
|
|
|
|
end Socket_Timeout;
|
|
|
|
--- Warning : 10: The body of package Socket_Timeout is hidden -
|
|
hidden text is ignored by the Examiner.
|
|
|
|
Generating listing file socket_timeout.lsb ...
|
|
|
|
Examining the specification of package SPARK_Ada_Command_Line ...
|
|
|
|
Examining the body of package SPARK_Ada_Command_Line ...
|
|
|
|
with Ada.Command_Line;
|
|
^
|
|
--- Warning : 1: The identifier Ada is either undeclared or not
|
|
visible at this point.
|
|
|
|
with Ada.Text_IO;
|
|
^
|
|
--- Warning : 1: The identifier Ada is either undeclared or not
|
|
visible at this point.
|
|
|
|
with Gnat.Os_Lib;
|
|
^
|
|
--- Warning :391: If the identifier Gnat represents a package
|
|
which contains a task or an interrupt handler then the
|
|
partition-level analysis performed by the Examiner will be
|
|
incomplete. Such packages must be inherited as well as withed.
|
|
|
|
end SPARK_Ada_Command_Line;
|
|
|
|
--- Warning : 10: The body of package SPARK_Ada_Command_Line is
|
|
hidden - hidden text is ignored by the Examiner.
|
|
|
|
Generating listing file spark_ada_command_line.lsb ...
|
|
|
|
Examining the specification of package Udp_Dns_Package ...
|
|
|
|
Examining the specification of package Tcp_Dns_Package ...
|
|
|
|
Examining the specification of package zone_file_io ...
|
|
|
|
Examining main program Spark_Dns_Main ...
|
|
|
|
+++ Flow analysis of subprogram Spark_Dns_Main
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of the entire partition performed:
|
|
no errors found.
|
|
|
|
Generating listing file spark_dns_main.lsb ...
|
|
|
|
Examining the specification of package Task_Limit ...
|
|
|
|
Examining the body of package Task_Limit ...
|
|
|
|
+++ Flow analysis of subprogram Increment performed:
|
|
no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Decrement performed:
|
|
no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
Generating listing file task_limit.lsb ...
|
|
|
|
Examining the body of package Tcp_Dns_Package ...
|
|
|
|
+++ Flow analysis of subprogram Initialization_Done
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Tcp_Dns_Task
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
Generating listing file tcp_dns_package.lsb ...
|
|
|
|
Examining the body of package Udp_Dns_Package ...
|
|
|
|
+++ Flow analysis of subprogram Initialization_Done
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram Udp_Dns_Task
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
Generating listing file udp_dns_package.lsb ...
|
|
|
|
Examining the body of package Zone_File_Io ...
|
|
|
|
+++ Flow analysis of subprogram processzoneFile
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
Generating listing file zone_file_io.lsb ...
|
|
|
|
Examining the body of package zone_file_parser ...
|
|
|
|
+++ Flow analysis of subprogram ParseDNSKeyHeader
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram ParseRRSig2ndLine
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
ParseTypeCoveredAlgorithmNumLabels performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram ParseRRSigHeader
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram parseDomainName
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
ParseDomainNameAndRRString performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram ParseTimeSpec
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram ParseControlLine
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram parseSerialNumber
|
|
performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
parsePrefAndDomainName performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram parseIpv4 performed:
|
|
no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram parseIpv6 performed:
|
|
no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
ParseNameServerAndEmail performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
+++ Flow analysis of subprogram
|
|
parseOwnerTTLClassAndRecordType performed: no errors found.
|
|
|
|
Building model of subprogram ...
|
|
|
|
Generating VCs ...
|
|
|
|
Writing VCs ...
|
|
|
|
Generating listing file zone_file_parser.lsb ...
|
|
|
|
Generating report file ...
|
|
|
|
44 errors or warnings, comprising:
|
|
44 warnings
|
|
56 expected (justified) warnings
|
|
|
|
|
|
-----------End of SPARK Examination--------------------------------
|