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

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


                       procedure DNS_Types.Byte_Swap




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

procedure_byte_swap_1.
H1:    fld_messageid(h) >= unsigned_short__first .
H2:    fld_messageid(h) <= unsigned_short__last .
H3:    fld_opcode(h) >= opcode_type__first .
H4:    fld_opcode(h) <= opcode_type__last .
H5:    fld_rcode(h) >= response_code__first .
H6:    fld_rcode(h) <= response_code__last .
H7:    fld_qdcount(h) >= unsigned_short__first .
H8:    fld_qdcount(h) <= unsigned_short__last .
H9:    fld_ancount(h) >= unsigned_short__first .
H10:   fld_ancount(h) <= unsigned_short__last .
H11:   fld_nscount(h) >= unsigned_short__first .
H12:   fld_nscount(h) <= unsigned_short__last .
H13:   fld_arcount(h) >= unsigned_short__first .
H14:   fld_arcount(h) <= unsigned_short__last .
        ->
C1:    fld_messageid(h) >= unsigned_short__first .
C2:    fld_messageid(h) <= unsigned_short__last .
 

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

procedure_byte_swap_2.
H1:    fld_messageid(h) >= unsigned_short__first .
H2:    fld_messageid(h) <= unsigned_short__last .
H3:    fld_opcode(h) >= opcode_type__first .
H4:    fld_opcode(h) <= opcode_type__last .
H5:    fld_rcode(h) >= response_code__first .
H6:    fld_rcode(h) <= response_code__last .
H7:    fld_qdcount(h) >= unsigned_short__first .
H8:    fld_qdcount(h) <= unsigned_short__last .
H9:    fld_ancount(h) >= unsigned_short__first .
H10:   fld_ancount(h) <= unsigned_short__last .
H11:   fld_nscount(h) >= unsigned_short__first .
H12:   fld_nscount(h) <= unsigned_short__last .
H13:   fld_arcount(h) >= unsigned_short__first .
H14:   fld_arcount(h) <= unsigned_short__last .
H15:   fld_messageid(h) >= unsigned_short__first .
H16:   fld_messageid(h) <= unsigned_short__last .
H17:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H18:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
        ->
C1:    byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
C2:    byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
 

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

procedure_byte_swap_3.
H1:    fld_messageid(h) >= unsigned_short__first .
H2:    fld_messageid(h) <= unsigned_short__last .
H3:    fld_opcode(h) >= opcode_type__first .
H4:    fld_opcode(h) <= opcode_type__last .
H5:    fld_rcode(h) >= response_code__first .
H6:    fld_rcode(h) <= response_code__last .
H7:    fld_qdcount(h) >= unsigned_short__first .
H8:    fld_qdcount(h) <= unsigned_short__last .
H9:    fld_ancount(h) >= unsigned_short__first .
H10:   fld_ancount(h) <= unsigned_short__last .
H11:   fld_nscount(h) >= unsigned_short__first .
H12:   fld_nscount(h) <= unsigned_short__last .
H13:   fld_arcount(h) >= unsigned_short__first .
H14:   fld_arcount(h) <= unsigned_short__last .
H15:   fld_messageid(h) >= unsigned_short__first .
H16:   fld_messageid(h) <= unsigned_short__last .
H17:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H18:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H19:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H20:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
        ->
C1:    fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) >= unsigned_short__first .
C2:    fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) <= unsigned_short__last .
 

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

