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

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


             procedure Process_Dns_Request.Process_Request_Tcp




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

procedure_process_request_tcp_1.
H1:    true .
H2:    (not failure__1) -> ((input_bytes__1 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__1 <= 
           dns_network__max_query_size)) .
H3:    fld_length(input_packet__1) >= 
           dns_types__unsigned_short__first .
H4:    fld_length(input_packet__1) <= 
           dns_types__unsigned_short__last .
H5:    fld_messageid(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H6:    fld_messageid(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H7:    fld_opcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__opcode_type__first .
H8:    fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__opcode_type__last .
H9:    fld_rcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__response_code__first .
H10:   fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__response_code__last .
H11:   fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H12:   fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H13:   fld_ancount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H14:   fld_ancount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H15:   fld_nscount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H16:   fld_nscount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H17:   fld_arcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H18:   fld_arcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H19:   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(input_packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           input_packet__1)), [i___1]) <= dns_types__byte__last))) .
H20:   input_bytes__1 >= dns_types__packet_length_range__first .
H21:   input_bytes__1 <= dns_types__packet_length_range__last .
        ->
C1:    input_bytes__1 >= dns_types__packet_length_range__first .
C2:    input_bytes__1 <= dns_types__packet_length_range__last .
 

For path(s) from start to precondition check associated with statement of line 1584:

procedure_process_request_tcp_2.
H1:    true .
H2:    (not failure__1) -> ((input_bytes__1 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__1 <= 
           dns_network__max_query_size)) .
H3:    fld_length(input_packet__1) >= 
           dns_types__unsigned_short__first .
H4:    fld_length(input_packet__1) <= 
           dns_types__unsigned_short__last .
H5:    fld_messageid(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H6:    fld_messageid(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H7:    fld_opcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__opcode_type__first .
H8:    fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__opcode_type__last .
H9:    fld_rcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__response_code__first .
H10:   fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__response_code__last .
H11:   fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H12:   fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H13:   fld_ancount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H14:   fld_ancount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H15:   fld_nscount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H16:   fld_nscount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H17:   fld_arcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H18:   fld_arcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H19:   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(input_packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           input_packet__1)), [i___1]) <= dns_types__byte__last))) .
H20:   input_bytes__1 >= dns_types__packet_length_range__first .
H21:   input_bytes__1 <= dns_types__packet_length_range__last .
H22:   input_bytes__1 >= dns_types__packet_length_range__first .
H23:   input_bytes__1 <= dns_types__packet_length_range__last .
H24:   not failure__1 .
        ->
C1:    input_bytes__1 >= dns_types__packet_length_range__first .
C2:    input_bytes__1 <= dns_types__packet_length_range__last .
C3:    input_bytes__1 >= dns_types__header_bits div 8 + 1 .
C4:    input_bytes__1 < 312 .
 

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

procedure_process_request_tcp_3.
H1:    true .
H2:    (not failure__1) -> ((input_bytes__1 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__1 <= 
           dns_network__max_query_size)) .
H3:    fld_length(input_packet__1) >= 
           dns_types__unsigned_short__first .
H4:    fld_length(input_packet__1) <= 
           dns_types__unsigned_short__last .
H5:    fld_messageid(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H6:    fld_messageid(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H7:    fld_opcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__opcode_type__first .
H8:    fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__opcode_type__last .
H9:    fld_rcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__response_code__first .
H10:   fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__response_code__last .
H11:   fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H12:   fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H13:   fld_ancount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H14:   fld_ancount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H15:   fld_nscount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H16:   fld_nscount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H17:   fld_arcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H18:   fld_arcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H19:   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(input_packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           input_packet__1)), [i___1]) <= dns_types__byte__last))) .
H20:   input_bytes__1 >= dns_types__packet_length_range__first .
H21:   input_bytes__1 <= dns_types__packet_length_range__last .
H22:   input_bytes__1 >= dns_types__packet_length_range__first .
H23:   input_bytes__1 <= dns_types__packet_length_range__last .
H24:   not failure__1 .
H25:   input_bytes__1 >= dns_types__packet_length_range__first .
H26:   input_bytes__1 <= dns_types__packet_length_range__last .
H27:   input_bytes__1 >= dns_types__header_bits div 8 + 1 .
H28:   input_bytes__1 < 312 .
H29:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H30:   output_bytes__2 <= dns_types__packet_size .
H31:   max_transmit__2 <= dns_types__packet_size .
H32:   max_transmit__2 >= dns_types__udp_max_size .
H33:   fld_messageid(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H34:   fld_messageid(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H35:   fld_opcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__opcode_type__first .
H36:   fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__opcode_type__last .
H37:   fld_rcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__response_code__first .
H38:   fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__response_code__last .
H39:   fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H40:   fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H41:   fld_ancount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H42:   fld_ancount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H43:   fld_nscount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H44:   fld_nscount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H45:   fld_arcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H46:   fld_arcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H47:   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(output_packet__2)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__2)), [i___1]) <= dns_types__byte__last))) .
H48:   output_bytes__2 >= dns_types__packet_length_range__first .
H49:   output_bytes__2 <= dns_types__packet_length_range__last .
H50:   max_transmit__2 >= dns_types__packet_length_range__first .
H51:   max_transmit__2 <= dns_types__packet_length_range__last .
H52:   fld_length(output_packet__2) = fld_length(
           output_packet) .
H53:   output_packet__2 = upf_rest(output_packet, fld_rest(
           output_packet__2)) .
        ->
C1:    max_transmit__2 >= dns_types__packet_length_range__first .
C2:    max_transmit__2 <= dns_types__packet_length_range__last .
C3:    output_bytes__2 >= dns_types__packet_length_range__first .
C4:    output_bytes__2 <= dns_types__packet_length_range__last .
 

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

