1049 lines
30 KiB
Plaintext
1049 lines
30 KiB
Plaintext
*******************************************************
|
|
Report of SPARK Examination
|
|
Examiner GPL Edition
|
|
|
|
*******************************************************
|
|
|
|
|
|
Options:
|
|
index_file=mcc.idx
|
|
nowarning_file
|
|
notarget_compiler_data
|
|
config_file=mcc.cfg
|
|
source_extension=ada
|
|
listing_extension=ls_
|
|
nodictionary_file
|
|
report_file=spark.rep
|
|
nohtml
|
|
vcg
|
|
plain_output
|
|
sparklib
|
|
nostatistics
|
|
fdl_identifiers=accept
|
|
flow_analysis=information
|
|
language=95
|
|
profile=ravenscar
|
|
annotation_character=#
|
|
rules=none
|
|
error_explanations=off
|
|
justification_option=full
|
|
output_directory=.
|
|
output_directory (actual)=.
|
|
|
|
Selected files:
|
|
@files.txt
|
|
|
|
|
|
Index Filename(s) used were:
|
|
mcc.idx
|
|
ada.idx
|
|
spark.idx
|
|
|
|
|
|
Meta File(s) used were:
|
|
files.txt
|
|
dns_network.adb
|
|
dns_network_receive.adb
|
|
dns_table_pkg.adb
|
|
dns_types.adb
|
|
error_msgs.adb
|
|
multitask_process_dns_request.adb
|
|
non_spark_stuff.adb
|
|
parser_utilities.adb
|
|
process_dns_request.adb
|
|
process_first_line_of_record.adb
|
|
protected_spark_io_05.adb
|
|
rr_type.adb
|
|
socket_timeout.adb
|
|
spark_ada_command_line.adb
|
|
spark_dns_main.adb
|
|
task_limit.adb
|
|
tcp_dns_package.adb
|
|
udp_dns_package.adb
|
|
zone_file_io.adb
|
|
zone_file_parser.adb
|
|
|
|
|
|
Full warning reporting selected
|
|
|
|
|
|
Target configuration file:
|
|
Line
|
|
-- Auto-generated SPARK target configuration file
|
|
-- Target claims to be 'SYSTEM_NAME_GNAT'
|
|
|
|
package Standard is
|
|
type Integer is range -2147483648 .. 2147483647;
|
|
type Float is digits 6 range -3.40282E+38 .. 3.40282E+38;
|
|
type Short_Short_Integer is range -128 .. 127;
|
|
type Short_Integer is range -32768 .. 32767;
|
|
type Long_Integer is range -2147483648 .. 2147483647;
|
|
type Long_Long_Integer is range -9223372036854775808 .. 9223372036854775807;
|
|
end Standard;
|
|
|
|
package System is
|
|
type Address is private;
|
|
|
|
--- Note : 3: The deferred constant Null_Address has been
|
|
implicitly defined here.
|
|
|
|
Min_Int : constant := -9223372036854775808;
|
|
Max_Int : constant := 9223372036854775807;
|
|
Max_Binary_Modulus : constant := 18446744073709551615 + 1;
|
|
Max_Digits : constant := 18;
|
|
Max_Base_Digits : constant := 18;
|
|
Max_Mantissa : constant := 63;
|
|
Storage_Unit : constant := 8;
|
|
Word_Size : constant := 32;
|
|
Fine_Delta : constant := 1.08420217248550443E-19;
|
|
subtype Any_Priority is Integer range 0 .. 31;
|
|
subtype Priority is Any_Priority range 0 .. 30;
|
|
|
|
--- Note : 4: The constant Default_Priority, of type Priority,
|
|
has been implicitly defined here.
|
|
|
|
subtype Interrupt_Priority is Any_Priority range 31 .. 31;
|
|
Default_Bit_Order : constant Bit_Order := Low_Order_First;
|
|
end System;
|
|
|
|
|
|
Source Filename(s) used were:
|
|
dns_network.adb
|
|
dns_network.ads
|
|
dns_types.ads
|
|
dns_network_receive.adb
|
|
dns_network_receive.ads
|
|
dns_table_pkg.adb
|
|
dns_table_pkg.ads
|
|
rr_type-soa_record_type.ads
|
|
rr_type-rrsig_record_type.ads
|
|
rr_type-ptr_record_type.ads
|
|
rr_type-nsec_record_type.ads
|
|
rr_type-ns_record_type.ads
|
|
rr_type-mx_record_type.ads
|
|
rr_type-dnskey_record_type.ads
|
|
rr_type-cname_record_type.ads
|
|
rr_type-aaaa_record_type.ads
|
|
rr_type-a_record_type.ads
|
|
rr_type.ads
|
|
unsigned_types.ads
|
|
ada-characters-handling.shs
|
|
dns_types.adb
|
|
error_msgs.adb
|
|
error_msgs.ads
|
|
multitask_process_dns_request.adb
|
|
multitask_process_dns_request.ads
|
|
process_dns_request.ads
|
|
protected_spark_io_05.ads
|
|
non_spark_stuff.adb
|
|
non_spark_stuff.ads
|
|
parser_utilities.adb
|
|
parser_utilities.ads
|
|
process_dns_request.adb
|
|
process_first_line_of_record.adb
|
|
process_first_line_of_record.ads
|
|
zone_file_parser.ads
|
|
spark-ada-text_io.ads
|
|
spark-ada.ads
|
|
spark.ads
|
|
spark-ada-strings-maps.ads
|
|
spark-ada-strings.ads
|
|
protected_spark_io_05.adb
|
|
rr_type.adb
|
|
socket_timeout.adb
|
|
socket_timeout.ads
|
|
spark_ada_command_line.adb
|
|
spark_ada_command_line.ads
|
|
spark_dns_main.adb
|
|
zone_file_io.ads
|
|
tcp_dns_package.ads
|
|
udp_dns_package.ads
|
|
task_limit.adb
|
|
task_limit.ads
|
|
tcp_dns_package.adb
|
|
udp_dns_package.adb
|
|
zone_file_io.adb
|
|
zone_file_parser.adb
|
|
|
|
|
|
|
|
Source Filename: dns_network.ads
|
|
No Listing File
|
|
|
|
Unit name: DNS_Network
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
2 error(s) or warning(s)
|
|
|
|
Line
|
|
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.
|
|
|
|
|
|
Source Filename: dns_types.ads
|
|
No Listing File
|
|
|
|
Unit name: DNS_Types
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Expected messages marked with the accept annotation
|
|
Type Msg Lines Reason Match
|
|
No. From To No. Line
|
|
Warn 2 representation clause ok 1
|
|
Warn 2 representation clause ok 1
|
|
Warn 2 representation clause ok 1
|
|
Warn 2 representation clause ok 1
|
|
Warn 2 representation clause ok 3
|
|
Warn 3 Inline ok 1
|
|
Warn 2 representation clause ok 2
|
|
Warn 2 representation clause ok 2
|
|
|
|
|
|
|
|
Source Filename: dns_network_receive.ads
|
|
No Listing File
|
|
|
|
Unit name: Dns_Network_Receive
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: dns_table_pkg.ads
|
|
No Listing File
|
|
|
|
Unit name: dns_table_pkg
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: rr_type-soa_record_type.ads
|
|
No Listing File
|
|
|
|
Unit name: Rr_Type.Soa_Record_Type
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: rr_type-rrsig_record_type.ads
|
|
No Listing File
|
|
|
|
Unit name: Rr_Type.Rrsig_Record_Type
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: rr_type-ptr_record_type.ads
|
|
No Listing File
|
|
|
|
Unit name: Rr_Type.Ptr_Record_Type
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: rr_type-nsec_record_type.ads
|
|
No Listing File
|
|
|
|
Unit name: Rr_Type.Nsec_Record_Type
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: rr_type-ns_record_type.ads
|
|
No Listing File
|
|
|
|
Unit name: Rr_Type.Ns_Record_Type
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: rr_type-mx_record_type.ads
|
|
No Listing File
|
|
|
|
Unit name: Rr_Type.Mx_Record_Type
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: rr_type-dnskey_record_type.ads
|
|
No Listing File
|
|
|
|
Unit name: Rr_Type.Dnskey_Record_Type
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: rr_type-cname_record_type.ads
|
|
No Listing File
|
|
|
|
Unit name: Rr_Type.Cname_Record_Type
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: rr_type-aaaa_record_type.ads
|
|
No Listing File
|
|
|
|
Unit name: RR_Type.Aaaa_Record_Type
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: rr_type-a_record_type.ads
|
|
No Listing File
|
|
|
|
Unit name: Rr_Type.A_Record_Type
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: rr_type.ads
|
|
No Listing File
|
|
|
|
Unit name: Rr_Type
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: unsigned_types.ads
|
|
No Listing File
|
|
|
|
Unit name: Unsigned_Types
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: ada-characters-handling.shs
|
|
No Listing File
|
|
|
|
Unit name: Ada.Characters.Handling
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: error_msgs.ads
|
|
No Listing File
|
|
|
|
Unit name: Error_Msgs
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: multitask_process_dns_request.ads
|
|
No Listing File
|
|
|
|
Unit name: Multitask_Process_Dns_Request
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: process_dns_request.ads
|
|
No Listing File
|
|
|
|
Unit name: Process_Dns_Request
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: protected_spark_io_05.ads
|
|
No Listing File
|
|
|
|
Unit name: Protected_SPARK_IO_05
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
2 error(s) or warning(s)
|
|
|
|
Line
|
|
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.
|
|
|
|
|
|
Source Filename: non_spark_stuff.ads
|
|
No Listing File
|
|
|
|
Unit name: Non_Spark_Stuff
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: parser_utilities.ads
|
|
No Listing File
|
|
|
|
Unit name: Parser_Utilities
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: process_first_line_of_record.ads
|
|
No Listing File
|
|
|
|
Unit name: process_first_line_of_record
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: zone_file_parser.ads
|
|
No Listing File
|
|
|
|
Unit name: Zone_File_Parser
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: spark-ada-text_io.ads
|
|
No Listing File
|
|
|
|
Unit name: SPARK.Ada.Text_IO
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
2 error(s) or warning(s)
|
|
|
|
Line
|
|
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.
|
|
|
|
|
|
Source Filename: spark-ada.ads
|
|
No Listing File
|
|
|
|
Unit name: SPARK.Ada
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: spark.ads
|
|
No Listing File
|
|
|
|
Unit name: SPARK
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: spark-ada-strings-maps.ads
|
|
No Listing File
|
|
|
|
Unit name: SPARK.Ada.Strings.Maps
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
2 error(s) or warning(s)
|
|
|
|
Line
|
|
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.
|
|
|
|
|
|
Source Filename: spark-ada-strings.ads
|
|
No Listing File
|
|
|
|
Unit name: SPARK.Ada.Strings
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: socket_timeout.ads
|
|
No Listing File
|
|
|
|
Unit name: Socket_Timeout
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
3 error(s) or warning(s)
|
|
|
|
Line
|
|
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.
|
|
|
|
|
|
Source Filename: spark_ada_command_line.ads
|
|
No Listing File
|
|
|
|
Unit name: SPARK_Ada_Command_Line
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: zone_file_io.ads
|
|
No Listing File
|
|
|
|
Unit name: zone_file_io
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: tcp_dns_package.ads
|
|
No Listing File
|
|
|
|
Unit name: Tcp_Dns_Package
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: udp_dns_package.ads
|
|
No Listing File
|
|
|
|
Unit name: Udp_Dns_Package
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: task_limit.ads
|
|
No Listing File
|
|
|
|
Unit name: Task_Limit
|
|
Unit type: package specification
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: dns_network.adb
|
|
Listing Filename: dns_network.lsb
|
|
|
|
Unit name: DNS_Network
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
4 error(s) or warning(s)
|
|
|
|
Line
|
|
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.
|
|
|
|
|
|
Source Filename: dns_network_receive.adb
|
|
Listing Filename: dns_network_receive.lsb
|
|
|
|
Unit name: Dns_Network_Receive
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: dns_table_pkg.adb
|
|
Listing Filename: dns_table_pkg.lsb
|
|
|
|
Unit name: Dns_Table_Pkg
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Expected messages marked with the accept annotation
|
|
Type Msg Lines Reason Match
|
|
No. From To No. Line
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 23 assigning to uninitialized array 1
|
|
Flow 602 end fills as much of array as needed 1
|
|
Flow 10 only care if there are any 1
|
|
Flow 33 end only care if there are any 1
|
|
|
|
|
|
|
|
Source Filename: dns_types.adb
|
|
Listing Filename: dns_types.lsb
|
|
|
|
Unit name: DNS_Types
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
2 error(s) or warning(s)
|
|
|
|
Line
|
|
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.
|
|
|
|
|
|
Source Filename: error_msgs.adb
|
|
Listing Filename: error_msgs.lsb
|
|
|
|
Unit name: Error_Msgs
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
3 error(s) or warning(s)
|
|
|
|
Line
|
|
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.
|
|
|
|
|
|
Source Filename: multitask_process_dns_request.adb
|
|
Listing Filename: multitask_process_dns_request.lsb
|
|
|
|
Unit name: Multitask_Process_Dns_Request
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
2 error(s) or warning(s)
|
|
|
|
Line
|
|
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.
|
|
|
|
|
|
Source Filename: non_spark_stuff.adb
|
|
Listing Filename: non_spark_stuff.lsb
|
|
|
|
Unit name: Non_Spark_Stuff
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
2 error(s) or warning(s)
|
|
|
|
Line
|
|
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.
|
|
|
|
|
|
Source Filename: parser_utilities.adb
|
|
Listing Filename: parser_utilities.lsb
|
|
|
|
Unit name: Parser_Utilities
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: process_dns_request.adb
|
|
Listing Filename: process_dns_request.lsb
|
|
|
|
Unit name: Process_Dns_Request
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
4 error(s) or warning(s)
|
|
|
|
Line
|
|
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.
|
|
|
|
for i in rr_type.aaaa_record_type.IPV6AddrTypeIndex loop
|
|
|
|
--- Warning :402: Default assertion planted to cut loop.
|
|
|
|
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.
|
|
|
|
|
|
Expected messages marked with the accept annotation
|
|
Type Msg Lines Reason Match
|
|
No. From To No. Line
|
|
Warn 12 unchecked conversions ok 2
|
|
Warn 12 unchecked conversions ok 1
|
|
Warn 12 unchecked conversions ok 2
|
|
Warn 12 unchecked conversions ok 1
|
|
Flow 10 The rest of the header fields re 1
|
|
Flow 10 The rest of the header fields re 1
|
|
Flow 10 The rest of the header fields re 1
|
|
Flow 10 not needed for ANY query 1
|
|
Flow 10 not needed for ANY query 1
|
|
Flow 10 not needed for any query 1
|
|
Flow 10 not needed for ANY query 1
|
|
Flow 10 not needed for ANY query 1
|
|
Flow 10 not needed for any query 1
|
|
Flow 23 init not needed 1
|
|
Flow 10 only needed for UDP 1
|
|
Flow 22 allow use of static expression f 1
|
|
Flow 602 end initialization is unneeded 1
|
|
Flow 602 end initialization is unneeded 1
|
|
Flow 33 end Max_Transmit only for UDP 1
|
|
|
|
|
|
|
|
Source Filename: process_first_line_of_record.adb
|
|
Listing Filename: process_first_line_of_record.lsb
|
|
|
|
Unit name: process_first_line_of_record
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: protected_spark_io_05.adb
|
|
Listing Filename: protected_spark_io_05.lsb
|
|
|
|
Unit name: Protected_Spark_Io_05
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
3 error(s) or warning(s)
|
|
|
|
Line
|
|
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.
|
|
|
|
|
|
Source Filename: rr_type.adb
|
|
Listing Filename: rr_type.lsb
|
|
|
|
Unit name: Rr_Type
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: socket_timeout.adb
|
|
Listing Filename: socket_timeout.lsb
|
|
|
|
Unit name: Socket_Timeout
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
7 error(s) or warning(s)
|
|
|
|
Line
|
|
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.
|
|
|
|
|
|
Source Filename: spark_ada_command_line.adb
|
|
Listing Filename: spark_ada_command_line.lsb
|
|
|
|
Unit name: SPARK_Ada_Command_Line
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
4 error(s) or warning(s)
|
|
|
|
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.
|
|
|
|
|
|
Source Filename: spark_dns_main.adb
|
|
Listing Filename: spark_dns_main.lsb
|
|
|
|
Unit name: Spark_Dns_Main
|
|
Unit type: main program
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Expected messages marked with the accept annotation
|
|
Type Msg Lines Reason Match
|
|
No. From To No. Line
|
|
Flow 10 done with file after this call 1
|
|
|
|
|
|
|
|
Source Filename: task_limit.adb
|
|
Listing Filename: task_limit.lsb
|
|
|
|
Unit name: Task_Limit
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: tcp_dns_package.adb
|
|
Listing Filename: tcp_dns_package.lsb
|
|
|
|
Unit name: Tcp_Dns_Package
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: udp_dns_package.adb
|
|
Listing Filename: udp_dns_package.lsb
|
|
|
|
Unit name: Udp_Dns_Package
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: zone_file_io.adb
|
|
Listing Filename: zone_file_io.lsb
|
|
|
|
Unit name: Zone_File_Io
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
Source Filename: zone_file_parser.adb
|
|
Listing Filename: zone_file_parser.lsb
|
|
|
|
Unit name: zone_file_parser
|
|
Unit type: package body
|
|
Unit has been analysed, any errors are listed below.
|
|
|
|
No errors found
|
|
|
|
|
|
--End of file--------------------------------------------------
|