procedure_byte_swap_4.
H1:    fld_messageid(h) >= unsigned_short__first .
H2:    fld_messageid(h) <= unsigned_short__last .
H3:    fld_opcode(h) >= opcode_type__first .
H4:    fld_opcode(h) <= opcode_type__last .
H5:    fld_rcode(h) >= response_code__first .
H6:    fld_rcode(h) <= response_code__last .
H7:    fld_qdcount(h) >= unsigned_short__first .
H8:    fld_qdcount(h) <= unsigned_short__last .
H9:    fld_ancount(h) >= unsigned_short__first .
H10:   fld_ancount(h) <= unsigned_short__last .
H11:   fld_nscount(h) >= unsigned_short__first .
H12:   fld_nscount(h) <= unsigned_short__last .
H13:   fld_arcount(h) >= unsigned_short__first .
H14:   fld_arcount(h) <= unsigned_short__last .
H15:   fld_messageid(h) >= unsigned_short__first .
H16:   fld_messageid(h) <= unsigned_short__last .
H17:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H18:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H19:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H20:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H21:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) >= unsigned_short__first .
H22:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) <= unsigned_short__last .
H23:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H24:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
        ->
C1:    byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
C2:    byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
 

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

procedure_byte_swap_5.
H1:    fld_messageid(h) >= unsigned_short__first .
H2:    fld_messageid(h) <= unsigned_short__last .
H3:    fld_opcode(h) >= opcode_type__first .
H4:    fld_opcode(h) <= opcode_type__last .
H5:    fld_rcode(h) >= response_code__first .
H6:    fld_rcode(h) <= response_code__last .
H7:    fld_qdcount(h) >= unsigned_short__first .
H8:    fld_qdcount(h) <= unsigned_short__last .
H9:    fld_ancount(h) >= unsigned_short__first .
H10:   fld_ancount(h) <= unsigned_short__last .
H11:   fld_nscount(h) >= unsigned_short__first .
H12:   fld_nscount(h) <= unsigned_short__last .
H13:   fld_arcount(h) >= unsigned_short__first .
H14:   fld_arcount(h) <= unsigned_short__last .
H15:   fld_messageid(h) >= unsigned_short__first .
H16:   fld_messageid(h) <= unsigned_short__last .
H17:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H18:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H19:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H20:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H21:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) >= unsigned_short__first .
H22:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) <= unsigned_short__last .
H23:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H24:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
H25:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H26:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
        ->
C1:    fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) >= 
           unsigned_short__first .
C2:    fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) <= 
           unsigned_short__last .
 

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

procedure_byte_swap_6.
H1:    fld_messageid(h) >= unsigned_short__first .
H2:    fld_messageid(h) <= unsigned_short__last .
H3:    fld_opcode(h) >= opcode_type__first .
H4:    fld_opcode(h) <= opcode_type__last .
H5:    fld_rcode(h) >= response_code__first .
H6:    fld_rcode(h) <= response_code__last .
H7:    fld_qdcount(h) >= unsigned_short__first .
H8:    fld_qdcount(h) <= unsigned_short__last .
H9:    fld_ancount(h) >= unsigned_short__first .
H10:   fld_ancount(h) <= unsigned_short__last .
H11:   fld_nscount(h) >= unsigned_short__first .
H12:   fld_nscount(h) <= unsigned_short__last .
H13:   fld_arcount(h) >= unsigned_short__first .
H14:   fld_arcount(h) <= unsigned_short__last .
H15:   fld_messageid(h) >= unsigned_short__first .
H16:   fld_messageid(h) <= unsigned_short__last .
H17:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H18:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H19:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H20:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H21:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) >= unsigned_short__first .
H22:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) <= unsigned_short__last .
H23:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H24:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
H25:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H26:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
H27:   fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) >= 
           unsigned_short__first .
H28:   fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) <= 
           unsigned_short__last .
H29:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) >= 
           unsigned_short__first .
H30:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) <= 
           unsigned_short__last .
        ->
C1:    byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) >= 
           unsigned_short__first .
C2:    byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) <= 
           unsigned_short__last .
 

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