procedure_process_request_tcp_4.
H1:    true .
H2:    (not failure__1) -> ((input_bytes__1 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__1 <= 
           dns_network__max_query_size)) .
H3:    fld_length(input_packet__1) >= 
           dns_types__unsigned_short__first .
H4:    fld_length(input_packet__1) <= 
           dns_types__unsigned_short__last .
H5:    fld_messageid(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H6:    fld_messageid(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H7:    fld_opcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__opcode_type__first .
H8:    fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__opcode_type__last .
H9:    fld_rcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__response_code__first .
H10:   fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__response_code__last .
H11:   fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H12:   fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H13:   fld_ancount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H14:   fld_ancount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H15:   fld_nscount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H16:   fld_nscount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H17:   fld_arcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H18:   fld_arcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H19:   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(input_packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           input_packet__1)), [i___1]) <= dns_types__byte__last))) .
H20:   input_bytes__1 >= dns_types__packet_length_range__first .
H21:   input_bytes__1 <= dns_types__packet_length_range__last .
H22:   input_bytes__1 >= dns_types__packet_length_range__first .
H23:   input_bytes__1 <= dns_types__packet_length_range__last .
H24:   not failure__1 .
H25:   input_bytes__1 >= dns_types__packet_length_range__first .
H26:   input_bytes__1 <= dns_types__packet_length_range__last .
H27:   input_bytes__1 >= dns_types__header_bits div 8 + 1 .
H28:   input_bytes__1 < 312 .
H29:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H30:   output_bytes__2 <= dns_types__packet_size .
H31:   max_transmit__2 <= dns_types__packet_size .
H32:   max_transmit__2 >= dns_types__udp_max_size .
H33:   fld_messageid(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H34:   fld_messageid(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H35:   fld_opcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__opcode_type__first .
H36:   fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__opcode_type__last .
H37:   fld_rcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__response_code__first .
H38:   fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__response_code__last .
H39:   fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H40:   fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H41:   fld_ancount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H42:   fld_ancount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H43:   fld_nscount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H44:   fld_nscount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H45:   fld_arcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H46:   fld_arcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H47:   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(output_packet__2)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__2)), [i___1]) <= dns_types__byte__last))) .
H48:   output_bytes__2 >= dns_types__packet_length_range__first .
H49:   output_bytes__2 <= dns_types__packet_length_range__last .
H50:   max_transmit__2 >= dns_types__packet_length_range__first .
H51:   max_transmit__2 <= dns_types__packet_length_range__last .
H52:   fld_length(output_packet__2) = fld_length(
           output_packet) .
H53:   output_packet__2 = upf_rest(output_packet, fld_rest(
           output_packet__2)) .
H54:   max_transmit__2 >= dns_types__packet_length_range__first .
H55:   max_transmit__2 <= dns_types__packet_length_range__last .
H56:   output_bytes__2 >= dns_types__packet_length_range__first .
H57:   output_bytes__2 <= dns_types__packet_length_range__last .
H58:   system__default_bit_order = system__low_order_first .
        ->
C1:    output_bytes__2 >= dns_types__unsigned_short__first .
C2:    output_bytes__2 <= dns_types__unsigned_short__last .
C3:    output_bytes__2 >= dns_types__unsigned_short__first .
C4:    output_bytes__2 <= dns_types__unsigned_short__last .
 

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

procedure_process_request_tcp_5.
H1:    true .
H2:    (not failure__1) -> ((input_bytes__1 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__1 <= 
           dns_network__max_query_size)) .
H3:    fld_length(input_packet__1) >= 
           dns_types__unsigned_short__first .
H4:    fld_length(input_packet__1) <= 
           dns_types__unsigned_short__last .
H5:    fld_messageid(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H6:    fld_messageid(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H7:    fld_opcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__opcode_type__first .
H8:    fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__opcode_type__last .
H9:    fld_rcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__response_code__first .
H10:   fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__response_code__last .
H11:   fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H12:   fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H13:   fld_ancount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H14:   fld_ancount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H15:   fld_nscount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H16:   fld_nscount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H17:   fld_arcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H18:   fld_arcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H19:   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(input_packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           input_packet__1)), [i___1]) <= dns_types__byte__last))) .
H20:   input_bytes__1 >= dns_types__packet_length_range__first .
H21:   input_bytes__1 <= dns_types__packet_length_range__last .
H22:   input_bytes__1 >= dns_types__packet_length_range__first .
H23:   input_bytes__1 <= dns_types__packet_length_range__last .
H24:   not failure__1 .
H25:   input_bytes__1 >= dns_types__packet_length_range__first .
H26:   input_bytes__1 <= dns_types__packet_length_range__last .
H27:   input_bytes__1 >= dns_types__header_bits div 8 + 1 .
H28:   input_bytes__1 < 312 .
H29:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H30:   output_bytes__2 <= dns_types__packet_size .
H31:   max_transmit__2 <= dns_types__packet_size .
H32:   max_transmit__2 >= dns_types__udp_max_size .
H33:   fld_messageid(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H34:   fld_messageid(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H35:   fld_opcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__opcode_type__first .
H36:   fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__opcode_type__last .
H37:   fld_rcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__response_code__first .
H38:   fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__response_code__last .
H39:   fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H40:   fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H41:   fld_ancount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H42:   fld_ancount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H43:   fld_nscount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H44:   fld_nscount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H45:   fld_arcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H46:   fld_arcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H47:   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(output_packet__2)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__2)), [i___1]) <= dns_types__byte__last))) .
H48:   output_bytes__2 >= dns_types__packet_length_range__first .
H49:   output_bytes__2 <= dns_types__packet_length_range__last .
H50:   max_transmit__2 >= dns_types__packet_length_range__first .
H51:   max_transmit__2 <= dns_types__packet_length_range__last .
H52:   fld_length(output_packet__2) = fld_length(
           output_packet) .
