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

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


           procedure Process_Dns_Request.Set_TTL_Data_MX_Response




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

procedure_set_ttl_data_mx_response_1.
H1:    current_name_length >= 0 .
H2:    current_name_length <= rr_type__wirestringtypeindex__last .
H3:    start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
H4:    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(
           bytes, [i___1]) >= dns_types__byte__first) and (element(
           bytes, [i___1]) <= dns_types__byte__last))) .
H5:    start_byte >= dns_types__packet_bytes_range__first .
H6:    start_byte <= dns_types__packet_bytes_range__last .
H7:    fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
H8:    fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
H9:    fld_class(fld_inherit(mx_record)) >= 
           rr_type__classtype__first .
H10:   fld_class(fld_inherit(mx_record)) <= 
           rr_type__classtype__last .
H11:   fld_pref(mx_record) >= unsigned_types__unsigned16__first .
H12:   fld_pref(mx_record) <= unsigned_types__unsigned16__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_mailexchanger(mx_record), [i___1]) >= 
           character__first) and (element(fld_mailexchanger(
           mx_record), [i___1]) <= character__last))) .
H14:   current_name_length >= rr_type__wirestringtypeindex__first .
H15:   current_name_length <= rr_type__wirestringtypeindex__last .
        ->
C1:    fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
C2:    fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
C3:    start_byte >= dns_types__packet_bytes_range__first .
C4:    start_byte <= dns_types__packet_bytes_range__last .
C5:    start_byte <= dns_types__packet_bytes_range__last - 3 .
 

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

procedure_set_ttl_data_mx_response_2.
H1:    current_name_length >= 0 .
H2:    current_name_length <= rr_type__wirestringtypeindex__last .
H3:    start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
H4:    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(
           bytes, [i___1]) >= dns_types__byte__first) and (element(
           bytes, [i___1]) <= dns_types__byte__last))) .
H5:    start_byte >= dns_types__packet_bytes_range__first .
H6:    start_byte <= dns_types__packet_bytes_range__last .
H7:    fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
H8:    fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
H9:    fld_class(fld_inherit(mx_record)) >= 
           rr_type__classtype__first .
H10:   fld_class(fld_inherit(mx_record)) <= 
           rr_type__classtype__last .
H11:   fld_pref(mx_record) >= unsigned_types__unsigned16__first .
H12:   fld_pref(mx_record) <= unsigned_types__unsigned16__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_mailexchanger(mx_record), [i___1]) >= 
           character__first) and (element(fld_mailexchanger(
           mx_record), [i___1]) <= character__last))) .
H14:   current_name_length >= rr_type__wirestringtypeindex__first .
H15:   current_name_length <= rr_type__wirestringtypeindex__last .
H16:   fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
H17:   fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
H18:   start_byte >= dns_types__packet_bytes_range__first .
H19:   start_byte <= dns_types__packet_bytes_range__last .
H20:   start_byte <= dns_types__packet_bytes_range__last - 3 .
H21:   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(
           bytes__1, [i___1]) >= dns_types__byte__first) and (element(
           bytes__1, [i___1]) <= dns_types__byte__last))) .
        ->
C1:    current_name_length + 2 >= unsigned_types__unsigned16__first .
C2:    current_name_length + 2 <= unsigned_types__unsigned16__last .
C3:    start_byte + 4 >= dns_types__packet_bytes_range__first .
C4:    start_byte + 4 <= dns_types__packet_bytes_range__last .
C5:    start_byte + 4 <= dns_types__packet_bytes_range__last - 1 .
C6:    current_name_length + 2 >= unsigned_types__unsigned16__first .
C7:    current_name_length + 2 <= unsigned_types__unsigned16__last .
C8:    current_name_length + 2 >= integer__base__first .
C9:    current_name_length + 2 <= integer__base__last .
C10:   start_byte + 4 >= dns_types__packet_bytes_range__base__first .
C11:   start_byte + 4 <= dns_types__packet_bytes_range__base__last .
 

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