procedure_byte_swap_7.
H1:    fld_messageid(h) >= unsigned_short__first .
H2:    fld_messageid(h) <= unsigned_short__last .
H3:    fld_opcode(h) >= opcode_type__first .
H4:    fld_opcode(h) <= opcode_type__last .
H5:    fld_rcode(h) >= response_code__first .
H6:    fld_rcode(h) <= response_code__last .
H7:    fld_qdcount(h) >= unsigned_short__first .
H8:    fld_qdcount(h) <= unsigned_short__last .
H9:    fld_ancount(h) >= unsigned_short__first .
H10:   fld_ancount(h) <= unsigned_short__last .
H11:   fld_nscount(h) >= unsigned_short__first .
H12:   fld_nscount(h) <= unsigned_short__last .
H13:   fld_arcount(h) >= unsigned_short__first .
H14:   fld_arcount(h) <= unsigned_short__last .
H15:   fld_messageid(h) >= unsigned_short__first .
H16:   fld_messageid(h) <= unsigned_short__last .
H17:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H18:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H19:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H20:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H21:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) >= unsigned_short__first .
H22:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) <= unsigned_short__last .
H23:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H24:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
H25:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H26:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
H27:   fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) >= 
           unsigned_short__first .
H28:   fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) <= 
           unsigned_short__last .
H29:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) >= 
           unsigned_short__first .
H30:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) <= 
           unsigned_short__last .
H31:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) >= 
           unsigned_short__first .
H32:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) <= 
           unsigned_short__last .
        ->
C1:    fld_nscount(upf_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))))) >= 
           unsigned_short__first .
C2:    fld_nscount(upf_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))))) <= 
           unsigned_short__last .
 

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

procedure_byte_swap_8.
H1:    fld_messageid(h) >= unsigned_short__first .
H2:    fld_messageid(h) <= unsigned_short__last .
H3:    fld_opcode(h) >= opcode_type__first .
H4:    fld_opcode(h) <= opcode_type__last .
H5:    fld_rcode(h) >= response_code__first .
H6:    fld_rcode(h) <= response_code__last .
H7:    fld_qdcount(h) >= unsigned_short__first .
H8:    fld_qdcount(h) <= unsigned_short__last .
H9:    fld_ancount(h) >= unsigned_short__first .
H10:   fld_ancount(h) <= unsigned_short__last .
H11:   fld_nscount(h) >= unsigned_short__first .
H12:   fld_nscount(h) <= unsigned_short__last .
H13:   fld_arcount(h) >= unsigned_short__first .
H14:   fld_arcount(h) <= unsigned_short__last .
H15:   fld_messageid(h) >= unsigned_short__first .
H16:   fld_messageid(h) <= unsigned_short__last .
H17:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H18:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H19:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H20:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H21:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) >= unsigned_short__first .
H22:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) <= unsigned_short__last .
H23:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H24:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
H25:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H26:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
H27:   fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) >= 
           unsigned_short__first .
H28:   fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) <= 
           unsigned_short__last .
H29:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) >= 
           unsigned_short__first .
H30:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) <= 
           unsigned_short__last .
H31:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) >= 
           unsigned_short__first .
H32:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) <= 
           unsigned_short__last .
H33:   fld_nscount(upf_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))))) >= 
           unsigned_short__first .
H34:   fld_nscount(upf_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))))) <= 
           unsigned_short__last .
H35:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) >= 
           unsigned_short__first .
H36:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) <= 
           unsigned_short__last .
        ->
C1:    byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) >= 
           unsigned_short__first .
C2:    byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) <= 
           unsigned_short__last .
 

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

