656 lines
34 KiB
Plaintext
656 lines
34 KiB
Plaintext
*******************************************************
|
|
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 113:
|
|
|
|
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: 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))) .
|
|
H8: fld_pref(mx_record) >= unsigned_types__unsigned16__first .
|
|
H9: fld_pref(mx_record) <= unsigned_types__unsigned16__last .
|
|
H10: fld_class(fld_inherit(mx_record)) >=
|
|
rr_type__classtype__first .
|
|
H11: fld_class(fld_inherit(mx_record)) <=
|
|
rr_type__classtype__last .
|
|
H12: fld_ttlinseconds(fld_inherit(mx_record)) >=
|
|
unsigned_types__unsigned32__first .
|
|
H13: fld_ttlinseconds(fld_inherit(mx_record)) <=
|
|
unsigned_types__unsigned32__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 115:
|
|
|
|
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: 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))) .
|
|
H8: fld_pref(mx_record) >= unsigned_types__unsigned16__first .
|
|
H9: fld_pref(mx_record) <= unsigned_types__unsigned16__last .
|
|
H10: fld_class(fld_inherit(mx_record)) >=
|
|
rr_type__classtype__first .
|
|
H11: fld_class(fld_inherit(mx_record)) <=
|
|
rr_type__classtype__last .
|
|
H12: fld_ttlinseconds(fld_inherit(mx_record)) >=
|
|
unsigned_types__unsigned32__first .
|
|
H13: fld_ttlinseconds(fld_inherit(mx_record)) <=
|
|
unsigned_types__unsigned32__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 117:
|
|
|
|
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: 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))) .
|
|
H8: fld_pref(mx_record) >= unsigned_types__unsigned16__first .
|
|
H9: fld_pref(mx_record) <= unsigned_types__unsigned16__last .
|
|
H10: fld_class(fld_inherit(mx_record)) >=
|
|
rr_type__classtype__first .
|
|
H11: fld_class(fld_inherit(mx_record)) <=
|
|
rr_type__classtype__last .
|
|
H12: fld_ttlinseconds(fld_inherit(mx_record)) >=
|
|
unsigned_types__unsigned32__first .
|
|
H13: fld_ttlinseconds(fld_inherit(mx_record)) <=
|
|
unsigned_types__unsigned32__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 119:
|
|
|
|
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: 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))) .
|
|
H8: fld_pref(mx_record) >= unsigned_types__unsigned16__first .
|
|
H9: fld_pref(mx_record) <= unsigned_types__unsigned16__last .
|
|
H10: fld_class(fld_inherit(mx_record)) >=
|
|
rr_type__classtype__first .
|
|
H11: fld_class(fld_inherit(mx_record)) <=
|
|
rr_type__classtype__last .
|
|
H12: fld_ttlinseconds(fld_inherit(mx_record)) >=
|
|
unsigned_types__unsigned32__first .
|
|
H13: fld_ttlinseconds(fld_inherit(mx_record)) <=
|
|
unsigned_types__unsigned32__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 119:
|
|
|
|
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: 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))) .
|
|
H8: fld_pref(mx_record) >= unsigned_types__unsigned16__first .
|
|
H9: fld_pref(mx_record) <= unsigned_types__unsigned16__last .
|
|
H10: fld_class(fld_inherit(mx_record)) >=
|
|
rr_type__classtype__first .
|
|
H11: fld_class(fld_inherit(mx_record)) <=
|
|
rr_type__classtype__last .
|
|
H12: fld_ttlinseconds(fld_inherit(mx_record)) >=
|
|
unsigned_types__unsigned32__first .
|
|
H13: fld_ttlinseconds(fld_inherit(mx_record)) <=
|
|
unsigned_types__unsigned32__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 120:
|
|
|
|
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: 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))) .
|
|
H8: fld_pref(mx_record) >= unsigned_types__unsigned16__first .
|
|
H9: fld_pref(mx_record) <= unsigned_types__unsigned16__last .
|
|
H10: fld_class(fld_inherit(mx_record)) >=
|
|
rr_type__classtype__first .
|
|
H11: fld_class(fld_inherit(mx_record)) <=
|
|
rr_type__classtype__last .
|
|
H12: fld_ttlinseconds(fld_inherit(mx_record)) >=
|
|
unsigned_types__unsigned32__first .
|
|
H13: fld_ttlinseconds(fld_inherit(mx_record)) <=
|
|
unsigned_types__unsigned32__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: 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))) .
|
|
C8: fld_pref(mx_record) >= unsigned_types__unsigned16__first .
|
|
C9: fld_pref(mx_record) <= unsigned_types__unsigned16__last .
|
|
C10: fld_class(fld_inherit(mx_record)) >=
|
|
rr_type__classtype__first .
|
|
C11: fld_class(fld_inherit(mx_record)) <=
|
|
rr_type__classtype__last .
|
|
C12: fld_ttlinseconds(fld_inherit(mx_record)) >=
|
|
unsigned_types__unsigned32__first .
|
|
C13: fld_ttlinseconds(fld_inherit(mx_record)) <=
|
|
unsigned_types__unsigned32__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 120 to assertion of line 120:
|
|
|
|
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: 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))) .
|
|
H8: fld_pref(mx_record) >= unsigned_types__unsigned16__first .
|
|
H9: fld_pref(mx_record) <= unsigned_types__unsigned16__last .
|
|
H10: fld_class(fld_inherit(mx_record)) >=
|
|
rr_type__classtype__first .
|
|
H11: fld_class(fld_inherit(mx_record)) <=
|
|
rr_type__classtype__last .
|
|
H12: fld_ttlinseconds(fld_inherit(mx_record)) >=
|
|
unsigned_types__unsigned32__first .
|
|
H13: fld_ttlinseconds(fld_inherit(mx_record)) <=
|
|
unsigned_types__unsigned32__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: 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))) .
|
|
C8: fld_pref(mx_record) >= unsigned_types__unsigned16__first .
|
|
C9: fld_pref(mx_record) <= unsigned_types__unsigned16__last .
|
|
C10: fld_class(fld_inherit(mx_record)) >=
|
|
rr_type__classtype__first .
|
|
C11: fld_class(fld_inherit(mx_record)) <=
|
|
rr_type__classtype__last .
|
|
C12: fld_ttlinseconds(fld_inherit(mx_record)) >=
|
|
unsigned_types__unsigned32__first .
|
|
C13: fld_ttlinseconds(fld_inherit(mx_record)) <=
|
|
unsigned_types__unsigned32__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 120 to run-time check associated with statement of line 122:
|
|
|
|
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: 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))) .
|
|
H8: fld_pref(mx_record) >= unsigned_types__unsigned16__first .
|
|
H9: fld_pref(mx_record) <= unsigned_types__unsigned16__last .
|
|
H10: fld_class(fld_inherit(mx_record)) >=
|
|
rr_type__classtype__first .
|
|
H11: fld_class(fld_inherit(mx_record)) <=
|
|
rr_type__classtype__last .
|
|
H12: fld_ttlinseconds(fld_inherit(mx_record)) >=
|
|
unsigned_types__unsigned32__first .
|
|
H13: fld_ttlinseconds(fld_inherit(mx_record)) <=
|
|
unsigned_types__unsigned32__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 120 to finish:
|
|
|
|
procedure_set_ttl_data_mx_response_10.
|
|
*** true . /* trivially true VC removed by Examiner */
|
|
|
|
|