procedure_set_ttl_data_mx_response_3.
H1:    current_name_length >= 0 .
H2:    current_name_length <= rr_type__wirestringtypeindex__last .
H3:    start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
H4:    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(
           bytes, [i___1]) >= dns_types__byte__first) and (element(
           bytes, [i___1]) <= dns_types__byte__last))) .
H5:    start_byte >= dns_types__packet_bytes_range__first .
H6:    start_byte <= dns_types__packet_bytes_range__last .
H7:    fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
H8:    fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
H9:    fld_class(fld_inherit(mx_record)) >= 
           rr_type__classtype__first .
H10:   fld_class(fld_inherit(mx_record)) <= 
           rr_type__classtype__last .
H11:   fld_pref(mx_record) >= unsigned_types__unsigned16__first .
H12:   fld_pref(mx_record) <= unsigned_types__unsigned16__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_mailexchanger(mx_record), [i___1]) >= 
           character__first) and (element(fld_mailexchanger(
           mx_record), [i___1]) <= character__last))) .
H14:   current_name_length >= rr_type__wirestringtypeindex__first .
H15:   current_name_length <= rr_type__wirestringtypeindex__last .
H16:   fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
H17:   fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
H18:   start_byte >= dns_types__packet_bytes_range__first .
H19:   start_byte <= dns_types__packet_bytes_range__last .
H20:   start_byte <= dns_types__packet_bytes_range__last - 3 .
H21:   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(
           bytes__1, [i___1]) >= dns_types__byte__first) and (element(
           bytes__1, [i___1]) <= dns_types__byte__last))) .
H22:   current_name_length + 2 >= unsigned_types__unsigned16__first .
H23:   current_name_length + 2 <= unsigned_types__unsigned16__last .
H24:   start_byte + 4 >= dns_types__packet_bytes_range__first .
H25:   start_byte + 4 <= dns_types__packet_bytes_range__last .
H26:   start_byte + 4 <= dns_types__packet_bytes_range__last - 1 .
H27:   current_name_length + 2 >= unsigned_types__unsigned16__first .
H28:   current_name_length + 2 <= unsigned_types__unsigned16__last .
H29:   current_name_length + 2 >= integer__base__first .
H30:   current_name_length + 2 <= integer__base__last .
H31:   start_byte + 4 >= dns_types__packet_bytes_range__base__first .
H32:   start_byte + 4 <= dns_types__packet_bytes_range__base__last .
H33:   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(
           bytes__2, [i___1]) >= dns_types__byte__first) and (element(
           bytes__2, [i___1]) <= dns_types__byte__last))) .
        ->
C1:    fld_pref(mx_record) >= unsigned_types__unsigned16__first .
C2:    fld_pref(mx_record) <= unsigned_types__unsigned16__last .
C3:    start_byte + 6 >= dns_types__packet_bytes_range__first .
C4:    start_byte + 6 <= dns_types__packet_bytes_range__last .
C5:    start_byte + 6 <= dns_types__packet_bytes_range__last - 1 .
C6:    start_byte + 6 >= dns_types__packet_bytes_range__base__first .
C7:    start_byte + 6 <= dns_types__packet_bytes_range__base__last .
 

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

procedure_set_ttl_data_mx_response_4.
H1:    current_name_length >= 0 .
H2:    current_name_length <= rr_type__wirestringtypeindex__last .
H3:    start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
H4:    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(
           bytes, [i___1]) >= dns_types__byte__first) and (element(
           bytes, [i___1]) <= dns_types__byte__last))) .
H5:    start_byte >= dns_types__packet_bytes_range__first .
H6:    start_byte <= dns_types__packet_bytes_range__last .
H7:    fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
H8:    fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
H9:    fld_class(fld_inherit(mx_record)) >= 
           rr_type__classtype__first .
H10:   fld_class(fld_inherit(mx_record)) <= 
           rr_type__classtype__last .
H11:   fld_pref(mx_record) >= unsigned_types__unsigned16__first .
H12:   fld_pref(mx_record) <= unsigned_types__unsigned16__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_mailexchanger(mx_record), [i___1]) >= 
           character__first) and (element(fld_mailexchanger(
           mx_record), [i___1]) <= character__last))) .