procedure_byte_swap_9.
H1:    fld_messageid(h) >= unsigned_short__first .
H2:    fld_messageid(h) <= unsigned_short__last .
H3:    fld_opcode(h) >= opcode_type__first .
H4:    fld_opcode(h) <= opcode_type__last .
H5:    fld_rcode(h) >= response_code__first .
H6:    fld_rcode(h) <= response_code__last .
H7:    fld_qdcount(h) >= unsigned_short__first .
H8:    fld_qdcount(h) <= unsigned_short__last .
H9:    fld_ancount(h) >= unsigned_short__first .
H10:   fld_ancount(h) <= unsigned_short__last .
H11:   fld_nscount(h) >= unsigned_short__first .
H12:   fld_nscount(h) <= unsigned_short__last .
H13:   fld_arcount(h) >= unsigned_short__first .
H14:   fld_arcount(h) <= unsigned_short__last .
H15:   fld_messageid(h) >= unsigned_short__first .
H16:   fld_messageid(h) <= unsigned_short__last .
H17:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H18:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H19:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H20:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H21:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) >= unsigned_short__first .
H22:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) <= unsigned_short__last .
H23:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H24:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
H25:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H26:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
H27:   fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) >= 
           unsigned_short__first .
H28:   fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) <= 
           unsigned_short__last .
H29:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) >= 
           unsigned_short__first .
H30:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) <= 
           unsigned_short__last .
H31:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) >= 
           unsigned_short__first .
H32:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) <= 
           unsigned_short__last .
H33:   fld_nscount(upf_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))))) >= 
           unsigned_short__first .
H34:   fld_nscount(upf_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))))) <= 
           unsigned_short__last .
H35:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) >= 
           unsigned_short__first .
H36:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) <= 
           unsigned_short__last .
H37:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) >= 
           unsigned_short__first .
H38:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) <= 
           unsigned_short__last .
        ->
C1:    fld_arcount(upf_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))))))) >= 
           unsigned_short__first .
C2:    fld_arcount(upf_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))))))) <= 
           unsigned_short__last .
 

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

procedure_byte_swap_10.
H1:    fld_messageid(h) >= unsigned_short__first .
H2:    fld_messageid(h) <= unsigned_short__last .
H3:    fld_opcode(h) >= opcode_type__first .
H4:    fld_opcode(h) <= opcode_type__last .
H5:    fld_rcode(h) >= response_code__first .
H6:    fld_rcode(h) <= response_code__last .
H7:    fld_qdcount(h) >= unsigned_short__first .
H8:    fld_qdcount(h) <= unsigned_short__last .
H9:    fld_ancount(h) >= unsigned_short__first .
H10:   fld_ancount(h) <= unsigned_short__last .
H11:   fld_nscount(h) >= unsigned_short__first .
H12:   fld_nscount(h) <= unsigned_short__last .
H13:   fld_arcount(h) >= unsigned_short__first .
H14:   fld_arcount(h) <= unsigned_short__last .
H15:   fld_messageid(h) >= unsigned_short__first .
H16:   fld_messageid(h) <= unsigned_short__last .
H17:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H18:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H19:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H20:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H21:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) >= unsigned_short__first .
H22:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) <= unsigned_short__last .
H23:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H24:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
H25:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H26:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
H27:   fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) >= 
           unsigned_short__first .
H28:   fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) <= 
           unsigned_short__last .
H29:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) >= 
           unsigned_short__first .
H30:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) <= 
           unsigned_short__last .
H31:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) >= 
           unsigned_short__first .
H32:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) <= 
           unsigned_short__last .
H33:   fld_nscount(upf_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))))) >= 
           unsigned_short__first .
H34:   fld_nscount(upf_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))))) <= 
           unsigned_short__last .
H35:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) >= 
           unsigned_short__first .
H36:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) <= 
           unsigned_short__last .
H37:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) >= 
           unsigned_short__first .
H38:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) <= 
           unsigned_short__last .
H39:   fld_arcount(upf_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))))))) >= 
           unsigned_short__first .
H40:   fld_arcount(upf_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))))))) <= 
           unsigned_short__last .
H41:   byte_swap_us(fld_arcount(upf_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))))))))))) >= 
           unsigned_short__first .
H42:   byte_swap_us(fld_arcount(upf_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))))))))))) <= 
           unsigned_short__last .
        ->
C1:    byte_swap_us(fld_arcount(upf_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))))))))))) >= 
           unsigned_short__first .