H53:   output_packet__2 = upf_rest(output_packet, fld_rest(
           output_packet__2)) .
H54:   max_transmit__2 >= dns_types__packet_length_range__first .
H55:   max_transmit__2 <= dns_types__packet_length_range__last .
H56:   output_bytes__2 >= dns_types__packet_length_range__first .
H57:   output_bytes__2 <= dns_types__packet_length_range__last .
H58:   system__default_bit_order = system__low_order_first .
H59:   output_bytes__2 >= dns_types__unsigned_short__first .
H60:   output_bytes__2 <= dns_types__unsigned_short__last .
H61:   output_bytes__2 >= dns_types__unsigned_short__first .
H62:   output_bytes__2 <= dns_types__unsigned_short__last .
H63:   dns_types__byte_swap_us(output_bytes__2) >= 
           dns_types__unsigned_short__first .
H64:   dns_types__byte_swap_us(output_bytes__2) <= 
           dns_types__unsigned_short__last .
        ->
C1:    dns_types__byte_swap_us(output_bytes__2) >= 
           dns_types__unsigned_short__first .
C2:    dns_types__byte_swap_us(output_bytes__2) <= 
           dns_types__unsigned_short__last .
 

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

procedure_process_request_tcp_6.
H1:    true .
H2:    (not failure__1) -> ((input_bytes__1 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__1 <= 
           dns_network__max_query_size)) .
H3:    fld_length(input_packet__1) >= 
           dns_types__unsigned_short__first .
H4:    fld_length(input_packet__1) <= 
           dns_types__unsigned_short__last .
H5:    fld_messageid(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H6:    fld_messageid(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H7:    fld_opcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__opcode_type__first .
H8:    fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__opcode_type__last .
H9:    fld_rcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__response_code__first .
H10:   fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__response_code__last .
H11:   fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H12:   fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H13:   fld_ancount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H14:   fld_ancount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H15:   fld_nscount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H16:   fld_nscount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H17:   fld_arcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H18:   fld_arcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H19:   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(input_packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           input_packet__1)), [i___1]) <= dns_types__byte__last))) .
H20:   input_bytes__1 >= dns_types__packet_length_range__first .
H21:   input_bytes__1 <= dns_types__packet_length_range__last .
H22:   input_bytes__1 >= dns_types__packet_length_range__first .
H23:   input_bytes__1 <= dns_types__packet_length_range__last .
H24:   not failure__1 .
H25:   input_bytes__1 >= dns_types__packet_length_range__first .
H26:   input_bytes__1 <= dns_types__packet_length_range__last .
H27:   input_bytes__1 >= dns_types__header_bits div 8 + 1 .
H28:   input_bytes__1 < 312 .
H29:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H30:   output_bytes__2 <= dns_types__packet_size .
H31:   max_transmit__2 <= dns_types__packet_size .
H32:   max_transmit__2 >= dns_types__udp_max_size .
H33:   fld_messageid(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H34:   fld_messageid(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H35:   fld_opcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__opcode_type__first .
H36:   fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__opcode_type__last .
H37:   fld_rcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__response_code__first .
H38:   fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__response_code__last .
H39:   fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H40:   fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H41:   fld_ancount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H42:   fld_ancount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H43:   fld_nscount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H44:   fld_nscount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H45:   fld_arcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H46:   fld_arcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H47:   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(output_packet__2)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__2)), [i___1]) <= dns_types__byte__last))) .
H48:   output_bytes__2 >= dns_types__packet_length_range__first .
H49:   output_bytes__2 <= dns_types__packet_length_range__last .
H50:   max_transmit__2 >= dns_types__packet_length_range__first .
H51:   max_transmit__2 <= dns_types__packet_length_range__last .
H52:   fld_length(output_packet__2) = fld_length(
           output_packet) .
H53:   output_packet__2 = upf_rest(output_packet, fld_rest(
           output_packet__2)) .
H54:   max_transmit__2 >= dns_types__packet_length_range__first .
H55:   max_transmit__2 <= dns_types__packet_length_range__last .
H56:   output_bytes__2 >= dns_types__packet_length_range__first .
H57:   output_bytes__2 <= dns_types__packet_length_range__last .
H58:   not (system__default_bit_order = 
           system__low_order_first) .
        ->
C1:    output_bytes__2 >= dns_types__unsigned_short__first .
C2:    output_bytes__2 <= dns_types__unsigned_short__last .
C3:    output_bytes__2 >= dns_types__unsigned_short__first .
C4:    output_bytes__2 <= dns_types__unsigned_short__last .
 

For path(s) from start to precondition check associated with statement of line 1607:

procedure_process_request_tcp_7.
H1:    true .
H2:    (not failure__1) -> ((input_bytes__1 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__1 <= 
           dns_network__max_query_size)) .
H3:    fld_length(input_packet__1) >= 
           dns_types__unsigned_short__first .
H4:    fld_length(input_packet__1) <= 
           dns_types__unsigned_short__last .