H14:   current_name_length >= rr_type__wirestringtypeindex__first .
H15:   current_name_length <= rr_type__wirestringtypeindex__last .
H16:   fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
H17:   fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
H18:   start_byte >= dns_types__packet_bytes_range__first .
H19:   start_byte <= dns_types__packet_bytes_range__last .
H20:   start_byte <= dns_types__packet_bytes_range__last - 3 .
H21:   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(
           bytes__1, [i___1]) >= dns_types__byte__first) and (element(
           bytes__1, [i___1]) <= dns_types__byte__last))) .
H22:   current_name_length + 2 >= unsigned_types__unsigned16__first .
H23:   current_name_length + 2 <= unsigned_types__unsigned16__last .
H24:   start_byte + 4 >= dns_types__packet_bytes_range__first .
H25:   start_byte + 4 <= dns_types__packet_bytes_range__last .
H26:   start_byte + 4 <= dns_types__packet_bytes_range__last - 1 .
H27:   current_name_length + 2 >= unsigned_types__unsigned16__first .
H28:   current_name_length + 2 <= unsigned_types__unsigned16__last .
H29:   current_name_length + 2 >= integer__base__first .
H30:   current_name_length + 2 <= integer__base__last .
H31:   start_byte + 4 >= dns_types__packet_bytes_range__base__first .
H32:   start_byte + 4 <= dns_types__packet_bytes_range__base__last .
H33:   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(
           bytes__2, [i___1]) >= dns_types__byte__first) and (element(
           bytes__2, [i___1]) <= dns_types__byte__last))) .
H34:   fld_pref(mx_record) >= unsigned_types__unsigned16__first .
H35:   fld_pref(mx_record) <= unsigned_types__unsigned16__last .
H36:   start_byte + 6 >= dns_types__packet_bytes_range__first .
H37:   start_byte + 6 <= dns_types__packet_bytes_range__last .
H38:   start_byte + 6 <= dns_types__packet_bytes_range__last - 1 .
H39:   start_byte + 6 >= dns_types__packet_bytes_range__base__first .
H40:   start_byte + 6 <= dns_types__packet_bytes_range__base__last .
H41:   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(
           bytes__3, [i___1]) >= dns_types__byte__first) and (element(
           bytes__3, [i___1]) <= dns_types__byte__last))) .
        ->
C1:    current_name_length >= integer__first .
C2:    current_name_length <= integer__last .
C3:    1 >= integer__first .
C4:    1 <= integer__last .
 

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

procedure_set_ttl_data_mx_response_5.
H1:    current_name_length >= 0 .
H2:    current_name_length <= rr_type__wirestringtypeindex__last .
H3:    start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
H4:    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(
           bytes, [i___1]) >= dns_types__byte__first) and (element(
           bytes, [i___1]) <= dns_types__byte__last))) .
H5:    start_byte >= dns_types__packet_bytes_range__first .
H6:    start_byte <= dns_types__packet_bytes_range__last .
H7:    fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
H8:    fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
H9:    fld_class(fld_inherit(mx_record)) >= 
           rr_type__classtype__first .
H10:   fld_class(fld_inherit(mx_record)) <= 
           rr_type__classtype__last .
H11:   fld_pref(mx_record) >= unsigned_types__unsigned16__first .
H12:   fld_pref(mx_record) <= unsigned_types__unsigned16__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_mailexchanger(mx_record), [i___1]) >= 
           character__first) and (element(fld_mailexchanger(
           mx_record), [i___1]) <= character__last))) .
H14:   current_name_length >= rr_type__wirestringtypeindex__first .
H15:   current_name_length <= rr_type__wirestringtypeindex__last .
H16:   fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
H17:   fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
H18:   start_byte >= dns_types__packet_bytes_range__first .
H19:   start_byte <= dns_types__packet_bytes_range__last .
H20:   start_byte <= dns_types__packet_bytes_range__last - 3 .
H21:   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(
           bytes__1, [i___1]) >= dns_types__byte__first) and (element(
           bytes__1, [i___1]) <= dns_types__byte__last))) .