C2:    byte_swap_us(fld_arcount(upf_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))))))))))) <= 
           unsigned_short__last .
 

For path(s) from start to finish:

procedure_byte_swap_11.
H1:    fld_messageid(h) >= unsigned_short__first .
H2:    fld_messageid(h) <= unsigned_short__last .
H3:    fld_opcode(h) >= opcode_type__first .
H4:    fld_opcode(h) <= opcode_type__last .
H5:    fld_rcode(h) >= response_code__first .
H6:    fld_rcode(h) <= response_code__last .
H7:    fld_qdcount(h) >= unsigned_short__first .
H8:    fld_qdcount(h) <= unsigned_short__last .
H9:    fld_ancount(h) >= unsigned_short__first .
H10:   fld_ancount(h) <= unsigned_short__last .
H11:   fld_nscount(h) >= unsigned_short__first .
H12:   fld_nscount(h) <= unsigned_short__last .
H13:   fld_arcount(h) >= unsigned_short__first .
H14:   fld_arcount(h) <= unsigned_short__last .
H15:   fld_messageid(h) >= unsigned_short__first .
H16:   fld_messageid(h) <= unsigned_short__last .
H17:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H18:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H19:   byte_swap_us(fld_messageid(h)) >= unsigned_short__first .
H20:   byte_swap_us(fld_messageid(h)) <= unsigned_short__last .
H21:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) >= unsigned_short__first .
H22:   fld_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h)))) <= unsigned_short__last .
H23:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H24:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
H25:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) >= 
           unsigned_short__first .
H26:   byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))) <= 
           unsigned_short__last .
H27:   fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) >= 
           unsigned_short__first .
H28:   fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))) <= 
           unsigned_short__last .
H29:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) >= 
           unsigned_short__first .
H30:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) <= 
           unsigned_short__last .
H31:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) >= 
           unsigned_short__first .
H32:   byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))) <= 
           unsigned_short__last .
H33:   fld_nscount(upf_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))))) >= 
           unsigned_short__first .
H34:   fld_nscount(upf_ancount(upf_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))))))) <= 
           unsigned_short__last .
H35:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) >= 
           unsigned_short__first .
H36:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) <= 
           unsigned_short__last .
H37:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) >= 
           unsigned_short__first .
H38:   byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))))) <= 
           unsigned_short__last .
H39:   fld_arcount(upf_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))))))) >= 
           unsigned_short__first .
H40:   fld_arcount(upf_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))))))) <= 
           unsigned_short__last .
H41:   byte_swap_us(fld_arcount(upf_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))))))))))) >= 
           unsigned_short__first .
H42:   byte_swap_us(fld_arcount(upf_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))))))))))) <= 
           unsigned_short__last .
H43:   byte_swap_us(fld_arcount(upf_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))))))))))) >= 
           unsigned_short__first .
H44:   byte_swap_us(fld_arcount(upf_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))))))))))) <= 
           unsigned_short__last .
        ->
C1:    upf_arcount(upf_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h)))))), 
           byte_swap_us(fld_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))))))))), 
           byte_swap_us(fld_arcount(upf_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))), 
           byte_swap_us(fld_nscount(upf_ancount(upf_qdcount(
           upf_messageid(h, byte_swap_us(fld_messageid(h))), 
           byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h)))))), byte_swap_us(fld_ancount(
           upf_qdcount(upf_messageid(h, byte_swap_us(fld_messageid(
           h))), byte_swap_us(fld_qdcount(upf_messageid(h, 
           byte_swap_us(fld_messageid(h))))))))))))))) = upf_arcount(
           upf_nscount(upf_ancount(upf_qdcount(upf_messageid(
           h, byte_swap_us(fld_messageid(h))), byte_swap_us(fld_qdcount(
           h))), byte_swap_us(fld_ancount(h))), 
           byte_swap_us(fld_nscount(h))), byte_swap_us(fld_arcount(
           h))) .
 