H5:    fld_messageid(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H6:    fld_messageid(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H7:    fld_opcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__opcode_type__first .
H8:    fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__opcode_type__last .
H9:    fld_rcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__response_code__first .
H10:   fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__response_code__last .
H11:   fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H12:   fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H13:   fld_ancount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H14:   fld_ancount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H15:   fld_nscount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H16:   fld_nscount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H17:   fld_arcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H18:   fld_arcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H19:   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(input_packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           input_packet__1)), [i___1]) <= dns_types__byte__last))) .
H20:   input_bytes__1 >= dns_types__packet_length_range__first .
H21:   input_bytes__1 <= dns_types__packet_length_range__last .
H22:   input_bytes__1 >= dns_types__packet_length_range__first .
H23:   input_bytes__1 <= dns_types__packet_length_range__last .
H24:   not failure__1 .
H25:   input_bytes__1 >= dns_types__packet_length_range__first .
H26:   input_bytes__1 <= dns_types__packet_length_range__last .
H27:   input_bytes__1 >= dns_types__header_bits div 8 + 1 .
H28:   input_bytes__1 < 312 .
H29:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H30:   output_bytes__2 <= dns_types__packet_size .
H31:   max_transmit__2 <= dns_types__packet_size .
H32:   max_transmit__2 >= dns_types__udp_max_size .
H33:   fld_messageid(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H34:   fld_messageid(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H35:   fld_opcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__opcode_type__first .
H36:   fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__opcode_type__last .
H37:   fld_rcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__response_code__first .
H38:   fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__response_code__last .
H39:   fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H40:   fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H41:   fld_ancount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H42:   fld_ancount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H43:   fld_nscount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H44:   fld_nscount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H45:   fld_arcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H46:   fld_arcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H47:   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(output_packet__2)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__2)), [i___1]) <= dns_types__byte__last))) .
H48:   output_bytes__2 >= dns_types__packet_length_range__first .
H49:   output_bytes__2 <= dns_types__packet_length_range__last .
H50:   max_transmit__2 >= dns_types__packet_length_range__first .
H51:   max_transmit__2 <= dns_types__packet_length_range__last .
H52:   fld_length(output_packet__2) = fld_length(
           output_packet) .
H53:   output_packet__2 = upf_rest(output_packet, fld_rest(
           output_packet__2)) .
H54:   max_transmit__2 >= dns_types__packet_length_range__first .
H55:   max_transmit__2 <= dns_types__packet_length_range__last .
H56:   output_bytes__2 >= dns_types__packet_length_range__first .
H57:   output_bytes__2 <= dns_types__packet_length_range__last .
H58:   system__default_bit_order = system__low_order_first .
H59:   output_bytes__2 >= dns_types__unsigned_short__first .
H60:   output_bytes__2 <= dns_types__unsigned_short__last .
H61:   output_bytes__2 >= dns_types__unsigned_short__first .
H62:   output_bytes__2 <= dns_types__unsigned_short__last .
H63:   dns_types__byte_swap_us(output_bytes__2) >= 
           dns_types__unsigned_short__first .
H64:   dns_types__byte_swap_us(output_bytes__2) <= 
           dns_types__unsigned_short__last .
H65:   dns_types__byte_swap_us(output_bytes__2) >= 
           dns_types__unsigned_short__first .
H66:   dns_types__byte_swap_us(output_bytes__2) <= 
           dns_types__unsigned_short__last .
        ->
C1:    output_bytes__2 >= dns_types__packet_length_range__first .
C2:    output_bytes__2 <= dns_types__packet_length_range__last .
C3:    output_bytes__2 > dns_types__header_bits div 8 .
 

procedure_process_request_tcp_8.
H1:    true .
H2:    (not failure__1) -> ((input_bytes__1 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__1 <= 
           dns_network__max_query_size)) .
H3:    fld_length(input_packet__1) >= 
           dns_types__unsigned_short__first .
H4:    fld_length(input_packet__1) <= 
           dns_types__unsigned_short__last .
H5:    fld_messageid(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H6:    fld_messageid(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H7:    fld_opcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__opcode_type__first .
H8:    fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__opcode_type__last .
H9:    fld_rcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__response_code__first .
H10:   fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__response_code__last .
H11:   fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H12:   fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H13:   fld_ancount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H14:   fld_ancount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H15:   fld_nscount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H16:   fld_nscount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H17:   fld_arcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H18:   fld_arcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H19:   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(input_packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           input_packet__1)), [i___1]) <= dns_types__byte__last))) .
H20:   input_bytes__1 >= dns_types__packet_length_range__first .
H21:   input_bytes__1 <= dns_types__packet_length_range__last .
H22:   input_bytes__1 >= dns_types__packet_length_range__first .
H23:   input_bytes__1 <= dns_types__packet_length_range__last .
H24:   not failure__1 .
H25:   input_bytes__1 >= dns_types__packet_length_range__first .
H26:   input_bytes__1 <= dns_types__packet_length_range__last .
H27:   input_bytes__1 >= dns_types__header_bits div 8 + 1 .
H28:   input_bytes__1 < 312 .
H29:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H30:   output_bytes__2 <= dns_types__packet_size .
H31:   max_transmit__2 <= dns_types__packet_size .
H32:   max_transmit__2 >= dns_types__udp_max_size .
H33:   fld_messageid(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H34:   fld_messageid(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H35:   fld_opcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__opcode_type__first .
H36:   fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__opcode_type__last .
H37:   fld_rcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__response_code__first .
H38:   fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__response_code__last .
H39:   fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H40:   fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H41:   fld_ancount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H42:   fld_ancount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H43:   fld_nscount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H44:   fld_nscount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H45:   fld_arcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H46:   fld_arcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H47:   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(output_packet__2)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__2)), [i___1]) <= dns_types__byte__last))) .
H48:   output_bytes__2 >= dns_types__packet_length_range__first .
H49:   output_bytes__2 <= dns_types__packet_length_range__last .
H50:   max_transmit__2 >= dns_types__packet_length_range__first .
H51:   max_transmit__2 <= dns_types__packet_length_range__last .
H52:   fld_length(output_packet__2) = fld_length(
           output_packet) .
H53:   output_packet__2 = upf_rest(output_packet, fld_rest(
           output_packet__2)) .