H22:   current_name_length + 2 >= unsigned_types__unsigned16__first .
H23:   current_name_length + 2 <= unsigned_types__unsigned16__last .
H24:   start_byte + 4 >= dns_types__packet_bytes_range__first .
H25:   start_byte + 4 <= dns_types__packet_bytes_range__last .
H26:   start_byte + 4 <= dns_types__packet_bytes_range__last - 1 .
H27:   current_name_length + 2 >= unsigned_types__unsigned16__first .
H28:   current_name_length + 2 <= unsigned_types__unsigned16__last .
H29:   current_name_length + 2 >= integer__base__first .
H30:   current_name_length + 2 <= integer__base__last .
H31:   start_byte + 4 >= dns_types__packet_bytes_range__base__first .
H32:   start_byte + 4 <= dns_types__packet_bytes_range__base__last .
H33:   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(
           bytes__2, [i___1]) >= dns_types__byte__first) and (element(
           bytes__2, [i___1]) <= dns_types__byte__last))) .
H34:   fld_pref(mx_record) >= unsigned_types__unsigned16__first .
H35:   fld_pref(mx_record) <= unsigned_types__unsigned16__last .
H36:   start_byte + 6 >= dns_types__packet_bytes_range__first .
H37:   start_byte + 6 <= dns_types__packet_bytes_range__last .
H38:   start_byte + 6 <= dns_types__packet_bytes_range__last - 1 .
H39:   start_byte + 6 >= dns_types__packet_bytes_range__base__first .
H40:   start_byte + 6 <= dns_types__packet_bytes_range__base__last .
H41:   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(
           bytes__3, [i___1]) >= dns_types__byte__first) and (element(
           bytes__3, [i___1]) <= dns_types__byte__last))) .
H42:   current_name_length >= integer__first .
H43:   current_name_length <= integer__last .
H44:   1 >= integer__first .
H45:   1 <= integer__last .
        ->
C1:    (1 <= current_name_length) -> ((current_name_length >= 
           rr_type__wirestringtypeindex__first) and (
           current_name_length <= 
           rr_type__wirestringtypeindex__last)) .
C2:    (1 <= current_name_length) -> ((1 >= 
           rr_type__wirestringtypeindex__first) and (1 <= 
           rr_type__wirestringtypeindex__last)) .
 

For path(s) from start to assertion of line 334:

procedure_set_ttl_data_mx_response_6.
H1:    current_name_length >= 0 .
H2:    current_name_length <= rr_type__wirestringtypeindex__last .
H3:    start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
H4:    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(
           bytes, [i___1]) >= dns_types__byte__first) and (element(
           bytes, [i___1]) <= dns_types__byte__last))) .
H5:    start_byte >= dns_types__packet_bytes_range__first .
H6:    start_byte <= dns_types__packet_bytes_range__last .
H7:    fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
H8:    fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
H9:    fld_class(fld_inherit(mx_record)) >= 
           rr_type__classtype__first .
H10:   fld_class(fld_inherit(mx_record)) <= 
           rr_type__classtype__last .
H11:   fld_pref(mx_record) >= unsigned_types__unsigned16__first .
H12:   fld_pref(mx_record) <= unsigned_types__unsigned16__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_mailexchanger(mx_record), [i___1]) >= 
           character__first) and (element(fld_mailexchanger(
           mx_record), [i___1]) <= character__last))) .
H14:   current_name_length >= rr_type__wirestringtypeindex__first .
H15:   current_name_length <= rr_type__wirestringtypeindex__last .
H16:   fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
H17:   fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
H18:   start_byte >= dns_types__packet_bytes_range__first .
H19:   start_byte <= dns_types__packet_bytes_range__last .
H20:   start_byte <= dns_types__packet_bytes_range__last - 3 .
H21:   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(
           bytes__1, [i___1]) >= dns_types__byte__first) and (element(
           bytes__1, [i___1]) <= dns_types__byte__last))) .
