312 lines
8.6 KiB
Plaintext
312 lines
8.6 KiB
Plaintext
*******************************************************
|
|
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 specification of package Dns_Network_Receive ...
|
|
|
|
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 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 Ns_Record_Type ...
|
|
|
|
Examining the specification of package Mx_Record_Type ...
|
|
|
|
Examining the specification of package Ptr_Record_Type ...
|
|
|
|
Examining the specification of package Soa_Record_Type ...
|
|
|
|
Examining the specification of package Handling ...
|
|
|
|
Examining the specification of package Dnskey_Record_Type ...
|
|
|
|
Examining the specification of package Nsec_Record_Type ...
|
|
|
|
Examining the specification of package dns_table_pkg ...
|
|
|
|
Examining the specification of package Process_Dns_Request ...
|
|
|
|
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 ...
|
|
|
|
Generating report file ...
|
|
|
|
10 errors or warnings, comprising:
|
|
10 warnings
|
|
33 expected (justified) warnings
|
|
|
|
|
|
-----------End of SPARK Examination--------------------------------
|