H54:   max_transmit__2 >= dns_types__packet_length_range__first .
H55:   max_transmit__2 <= dns_types__packet_length_range__last .
H56:   output_bytes__2 >= dns_types__packet_length_range__first .
H57:   output_bytes__2 <= dns_types__packet_length_range__last .
H58:   not (system__default_bit_order = 
           system__low_order_first) .
H59:   output_bytes__2 >= dns_types__unsigned_short__first .
H60:   output_bytes__2 <= dns_types__unsigned_short__last .
H61:   output_bytes__2 >= dns_types__unsigned_short__first .
H62:   output_bytes__2 <= dns_types__unsigned_short__last .
        ->
C1:    output_bytes__2 >= dns_types__packet_length_range__first .
C2:    output_bytes__2 <= dns_types__packet_length_range__last .
C3:    output_bytes__2 > dns_types__header_bits div 8 .
 

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

procedure_process_request_tcp_9.
H1:    true .
H2:    (not failure__1) -> ((input_bytes__1 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__1 <= 
           dns_network__max_query_size)) .
H3:    fld_length(input_packet__1) >= 
           dns_types__unsigned_short__first .
H4:    fld_length(input_packet__1) <= 
           dns_types__unsigned_short__last .
H5:    fld_messageid(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H6:    fld_messageid(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H7:    fld_opcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__opcode_type__first .
H8:    fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__opcode_type__last .
H9:    fld_rcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__response_code__first .
H10:   fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__response_code__last .
H11:   fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H12:   fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H13:   fld_ancount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H14:   fld_ancount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H15:   fld_nscount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H16:   fld_nscount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H17:   fld_arcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H18:   fld_arcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H19:   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(input_packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           input_packet__1)), [i___1]) <= dns_types__byte__last))) .
H20:   input_bytes__1 >= dns_types__packet_length_range__first .
H21:   input_bytes__1 <= dns_types__packet_length_range__last .
H22:   input_bytes__1 >= dns_types__packet_length_range__first .
H23:   input_bytes__1 <= dns_types__packet_length_range__last .
H24:   not failure__1 .
H25:   input_bytes__1 >= dns_types__packet_length_range__first .
H26:   input_bytes__1 <= dns_types__packet_length_range__last .
H27:   input_bytes__1 >= dns_types__header_bits div 8 + 1 .
H28:   input_bytes__1 < 312 .
H29:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H30:   output_bytes__2 <= dns_types__packet_size .
H31:   max_transmit__2 <= dns_types__packet_size .
H32:   max_transmit__2 >= dns_types__udp_max_size .
H33:   fld_messageid(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H34:   fld_messageid(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H35:   fld_opcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__opcode_type__first .
H36:   fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__opcode_type__last .
H37:   fld_rcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__response_code__first .
H38:   fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__response_code__last .
H39:   fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H40:   fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H41:   fld_ancount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H42:   fld_ancount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H43:   fld_nscount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H44:   fld_nscount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H45:   fld_arcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H46:   fld_arcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H47:   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(output_packet__2)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__2)), [i___1]) <= dns_types__byte__last))) .
H48:   output_bytes__2 >= dns_types__packet_length_range__first .
H49:   output_bytes__2 <= dns_types__packet_length_range__last .
H50:   max_transmit__2 >= dns_types__packet_length_range__first .
H51:   max_transmit__2 <= dns_types__packet_length_range__last .
H52:   fld_length(output_packet__2) = fld_length(
           output_packet) .
H53:   output_packet__2 = upf_rest(output_packet, fld_rest(
           output_packet__2)) .
H54:   max_transmit__2 >= dns_types__packet_length_range__first .
H55:   max_transmit__2 <= dns_types__packet_length_range__last .
H56:   output_bytes__2 >= dns_types__packet_length_range__first .
H57:   output_bytes__2 <= dns_types__packet_length_range__last .
H58:   system__default_bit_order = system__low_order_first .
H59:   output_bytes__2 >= dns_types__unsigned_short__first .
H60:   output_bytes__2 <= dns_types__unsigned_short__last .
H61:   output_bytes__2 >= dns_types__unsigned_short__first .
H62:   output_bytes__2 <= dns_types__unsigned_short__last .
H63:   dns_types__byte_swap_us(output_bytes__2) >= 
           dns_types__unsigned_short__first .
H64:   dns_types__byte_swap_us(output_bytes__2) <= 
           dns_types__unsigned_short__last .
H65:   dns_types__byte_swap_us(output_bytes__2) >= 
           dns_types__unsigned_short__first .
H66:   dns_types__byte_swap_us(output_bytes__2) <= 
           dns_types__unsigned_short__last .
H67:   output_bytes__2 >= dns_types__packet_length_range__first .
H68:   output_bytes__2 <= dns_types__packet_length_range__last .
H69:   output_bytes__2 > dns_types__header_bits div 8 .
H70:   (system__default_bit_order = system__high_order_first) -> (
           output_packet__3 = upf_length(output_packet__2, 
           dns_types__byte_swap_us(output_bytes__2))) .
H71:   fld_length(output_packet__3) >= 
           dns_types__unsigned_short__first .
H72:   fld_length(output_packet__3) <= 
           dns_types__unsigned_short__last .
H73:   fld_messageid(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H74:   fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H75:   fld_opcode(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__opcode_type__first .
H76:   fld_opcode(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__opcode_type__last .
H77:   fld_rcode(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__response_code__first .
H78:   fld_rcode(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__response_code__last .
H79:   fld_qdcount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H80:   fld_qdcount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H81:   fld_ancount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H82:   fld_ancount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H83:   fld_nscount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H84:   fld_nscount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H85:   fld_arcount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H86:   fld_arcount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H87:   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(output_packet__3)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__3)), [i___1]) <= dns_types__byte__last))) .
H88:   failure__3 .
H89:   true .
        ->