H22:   current_name_length + 2 >= unsigned_types__unsigned16__first .
H23:   current_name_length + 2 <= unsigned_types__unsigned16__last .
H24:   start_byte + 4 >= dns_types__packet_bytes_range__first .
H25:   start_byte + 4 <= dns_types__packet_bytes_range__last .
H26:   start_byte + 4 <= dns_types__packet_bytes_range__last - 1 .
H27:   current_name_length + 2 >= unsigned_types__unsigned16__first .
H28:   current_name_length + 2 <= unsigned_types__unsigned16__last .
H29:   current_name_length + 2 >= integer__base__first .
H30:   current_name_length + 2 <= integer__base__last .
H31:   start_byte + 4 >= dns_types__packet_bytes_range__base__first .
H32:   start_byte + 4 <= dns_types__packet_bytes_range__base__last .
H33:   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(
           bytes__2, [i___1]) >= dns_types__byte__first) and (element(
           bytes__2, [i___1]) <= dns_types__byte__last))) .
H34:   fld_pref(mx_record) >= unsigned_types__unsigned16__first .
H35:   fld_pref(mx_record) <= unsigned_types__unsigned16__last .
H36:   start_byte + 6 >= dns_types__packet_bytes_range__first .
H37:   start_byte + 6 <= dns_types__packet_bytes_range__last .
H38:   start_byte + 6 <= dns_types__packet_bytes_range__last - 1 .
H39:   start_byte + 6 >= dns_types__packet_bytes_range__base__first .
H40:   start_byte + 6 <= dns_types__packet_bytes_range__base__last .
H41:   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(
           bytes__3, [i___1]) >= dns_types__byte__first) and (element(
           bytes__3, [i___1]) <= dns_types__byte__last))) .
H42:   current_name_length >= integer__first .
H43:   current_name_length <= integer__last .
H44:   1 >= integer__first .
H45:   1 <= integer__last .
H46:   (1 <= current_name_length) -> ((current_name_length >= 
           rr_type__wirestringtypeindex__first) and (
           current_name_length <= 
           rr_type__wirestringtypeindex__last)) .
H47:   (1 <= current_name_length) -> ((1 >= 
           rr_type__wirestringtypeindex__first) and (1 <= 
           rr_type__wirestringtypeindex__last)) .
H48:   1 <= current_name_length .
        ->
C1:    start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
C2:    1 >= rr_type__wirestringtypeindex__first .
C3:    1 <= rr_type__wirestringtypeindex__last .
C4:    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(
           bytes__3, [i___1]) >= dns_types__byte__first) and (element(
           bytes__3, [i___1]) <= dns_types__byte__last))) .
C5:    start_byte >= dns_types__packet_bytes_range__first .
C6:    start_byte <= dns_types__packet_bytes_range__last .
C7:    fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
C8:    fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
C9:    fld_class(fld_inherit(mx_record)) >= 
           rr_type__classtype__first .
C10:   fld_class(fld_inherit(mx_record)) <= 
           rr_type__classtype__last .
C11:   fld_pref(mx_record) >= unsigned_types__unsigned16__first .
C12:   fld_pref(mx_record) <= unsigned_types__unsigned16__last .
C13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_mailexchanger(mx_record), [i___1]) >= 
           character__first) and (element(fld_mailexchanger(
           mx_record), [i___1]) <= character__last))) .
C14:   current_name_length >= rr_type__wirestringtypeindex__first .
C15:   current_name_length <= rr_type__wirestringtypeindex__last .
C16:   current_name_length >= 0 .
C17:   current_name_length <= rr_type__wirestringtypeindex__last .
C18:   start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
C19:   1 >= rr_type__wirestringtypeindex__first .
C20:   1 <= rr_type__wirestringtypeindex__last .
C21:   1 >= 1 .
C22:   1 <= current_name_length .
 

For path(s) from assertion of line 334 to assertion of line 334:

