           *******************************************************
                       Semantic Analysis of SPARK Text
                             Examiner GPL Edition

           *******************************************************


            procedure Dns_Network_Receive.Receive_DNS_Packet_TCP




For path(s) from start to run-time check associated with statement of line 33:

procedure_receive_dns_packet_tcp_1.
H1:    true .
H2:    fld_length(packet__1) >= dns_types__unsigned_short__first .
H3:    fld_length(packet__1) <= dns_types__unsigned_short__last .
H4:    fld_messageid(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H5:    fld_messageid(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H6:    fld_opcode(fld_header(fld_rest(packet__1))) >= 
           dns_types__opcode_type__first .
H7:    fld_opcode(fld_header(fld_rest(packet__1))) <= 
           dns_types__opcode_type__last .
H8:    fld_rcode(fld_header(fld_rest(packet__1))) >= 
           dns_types__response_code__first .
H9:    fld_rcode(fld_header(fld_rest(packet__1))) <= 
           dns_types__response_code__last .
H10:   fld_qdcount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H11:   fld_qdcount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H12:   fld_ancount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H13:   fld_ancount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H14:   fld_nscount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H15:   fld_nscount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H16:   fld_arcount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H17:   fld_arcount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H18:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(fld_rest(packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           packet__1)), [i___1]) <= dns_types__byte__last))) .
H19:   number_bytes__1 >= dns_types__packet_length_range__first .
H20:   number_bytes__1 <= dns_types__packet_length_range__last .
        ->
C1:    number_bytes__1 >= dns_types__packet_length_range__first .
C2:    number_bytes__1 <= dns_types__packet_length_range__last .
 

For path(s) from start to run-time check associated with statement of line 39:

procedure_receive_dns_packet_tcp_2.
H1:    true .
H2:    fld_length(packet__1) >= dns_types__unsigned_short__first .
H3:    fld_length(packet__1) <= dns_types__unsigned_short__last .
H4:    fld_messageid(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H5:    fld_messageid(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H6:    fld_opcode(fld_header(fld_rest(packet__1))) >= 
           dns_types__opcode_type__first .
H7:    fld_opcode(fld_header(fld_rest(packet__1))) <= 
           dns_types__opcode_type__last .
H8:    fld_rcode(fld_header(fld_rest(packet__1))) >= 
           dns_types__response_code__first .
H9:    fld_rcode(fld_header(fld_rest(packet__1))) <= 
           dns_types__response_code__last .
H10:   fld_qdcount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H11:   fld_qdcount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H12:   fld_ancount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H13:   fld_ancount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H14:   fld_nscount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H15:   fld_nscount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H16:   fld_arcount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H17:   fld_arcount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H18:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(fld_rest(packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           packet__1)), [i___1]) <= dns_types__byte__last))) .
H19:   number_bytes__1 >= dns_types__packet_length_range__first .
H20:   number_bytes__1 <= dns_types__packet_length_range__last .
H21:   number_bytes__1 >= dns_types__packet_length_range__first .
H22:   number_bytes__1 <= dns_types__packet_length_range__last .
H23:   true .
H24:   not failure__1 .
H25:   number_bytes__1 >= dns_types__packet_length_range__first .
H26:   number_bytes__1 <= dns_types__packet_length_range__last .
        ->
C1:    1 + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
C2:    1 + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
C3:    1 + dns_types__header_bits div 8 >= system__min_int .
C4:    1 + dns_types__header_bits div 8 <= system__max_int .
C5:    dns_types__header_bits div 8 >= system__min_int .
C6:    dns_types__header_bits div 8 <= system__max_int .
C7:    8 <> 0 .
 

For path(s) from start to finish:

procedure_receive_dns_packet_tcp_3.
H1:    true .
H2:    fld_length(packet__1) >= dns_types__unsigned_short__first .
H3:    fld_length(packet__1) <= dns_types__unsigned_short__last .
H4:    fld_messageid(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H5:    fld_messageid(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H6:    fld_opcode(fld_header(fld_rest(packet__1))) >= 
           dns_types__opcode_type__first .
H7:    fld_opcode(fld_header(fld_rest(packet__1))) <= 
           dns_types__opcode_type__last .
H8:    fld_rcode(fld_header(fld_rest(packet__1))) >= 
           dns_types__response_code__first .
H9:    fld_rcode(fld_header(fld_rest(packet__1))) <= 
           dns_types__response_code__last .
H10:   fld_qdcount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H11:   fld_qdcount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H12:   fld_ancount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H13:   fld_ancount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H14:   fld_nscount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H15:   fld_nscount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H16:   fld_arcount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H17:   fld_arcount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H18:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(fld_rest(packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           packet__1)), [i___1]) <= dns_types__byte__last))) .
H19:   number_bytes__1 >= dns_types__packet_length_range__first .
H20:   number_bytes__1 <= dns_types__packet_length_range__last .
H21:   number_bytes__1 >= dns_types__packet_length_range__first .
H22:   number_bytes__1 <= dns_types__packet_length_range__last .
H23:   true .
H24:   not failure__1 .
H25:   number_bytes__1 >= dns_types__packet_length_range__first .
H26:   number_bytes__1 <= dns_types__packet_length_range__last .
H27:   1 + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H28:   1 + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H29:   1 + dns_types__header_bits div 8 >= system__min_int .
H30:   1 + dns_types__header_bits div 8 <= system__max_int .
H31:   dns_types__header_bits div 8 >= system__min_int .
H32:   dns_types__header_bits div 8 <= system__max_int .
H33:   8 <> 0 .
        ->
C1:    (not ((number_bytes__1 < 1 + dns_types__header_bits div 8) or (
           number_bytes__1 > dns_network__max_query_size))) -> ((
           number_bytes__1 >= 1 + dns_types__header_bits div 8) and (
           number_bytes__1 <= dns_network__max_query_size)) .
 

procedure_receive_dns_packet_tcp_4.
H1:    true .
H2:    fld_length(packet__1) >= dns_types__unsigned_short__first .
H3:    fld_length(packet__1) <= dns_types__unsigned_short__last .
H4:    fld_messageid(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H5:    fld_messageid(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H6:    fld_opcode(fld_header(fld_rest(packet__1))) >= 
           dns_types__opcode_type__first .
H7:    fld_opcode(fld_header(fld_rest(packet__1))) <= 
           dns_types__opcode_type__last .
H8:    fld_rcode(fld_header(fld_rest(packet__1))) >= 
           dns_types__response_code__first .
H9:    fld_rcode(fld_header(fld_rest(packet__1))) <= 
           dns_types__response_code__last .
H10:   fld_qdcount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H11:   fld_qdcount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H12:   fld_ancount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H13:   fld_ancount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H14:   fld_nscount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H15:   fld_nscount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H16:   fld_arcount(fld_header(fld_rest(packet__1))) >= 
           dns_types__unsigned_short__first .
H17:   fld_arcount(fld_header(fld_rest(packet__1))) <= 
           dns_types__unsigned_short__last .
H18:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(fld_rest(packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           packet__1)), [i___1]) <= dns_types__byte__last))) .
H19:   number_bytes__1 >= dns_types__packet_length_range__first .
H20:   number_bytes__1 <= dns_types__packet_length_range__last .
H21:   number_bytes__1 >= dns_types__packet_length_range__first .
H22:   number_bytes__1 <= dns_types__packet_length_range__last .
H23:   true .
H24:   not (not failure__1) .
        ->
C1:    (not failure__1) -> ((number_bytes__1 >= 1 + 
           dns_types__header_bits div 8) and (number_bytes__1 <= 
           dns_network__max_query_size)) .
 