C1:    16 >= protected_spark_io_05__number_base__first .
C2:    16 <= protected_spark_io_05__number_base__last .
C3:    0 >= natural__first .
C4:    0 <= natural__last .
C5:    fld_messageid(fld_header(fld_rest(output_packet__3))) >= 
           integer__first .
C6:    fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
           integer__last .
C7:    fld_messageid(fld_header(fld_rest(output_packet__3))) >= 
           integer__first .
C8:    fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
           integer__last .
 

procedure_process_request_tcp_10.
H1:    true .
H2:    (not failure__1) -> ((input_bytes__1 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__1 <= 
           dns_network__max_query_size)) .
H3:    fld_length(input_packet__1) >= 
           dns_types__unsigned_short__first .
H4:    fld_length(input_packet__1) <= 
           dns_types__unsigned_short__last .
H5:    fld_messageid(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H6:    fld_messageid(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H7:    fld_opcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__opcode_type__first .
H8:    fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__opcode_type__last .
H9:    fld_rcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__response_code__first .
H10:   fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__response_code__last .
H11:   fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H12:   fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H13:   fld_ancount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H14:   fld_ancount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H15:   fld_nscount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H16:   fld_nscount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H17:   fld_arcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H18:   fld_arcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H19:   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(input_packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           input_packet__1)), [i___1]) <= dns_types__byte__last))) .
H20:   input_bytes__1 >= dns_types__packet_length_range__first .
H21:   input_bytes__1 <= dns_types__packet_length_range__last .
H22:   input_bytes__1 >= dns_types__packet_length_range__first .
H23:   input_bytes__1 <= dns_types__packet_length_range__last .
H24:   not failure__1 .
H25:   input_bytes__1 >= dns_types__packet_length_range__first .
H26:   input_bytes__1 <= dns_types__packet_length_range__last .
H27:   input_bytes__1 >= dns_types__header_bits div 8 + 1 .
H28:   input_bytes__1 < 312 .
H29:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H30:   output_bytes__2 <= dns_types__packet_size .
H31:   max_transmit__2 <= dns_types__packet_size .
H32:   max_transmit__2 >= dns_types__udp_max_size .
H33:   fld_messageid(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H34:   fld_messageid(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H35:   fld_opcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__opcode_type__first .
H36:   fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__opcode_type__last .
H37:   fld_rcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__response_code__first .
H38:   fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__response_code__last .
H39:   fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H40:   fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H41:   fld_ancount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H42:   fld_ancount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H43:   fld_nscount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H44:   fld_nscount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H45:   fld_arcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H46:   fld_arcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H47:   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(output_packet__2)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__2)), [i___1]) <= dns_types__byte__last))) .
H48:   output_bytes__2 >= dns_types__packet_length_range__first .
H49:   output_bytes__2 <= dns_types__packet_length_range__last .
H50:   max_transmit__2 >= dns_types__packet_length_range__first .
H51:   max_transmit__2 <= dns_types__packet_length_range__last .
H52:   fld_length(output_packet__2) = fld_length(
           output_packet) .
H53:   output_packet__2 = upf_rest(output_packet, fld_rest(
           output_packet__2)) .
H54:   max_transmit__2 >= dns_types__packet_length_range__first .
H55:   max_transmit__2 <= dns_types__packet_length_range__last .
H56:   output_bytes__2 >= dns_types__packet_length_range__first .
H57:   output_bytes__2 <= dns_types__packet_length_range__last .
H58:   not (system__default_bit_order = 
           system__low_order_first) .
H59:   output_bytes__2 >= dns_types__unsigned_short__first .
H60:   output_bytes__2 <= dns_types__unsigned_short__last .
H61:   output_bytes__2 >= dns_types__unsigned_short__first .
H62:   output_bytes__2 <= dns_types__unsigned_short__last .
H63:   output_bytes__2 >= dns_types__packet_length_range__first .
H64:   output_bytes__2 <= dns_types__packet_length_range__last .
H65:   output_bytes__2 > dns_types__header_bits div 8 .
H66:   (system__default_bit_order = system__high_order_first) -> (
           output_packet__3 = upf_length(output_packet__2, 
           output_bytes__2)) .
H67:   fld_length(output_packet__3) >= 
           dns_types__unsigned_short__first .
H68:   fld_length(output_packet__3) <= 
           dns_types__unsigned_short__last .
H69:   fld_messageid(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H70:   fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H71:   fld_opcode(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__opcode_type__first .
H72:   fld_opcode(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__opcode_type__last .
H73:   fld_rcode(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__response_code__first .
H74:   fld_rcode(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__response_code__last .
H75:   fld_qdcount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H76:   fld_qdcount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H77:   fld_ancount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H78:   fld_ancount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H79:   fld_nscount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H80:   fld_nscount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H81:   fld_arcount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H82:   fld_arcount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H83:   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(output_packet__3)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__3)), [i___1]) <= dns_types__byte__last))) .
H84:   failure__3 .
H85:   true .
        ->
C1:    16 >= protected_spark_io_05__number_base__first .
C2:    16 <= protected_spark_io_05__number_base__last .
C3:    0 >= natural__first .
C4:    0 <= natural__last .
C5:    fld_messageid(fld_header(fld_rest(output_packet__3))) >= 
           integer__first .
C6:    fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
           integer__last .
C7:    fld_messageid(fld_header(fld_rest(output_packet__3))) >= 
           integer__first .
C8:    fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
           integer__last .
 

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

procedure_process_request_tcp_11.
H1:    true .
H2:    (not failure__1) -> ((input_bytes__1 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__1 <= 
           dns_network__max_query_size)) .
H3:    fld_length(input_packet__1) >= 
           dns_types__unsigned_short__first .