procedure_set_ttl_data_mx_response_7.
H1:    start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
H2:    loop__1__i >= rr_type__wirestringtypeindex__first .
H3:    loop__1__i <= rr_type__wirestringtypeindex__last .
H4:    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(
           bytes, [i___1]) >= dns_types__byte__first) and (element(
           bytes, [i___1]) <= dns_types__byte__last))) .
H5:    start_byte >= dns_types__packet_bytes_range__first .
H6:    start_byte <= dns_types__packet_bytes_range__last .
H7:    fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
H8:    fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
H9:    fld_class(fld_inherit(mx_record)) >= 
           rr_type__classtype__first .
H10:   fld_class(fld_inherit(mx_record)) <= 
           rr_type__classtype__last .
H11:   fld_pref(mx_record) >= unsigned_types__unsigned16__first .
H12:   fld_pref(mx_record) <= unsigned_types__unsigned16__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_mailexchanger(mx_record), [i___1]) >= 
           character__first) and (element(fld_mailexchanger(
           mx_record), [i___1]) <= character__last))) .
H14:   current_name_length >= rr_type__wirestringtypeindex__first .
H15:   current_name_length <= rr_type__wirestringtypeindex__last .
H16:   current_name_length >= 0 .
H17:   current_name_length <= rr_type__wirestringtypeindex__last .
H18:   start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
H19:   loop__1__i >= rr_type__wirestringtypeindex__first .
H20:   loop__1__i <= rr_type__wirestringtypeindex__last .
H21:   loop__1__i >= 1 .
H22:   loop__1__i <= current_name_length .
H23:   element(fld_mailexchanger(mx_record), [loop__1__i]) >= 
           dns_types__byte__first .
H24:   element(fld_mailexchanger(mx_record), [loop__1__i]) <= 
           dns_types__byte__last .
H25:   element(fld_mailexchanger(mx_record), [loop__1__i]) >= 
           dns_types__byte__first .
H26:   element(fld_mailexchanger(mx_record), [loop__1__i]) <= 
           dns_types__byte__last .
H27:   loop__1__i >= rr_type__wirestringtypeindex__first .
H28:   loop__1__i <= rr_type__wirestringtypeindex__last .
H29:   start_byte + 7 + loop__1__i >= 
           dns_types__packet_bytes_range__first .
H30:   start_byte + 7 + loop__1__i <= 
           dns_types__packet_bytes_range__last .
H31:   start_byte + 7 + loop__1__i >= 
           dns_types__packet_bytes_range__base__first .
H32:   start_byte + 7 + loop__1__i <= 
           dns_types__packet_bytes_range__base__last .
H33:   loop__1__i >= dns_types__packet_bytes_range__first .
H34:   loop__1__i <= dns_types__packet_bytes_range__last .
H35:   start_byte + 7 >= dns_types__packet_bytes_range__base__first .
H36:   start_byte + 7 <= dns_types__packet_bytes_range__base__last .
H37:   not (loop__1__i = current_name_length) .
        ->
C1:    start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
C2:    loop__1__i + 1 >= rr_type__wirestringtypeindex__first .
C3:    loop__1__i + 1 <= rr_type__wirestringtypeindex__last .
C4:    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(update(
           bytes, [start_byte + 7 + loop__1__i], element(
           fld_mailexchanger(mx_record), [loop__1__i])), [
           i___1]) >= dns_types__byte__first) and (element(update(
           bytes, [start_byte + 7 + loop__1__i], element(
           fld_mailexchanger(mx_record), [loop__1__i])), [
           i___1]) <= dns_types__byte__last))) .
C5:    start_byte >= dns_types__packet_bytes_range__first .
C6:    start_byte <= dns_types__packet_bytes_range__last .
C7:    fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
C8:    fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
C9:    fld_class(fld_inherit(mx_record)) >= 
           rr_type__classtype__first .
C10:   fld_class(fld_inherit(mx_record)) <= 
           rr_type__classtype__last .
C11:   fld_pref(mx_record) >= unsigned_types__unsigned16__first .
C12:   fld_pref(mx_record) <= unsigned_types__unsigned16__last .
C13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_mailexchanger(mx_record), [i___1]) >= 
           character__first) and (element(fld_mailexchanger(
           mx_record), [i___1]) <= character__last))) .
