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--------------------------------