H4:    fld_length(input_packet__1) <= 
           dns_types__unsigned_short__last .
H5:    fld_messageid(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H6:    fld_messageid(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H7:    fld_opcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__opcode_type__first .
H8:    fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__opcode_type__last .
H9:    fld_rcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__response_code__first .
H10:   fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__response_code__last .
H11:   fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H12:   fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H13:   fld_ancount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H14:   fld_ancount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H15:   fld_nscount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H16:   fld_nscount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H17:   fld_arcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H18:   fld_arcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H19:   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(input_packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           input_packet__1)), [i___1]) <= dns_types__byte__last))) .
H20:   input_bytes__1 >= dns_types__packet_length_range__first .
H21:   input_bytes__1 <= dns_types__packet_length_range__last .
H22:   input_bytes__1 >= dns_types__packet_length_range__first .
H23:   input_bytes__1 <= dns_types__packet_length_range__last .
H24:   not failure__1 .
H25:   input_bytes__1 >= dns_types__packet_length_range__first .
H26:   input_bytes__1 <= dns_types__packet_length_range__last .
H27:   input_bytes__1 >= dns_types__header_bits div 8 + 1 .
H28:   input_bytes__1 < 312 .
H29:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H30:   output_bytes__2 <= dns_types__packet_size .
H31:   max_transmit__2 <= dns_types__packet_size .
H32:   max_transmit__2 >= dns_types__udp_max_size .
H33:   fld_messageid(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H34:   fld_messageid(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H35:   fld_opcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__opcode_type__first .
H36:   fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__opcode_type__last .
H37:   fld_rcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__response_code__first .
H38:   fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__response_code__last .
H39:   fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H40:   fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H41:   fld_ancount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H42:   fld_ancount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H43:   fld_nscount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H44:   fld_nscount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H45:   fld_arcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H46:   fld_arcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H47:   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(output_packet__2)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__2)), [i___1]) <= dns_types__byte__last))) .
H48:   output_bytes__2 >= dns_types__packet_length_range__first .
H49:   output_bytes__2 <= dns_types__packet_length_range__last .
H50:   max_transmit__2 >= dns_types__packet_length_range__first .
H51:   max_transmit__2 <= dns_types__packet_length_range__last .
H52:   fld_length(output_packet__2) = fld_length(
           output_packet) .
H53:   output_packet__2 = upf_rest(output_packet, fld_rest(
           output_packet__2)) .
H54:   max_transmit__2 >= dns_types__packet_length_range__first .
H55:   max_transmit__2 <= dns_types__packet_length_range__last .
H56:   output_bytes__2 >= dns_types__packet_length_range__first .
H57:   output_bytes__2 <= dns_types__packet_length_range__last .
H58:   system__default_bit_order = system__low_order_first .
H59:   output_bytes__2 >= dns_types__unsigned_short__first .
H60:   output_bytes__2 <= dns_types__unsigned_short__last .
H61:   output_bytes__2 >= dns_types__unsigned_short__first .
H62:   output_bytes__2 <= dns_types__unsigned_short__last .
H63:   dns_types__byte_swap_us(output_bytes__2) >= 
           dns_types__unsigned_short__first .
H64:   dns_types__byte_swap_us(output_bytes__2) <= 
           dns_types__unsigned_short__last .
H65:   dns_types__byte_swap_us(output_bytes__2) >= 
           dns_types__unsigned_short__first .
H66:   dns_types__byte_swap_us(output_bytes__2) <= 
           dns_types__unsigned_short__last .
H67:   output_bytes__2 >= dns_types__packet_length_range__first .
H68:   output_bytes__2 <= dns_types__packet_length_range__last .
H69:   output_bytes__2 > dns_types__header_bits div 8 .
H70:   (system__default_bit_order = system__high_order_first) -> (
           output_packet__3 = upf_length(output_packet__2, 
           dns_types__byte_swap_us(output_bytes__2))) .
H71:   fld_length(output_packet__3) >= 
           dns_types__unsigned_short__first .
H72:   fld_length(output_packet__3) <= 
           dns_types__unsigned_short__last .
H73:   fld_messageid(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H74:   fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H75:   fld_opcode(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__opcode_type__first .
H76:   fld_opcode(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__opcode_type__last .
H77:   fld_rcode(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__response_code__first .
H78:   fld_rcode(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__response_code__last .
H79:   fld_qdcount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H80:   fld_qdcount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H81:   fld_ancount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H82:   fld_ancount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H83:   fld_nscount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H84:   fld_nscount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H85:   fld_arcount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H86:   fld_arcount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H87:   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(output_packet__3)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__3)), [i___1]) <= dns_types__byte__last))) .
H88:   failure__3 .
H89:   true .
H90:   16 >= protected_spark_io_05__number_base__first .
H91:   16 <= protected_spark_io_05__number_base__last .
H92:   0 >= natural__first .
H93:   0 <= natural__last .
H94:   fld_messageid(fld_header(fld_rest(output_packet__3))) >= 
           integer__first .
H95:   fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
           integer__last .
H96:   fld_messageid(fld_header(fld_rest(output_packet__3))) >= 
           integer__first .
H97:   fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
           integer__last .
H98:   true .
        ->
C1:    0 >= natural__first .
C2:    0 <= natural__last .
 

procedure_process_request_tcp_12.
H1:    true .
H2:    (not failure__1) -> ((input_bytes__1 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__1 <= 
           dns_network__max_query_size)) .
H3:    fld_length(input_packet__1) >= 
           dns_types__unsigned_short__first .
H4:    fld_length(input_packet__1) <= 
           dns_types__unsigned_short__last .