C14:   current_name_length >= rr_type__wirestringtypeindex__first .
C15:   current_name_length <= rr_type__wirestringtypeindex__last .
C16:   current_name_length >= 0 .
C17:   current_name_length <= rr_type__wirestringtypeindex__last .
C18:   start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
C19:   loop__1__i + 1 >= rr_type__wirestringtypeindex__first .
C20:   loop__1__i + 1 <= rr_type__wirestringtypeindex__last .
C21:   loop__1__i + 1 >= 1 .
C22:   loop__1__i + 1 <= current_name_length .
 

For path(s) from assertion of line 334 to run-time check associated with statement of line 336:

procedure_set_ttl_data_mx_response_8.
H1:    start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
H2:    loop__1__i >= rr_type__wirestringtypeindex__first .
H3:    loop__1__i <= rr_type__wirestringtypeindex__last .
H4:    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(
           bytes, [i___1]) >= dns_types__byte__first) and (element(
           bytes, [i___1]) <= dns_types__byte__last))) .
H5:    start_byte >= dns_types__packet_bytes_range__first .
H6:    start_byte <= dns_types__packet_bytes_range__last .
H7:    fld_ttlinseconds(fld_inherit(mx_record)) >= 
           unsigned_types__unsigned32__first .
H8:    fld_ttlinseconds(fld_inherit(mx_record)) <= 
           unsigned_types__unsigned32__last .
H9:    fld_class(fld_inherit(mx_record)) >= 
           rr_type__classtype__first .
H10:   fld_class(fld_inherit(mx_record)) <= 
           rr_type__classtype__last .
H11:   fld_pref(mx_record) >= unsigned_types__unsigned16__first .
H12:   fld_pref(mx_record) <= unsigned_types__unsigned16__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_mailexchanger(mx_record), [i___1]) >= 
           character__first) and (element(fld_mailexchanger(
           mx_record), [i___1]) <= character__last))) .
H14:   current_name_length >= rr_type__wirestringtypeindex__first .
H15:   current_name_length <= rr_type__wirestringtypeindex__last .
H16:   current_name_length >= 0 .
H17:   current_name_length <= rr_type__wirestringtypeindex__last .
H18:   start_byte <= dns_types__packet_bytes_range__last - 8 - 
           current_name_length .
H19:   loop__1__i >= rr_type__wirestringtypeindex__first .
H20:   loop__1__i <= rr_type__wirestringtypeindex__last .
H21:   loop__1__i >= 1 .
H22:   loop__1__i <= current_name_length .
        ->
C1:    element(fld_mailexchanger(mx_record), [loop__1__i]) >= 
           dns_types__byte__first .
C2:    element(fld_mailexchanger(mx_record), [loop__1__i]) <= 
           dns_types__byte__last .
C3:    element(fld_mailexchanger(mx_record), [loop__1__i]) >= 
           dns_types__byte__first .
C4:    element(fld_mailexchanger(mx_record), [loop__1__i]) <= 
           dns_types__byte__last .
C5:    loop__1__i >= rr_type__wirestringtypeindex__first .
C6:    loop__1__i <= rr_type__wirestringtypeindex__last .
C7:    start_byte + 7 + loop__1__i >= 
           dns_types__packet_bytes_range__first .
C8:    start_byte + 7 + loop__1__i <= 
           dns_types__packet_bytes_range__last .
C9:    start_byte + 7 + loop__1__i >= 
           dns_types__packet_bytes_range__base__first .
C10:   start_byte + 7 + loop__1__i <= 
           dns_types__packet_bytes_range__base__last .
C11:   loop__1__i >= dns_types__packet_bytes_range__first .
C12:   loop__1__i <= dns_types__packet_bytes_range__last .
C13:   start_byte + 7 >= dns_types__packet_bytes_range__base__first .
C14:   start_byte + 7 <= dns_types__packet_bytes_range__base__last .
 

For path(s) from start to finish:

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


For path(s) from assertion of line 334 to finish:

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