H5:    fld_messageid(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H6:    fld_messageid(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H7:    fld_opcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__opcode_type__first .
H8:    fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__opcode_type__last .
H9:    fld_rcode(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__response_code__first .
H10:   fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__response_code__last .
H11:   fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H12:   fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H13:   fld_ancount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H14:   fld_ancount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H15:   fld_nscount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H16:   fld_nscount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H17:   fld_arcount(fld_header(fld_rest(input_packet__1))) >= 
           dns_types__unsigned_short__first .
H18:   fld_arcount(fld_header(fld_rest(input_packet__1))) <= 
           dns_types__unsigned_short__last .
H19:   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(input_packet__1)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           input_packet__1)), [i___1]) <= dns_types__byte__last))) .
H20:   input_bytes__1 >= dns_types__packet_length_range__first .
H21:   input_bytes__1 <= dns_types__packet_length_range__last .
H22:   input_bytes__1 >= dns_types__packet_length_range__first .
H23:   input_bytes__1 <= dns_types__packet_length_range__last .
H24:   not failure__1 .
H25:   input_bytes__1 >= dns_types__packet_length_range__first .
H26:   input_bytes__1 <= dns_types__packet_length_range__last .
H27:   input_bytes__1 >= dns_types__header_bits div 8 + 1 .
H28:   input_bytes__1 < 312 .
H29:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H30:   output_bytes__2 <= dns_types__packet_size .
H31:   max_transmit__2 <= dns_types__packet_size .
H32:   max_transmit__2 >= dns_types__udp_max_size .
H33:   fld_messageid(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H34:   fld_messageid(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H35:   fld_opcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__opcode_type__first .
H36:   fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__opcode_type__last .
H37:   fld_rcode(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__response_code__first .
H38:   fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__response_code__last .
H39:   fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H40:   fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H41:   fld_ancount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H42:   fld_ancount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H43:   fld_nscount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H44:   fld_nscount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H45:   fld_arcount(fld_header(fld_rest(output_packet__2))) >= 
           dns_types__unsigned_short__first .
H46:   fld_arcount(fld_header(fld_rest(output_packet__2))) <= 
           dns_types__unsigned_short__last .
H47:   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(output_packet__2)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__2)), [i___1]) <= dns_types__byte__last))) .
H48:   output_bytes__2 >= dns_types__packet_length_range__first .
H49:   output_bytes__2 <= dns_types__packet_length_range__last .
H50:   max_transmit__2 >= dns_types__packet_length_range__first .
H51:   max_transmit__2 <= dns_types__packet_length_range__last .
H52:   fld_length(output_packet__2) = fld_length(
           output_packet) .
H53:   output_packet__2 = upf_rest(output_packet, fld_rest(
           output_packet__2)) .
H54:   max_transmit__2 >= dns_types__packet_length_range__first .
H55:   max_transmit__2 <= dns_types__packet_length_range__last .
H56:   output_bytes__2 >= dns_types__packet_length_range__first .
H57:   output_bytes__2 <= dns_types__packet_length_range__last .
H58:   not (system__default_bit_order = 
           system__low_order_first) .
H59:   output_bytes__2 >= dns_types__unsigned_short__first .
H60:   output_bytes__2 <= dns_types__unsigned_short__last .
H61:   output_bytes__2 >= dns_types__unsigned_short__first .
H62:   output_bytes__2 <= dns_types__unsigned_short__last .
H63:   output_bytes__2 >= dns_types__packet_length_range__first .
H64:   output_bytes__2 <= dns_types__packet_length_range__last .
H65:   output_bytes__2 > dns_types__header_bits div 8 .
H66:   (system__default_bit_order = system__high_order_first) -> (
           output_packet__3 = upf_length(output_packet__2, 
           output_bytes__2)) .
H67:   fld_length(output_packet__3) >= 
           dns_types__unsigned_short__first .
H68:   fld_length(output_packet__3) <= 
           dns_types__unsigned_short__last .
H69:   fld_messageid(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H70:   fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H71:   fld_opcode(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__opcode_type__first .
H72:   fld_opcode(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__opcode_type__last .
H73:   fld_rcode(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__response_code__first .
H74:   fld_rcode(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__response_code__last .
H75:   fld_qdcount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H76:   fld_qdcount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H77:   fld_ancount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H78:   fld_ancount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H79:   fld_nscount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H80:   fld_nscount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H81:   fld_arcount(fld_header(fld_rest(output_packet__3))) >= 
           dns_types__unsigned_short__first .
H82:   fld_arcount(fld_header(fld_rest(output_packet__3))) <= 
           dns_types__unsigned_short__last .
H83:   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(output_packet__3)), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(fld_rest(
           output_packet__3)), [i___1]) <= dns_types__byte__last))) .
H84:   failure__3 .
H85:   true .
H86:   16 >= protected_spark_io_05__number_base__first .
H87:   16 <= protected_spark_io_05__number_base__last .
H88:   0 >= natural__first .
H89:   0 <= natural__last .
H90:   fld_messageid(fld_header(fld_rest(output_packet__3))) >= 
           integer__first .
H91:   fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
           integer__last .
H92:   fld_messageid(fld_header(fld_rest(output_packet__3))) >= 
           integer__first .
H93:   fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
           integer__last .
H94:   true .
        ->
C1:    0 >= natural__first .
C2:    0 <= natural__last .
 

For path(s) from start to finish:

procedure_process_request_tcp_13.
*** true .          /* trivially true VC removed by Examiner */


procedure_process_request_tcp_14.
*** true .          /* trivially true VC removed by Examiner */


procedure_process_request_tcp_15.
*** true .          /* trivially true VC removed by Examiner */


procedure_process_request_tcp_16.
*** true .          /* trivially true VC removed by Examiner */


procedure_process_request_tcp_17.
*** true .          /* trivially true VC removed by Examiner */


