3277 lines
160 KiB
Plaintext
3277 lines
160 KiB
Plaintext
*******************************************************
|
|
Semantic Analysis of SPARK Text
|
|
Examiner GPL Edition
|
|
|
|
*******************************************************
|
|
|
|
|
|
procedure Process_Dns_Request.Create_NXDOMAIN_Response
|
|
|
|
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 676:
|
|
|
|
procedure_create_nxdomain_response_1.
|
|
H1: start_byte <= dns_types__packet_size .
|
|
H2: start_byte >= dns_types__packet_bytes_range__first .
|
|
H3: start_byte <= dns_types__packet_bytes_range__last .
|
|
H4: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H5: qname_location >= dns_types__qname_ptr_range__first .
|
|
H6: qname_location <= dns_types__qname_ptr_range__last .
|
|
H7: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H8: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H9: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H10: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H11: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H12: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H17: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H18: true .
|
|
H19: true .
|
|
H20: true .
|
|
H21: true .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H26: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H27: true .
|
|
H28: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H29: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
->
|
|
C1: qname_location >= dns_types__qname_ptr_range__first .
|
|
C2: qname_location <= dns_types__qname_ptr_range__last .
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 677:
|
|
|
|
procedure_create_nxdomain_response_2.
|
|
H1: start_byte <= dns_types__packet_size .
|
|
H2: start_byte >= dns_types__packet_bytes_range__first .
|
|
H3: start_byte <= dns_types__packet_bytes_range__last .
|
|
H4: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H5: qname_location >= dns_types__qname_ptr_range__first .
|
|
H6: qname_location <= dns_types__qname_ptr_range__last .
|
|
H7: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H8: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H9: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H10: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H11: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H12: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H17: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H18: true .
|
|
H19: true .
|
|
H20: true .
|
|
H21: true .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H26: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H27: true .
|
|
H28: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H29: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H30: qname_location >= dns_types__qname_ptr_range__first .
|
|
H31: qname_location <= dns_types__qname_ptr_range__last .
|
|
->
|
|
C1: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
C2: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
C3: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
C4: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
C5: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__base__first .
|
|
C6: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__base__last .
|
|
C7: dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__first .
|
|
C8: dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__last .
|
|
C9: dns_types__header_bits div 8 >= system__min_int .
|
|
C10: dns_types__header_bits div 8 <= system__max_int .
|
|
C11: 8 <> 0 .
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 679:
|
|
|
|
procedure_create_nxdomain_response_3.
|
|
H1: start_byte <= dns_types__packet_size .
|
|
H2: start_byte >= dns_types__packet_bytes_range__first .
|
|
H3: start_byte <= dns_types__packet_bytes_range__last .
|
|
H4: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H5: qname_location >= dns_types__qname_ptr_range__first .
|
|
H6: qname_location <= dns_types__qname_ptr_range__last .
|
|
H7: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H8: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H9: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H10: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H11: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H12: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H17: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H18: true .
|
|
H19: true .
|
|
H20: true .
|
|
H21: true .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H26: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H27: true .
|
|
H28: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H29: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H30: qname_location >= dns_types__qname_ptr_range__first .
|
|
H31: qname_location <= dns_types__qname_ptr_range__last .
|
|
H32: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H33: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H34: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H35: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H36: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__base__first .
|
|
H37: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__base__last .
|
|
H38: dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__first .
|
|
H39: dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__last .
|
|
H40: dns_types__header_bits div 8 >= system__min_int .
|
|
H41: dns_types__header_bits div 8 <= system__max_int .
|
|
H42: 8 <> 0 .
|
|
->
|
|
C1: dns_types__name_error >= dns_types__response_code__first .
|
|
C2: dns_types__name_error <= dns_types__response_code__last .
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 680:
|
|
|
|
procedure_create_nxdomain_response_4.
|
|
H1: start_byte <= dns_types__packet_size .
|
|
H2: start_byte >= dns_types__packet_bytes_range__first .
|
|
H3: start_byte <= dns_types__packet_bytes_range__last .
|
|
H4: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H5: qname_location >= dns_types__qname_ptr_range__first .
|
|
H6: qname_location <= dns_types__qname_ptr_range__last .
|
|
H7: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H8: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H9: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H10: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H11: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H12: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H17: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H18: true .
|
|
H19: true .
|
|
H20: true .
|
|
H21: true .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H26: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H27: true .
|
|
H28: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H29: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H30: qname_location >= dns_types__qname_ptr_range__first .
|
|
H31: qname_location <= dns_types__qname_ptr_range__last .
|
|
H32: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H33: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H34: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H35: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H36: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__base__first .
|
|
H37: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__base__last .
|
|
H38: dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__first .
|
|
H39: dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__last .
|
|
H40: dns_types__header_bits div 8 >= system__min_int .
|
|
H41: dns_types__header_bits div 8 <= system__max_int .
|
|
H42: 8 <> 0 .
|
|
H43: dns_types__name_error >= dns_types__response_code__first .
|
|
H44: dns_types__name_error <= dns_types__response_code__last .
|
|
->
|
|
C1: 0 >= dns_types__unsigned_short__first .
|
|
C2: 0 <= dns_types__unsigned_short__last .
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 683:
|
|
|
|
procedure_create_nxdomain_response_5.
|
|
H1: start_byte <= dns_types__packet_size .
|
|
H2: start_byte >= dns_types__packet_bytes_range__first .
|
|
H3: start_byte <= dns_types__packet_bytes_range__last .
|
|
H4: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H5: qname_location >= dns_types__qname_ptr_range__first .
|
|
H6: qname_location <= dns_types__qname_ptr_range__last .
|
|
H7: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H8: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H9: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H10: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H11: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H12: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H17: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H18: true .
|
|
H19: true .
|
|
H20: true .
|
|
H21: true .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H26: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H27: true .
|
|
H28: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H29: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H30: qname_location >= dns_types__qname_ptr_range__first .
|
|
H31: qname_location <= dns_types__qname_ptr_range__last .
|
|
H32: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H33: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H34: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H35: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H36: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__base__first .
|
|
H37: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__base__last .
|
|
H38: dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__first .
|
|
H39: dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__last .
|
|
H40: dns_types__header_bits div 8 >= system__min_int .
|
|
H41: dns_types__header_bits div 8 <= system__max_int .
|
|
H42: 8 <> 0 .
|
|
H43: dns_types__name_error >= dns_types__response_code__first .
|
|
H44: dns_types__name_error <= dns_types__response_code__last .
|
|
H45: 0 >= dns_types__unsigned_short__first .
|
|
H46: 0 <= dns_types__unsigned_short__last .
|
|
H47: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H48: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H49: 0 >= dns_types__unsigned_short__first .
|
|
H50: 0 <= dns_types__unsigned_short__last .
|
|
H51: 0 >= natural__first .
|
|
H52: 0 <= natural__last .
|
|
H53: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H54: qname_location >= dns_types__qname_ptr_range__first .
|
|
H55: qname_location <= dns_types__qname_ptr_range__last .
|
|
->
|
|
C1: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__qname_ptr_range__first .
|
|
C2: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__qname_ptr_range__last .
|
|
C3: element(domainname, [rr_type__wirestringtypeindex__first]) >=
|
|
natural__first .
|
|
C4: element(domainname, [rr_type__wirestringtypeindex__first]) <=
|
|
natural__last .
|
|
C5: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
C6: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
|
|
|
|
For path(s) from assertion of line 686 to run-time check associated with statement of line 683:
|
|
|
|
procedure_create_nxdomain_response_6.
|
|
H1: answer_count = 0 .
|
|
H2: amount_trimmed >= 0 .
|
|
H3: amount_trimmed < rr_type__wirestringtypeindex__last .
|
|
H4: output_bytes <= dns_types__packet_length_range__last .
|
|
H5: current_qname_location <= output_bytes .
|
|
H6: start_byte >= dns_types__packet_bytes_range__first .
|
|
H7: start_byte <= dns_types__packet_bytes_range__last .
|
|
H8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H9: qname_location >= dns_types__qname_ptr_range__first .
|
|
H10: qname_location <= dns_types__qname_ptr_range__last .
|
|
H11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H12: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H17: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H18: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H19: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H20: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H21: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: true .
|
|
H26: true .
|
|
H27: true .
|
|
H28: true .
|
|
H29: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H30: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H31: true .
|
|
H32: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H33: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H34: start_byte <= dns_types__packet_size .
|
|
H35: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
current_name, [i___1]) >= character__first) and (element(
|
|
current_name, [i___1]) <= character__last))) .
|
|
H36: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H37: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H38: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H39: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H40: current_qname_location <=
|
|
dns_types__packet_length_range__last .
|
|
H41: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H42: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H43: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H44: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H45: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H46: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H47: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H48: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H49: answer_count >= dns_types__unsigned_short__first .
|
|
H50: answer_count <= dns_types__unsigned_short__last .
|
|
H51: answer_count >= dns_types__unsigned_short__first .
|
|
H52: answer_count <= dns_types__unsigned_short__last .
|
|
H53: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H54: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H55: start_byte >= dns_types__packet_bytes_range__first .
|
|
H56: start_byte <= dns_types__packet_bytes_range__last .
|
|
H57: start_byte <= dns_types__packet_size .
|
|
H58: answer_count <= dns_types__unsigned_short__last -
|
|
rr_type__maxnumrecords .
|
|
H59: output_bytes__2 >= dns_types__header_bits div 8 + 1 .
|
|
H60: output_bytes__2 <= dns_types__packet_size .
|
|
H61: answer_count__2 <= answer_count +
|
|
rr_type__maxnumrecords .
|
|
H62: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet__2), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet__2), [i___1]) <= dns_types__byte__last))) .
|
|
H63: fld_arcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H64: fld_arcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H65: fld_nscount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H66: fld_nscount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H67: fld_ancount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H68: fld_ancount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H69: fld_qdcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H70: fld_qdcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H71: fld_rcode(fld_header(output_packet__2)) >=
|
|
dns_types__response_code__first .
|
|
H72: fld_rcode(fld_header(output_packet__2)) <=
|
|
dns_types__response_code__last .
|
|
H73: true .
|
|
H74: true .
|
|
H75: true .
|
|
H76: true .
|
|
H77: true .
|
|
H78: true .
|
|
H79: true .
|
|
H80: fld_opcode(fld_header(output_packet__2)) >=
|
|
dns_types__opcode_type__first .
|
|
H81: fld_opcode(fld_header(output_packet__2)) <=
|
|
dns_types__opcode_type__last .
|
|
H82: true .
|
|
H83: fld_messageid(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H84: fld_messageid(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H85: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H86: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H87: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H88: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H89: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H90: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H91: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H92: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H93: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H94: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H95: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H96: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H97: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H98: amount_trimmed >= natural__first .
|
|
H99: amount_trimmed <= natural__last .
|
|
H100: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >=
|
|
natural__first .
|
|
H101: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <=
|
|
natural__last .
|
|
H102: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >=
|
|
natural__first .
|
|
H103: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <=
|
|
natural__last .
|
|
H104: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
|
|
H105: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
|
|
H106: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H107: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H108: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H109: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H110: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H111: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H112: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >=
|
|
natural__first .
|
|
H113: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <=
|
|
natural__last .
|
|
H114: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H115: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H116: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
->
|
|
C1: output_bytes__2 >= dns_types__qname_ptr_range__first .
|
|
C2: output_bytes__2 <= dns_types__qname_ptr_range__last .
|
|
C3: element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) >=
|
|
natural__first .
|
|
C4: element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <=
|
|
natural__last .
|
|
C5: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
C6: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
|
|
|
|
For path(s) from start to assertion of line 686:
|
|
|
|
procedure_create_nxdomain_response_7.
|
|
H1: start_byte <= dns_types__packet_size .
|
|
H2: start_byte >= dns_types__packet_bytes_range__first .
|
|
H3: start_byte <= dns_types__packet_bytes_range__last .
|
|
H4: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H5: qname_location >= dns_types__qname_ptr_range__first .
|
|
H6: qname_location <= dns_types__qname_ptr_range__last .
|
|
H7: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H8: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H9: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H10: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H11: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H12: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H17: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H18: true .
|
|
H19: true .
|
|
H20: true .
|
|
H21: true .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H26: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H27: true .
|
|
H28: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H29: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H30: qname_location >= dns_types__qname_ptr_range__first .
|
|
H31: qname_location <= dns_types__qname_ptr_range__last .
|
|
H32: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H33: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H34: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H35: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H36: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__base__first .
|
|
H37: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__base__last .
|
|
H38: dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__first .
|
|
H39: dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__last .
|
|
H40: dns_types__header_bits div 8 >= system__min_int .
|
|
H41: dns_types__header_bits div 8 <= system__max_int .
|
|
H42: 8 <> 0 .
|
|
H43: dns_types__name_error >= dns_types__response_code__first .
|
|
H44: dns_types__name_error <= dns_types__response_code__last .
|
|
H45: 0 >= dns_types__unsigned_short__first .
|
|
H46: 0 <= dns_types__unsigned_short__last .
|
|
H47: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H48: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H49: 0 >= dns_types__unsigned_short__first .
|
|
H50: 0 <= dns_types__unsigned_short__last .
|
|
H51: 0 >= natural__first .
|
|
H52: 0 <= natural__last .
|
|
H53: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H54: qname_location >= dns_types__qname_ptr_range__first .
|
|
H55: qname_location <= dns_types__qname_ptr_range__last .
|
|
H56: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__qname_ptr_range__first .
|
|
H57: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__qname_ptr_range__last .
|
|
H58: element(domainname, [rr_type__wirestringtypeindex__first]) >=
|
|
natural__first .
|
|
H59: element(domainname, [rr_type__wirestringtypeindex__first]) <=
|
|
natural__last .
|
|
H60: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H61: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H62: 0 = 0 .
|
|
H63: 0 < rr_type__wirestringtypeindex__last .
|
|
H64: element(domainname, [rr_type__wirestringtypeindex__first]) <> 0 .
|
|
H65: qname_location <= start_byte + dns_types__header_bits div 8 .
|
|
->
|
|
C1: 0 = 0 .
|
|
C2: 0 >= 0 .
|
|
C3: 0 < rr_type__wirestringtypeindex__last .
|
|
C4: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
C5: qname_location <= start_byte + dns_types__header_bits div 8 .
|
|
C6: start_byte >= dns_types__packet_bytes_range__first .
|
|
C7: start_byte <= dns_types__packet_bytes_range__last .
|
|
C8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
C9: qname_location >= dns_types__qname_ptr_range__first .
|
|
C10: qname_location <= dns_types__qname_ptr_range__last .
|
|
C11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(upf_header(upf_header(output_packet, upf_rcode(
|
|
fld_header(output_packet), dns_types__name_error)),
|
|
upf_ancount(fld_header(upf_header(output_packet, upf_rcode(
|
|
fld_header(output_packet), dns_types__name_error))), 0))), [
|
|
i___1]) >= dns_types__byte__first) and (element(fld_bytes(
|
|
upf_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0))), [
|
|
i___1]) <= dns_types__byte__last))) .
|
|
C12: fld_arcount(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) >=
|
|
dns_types__unsigned_short__first .
|
|
C13: fld_arcount(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) <=
|
|
dns_types__unsigned_short__last .
|
|
C14: fld_nscount(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) >=
|
|
dns_types__unsigned_short__first .
|
|
C15: fld_nscount(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) <=
|
|
dns_types__unsigned_short__last .
|
|
C16: fld_ancount(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) >=
|
|
dns_types__unsigned_short__first .
|
|
C17: fld_ancount(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) <=
|
|
dns_types__unsigned_short__last .
|
|
C18: fld_qdcount(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) >=
|
|
dns_types__unsigned_short__first .
|
|
C19: fld_qdcount(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) <=
|
|
dns_types__unsigned_short__last .
|
|
C20: fld_rcode(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) >=
|
|
dns_types__response_code__first .
|
|
C21: fld_rcode(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) <=
|
|
dns_types__response_code__last .
|
|
C22: true .
|
|
C23: true .
|
|
C24: true .
|
|
C25: true .
|
|
C26: true .
|
|
C27: true .
|
|
C28: true .
|
|
C29: fld_opcode(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) >=
|
|
dns_types__opcode_type__first .
|
|
C30: fld_opcode(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) <=
|
|
dns_types__opcode_type__last .
|
|
C31: true .
|
|
C32: fld_messageid(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) >=
|
|
dns_types__unsigned_short__first .
|
|
C33: fld_messageid(fld_header(upf_header(upf_header(
|
|
output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error)), upf_ancount(
|
|
fld_header(upf_header(output_packet, upf_rcode(fld_header(
|
|
output_packet), dns_types__name_error))), 0)))) <=
|
|
dns_types__unsigned_short__last .
|
|
C34: start_byte <= dns_types__packet_size .
|
|
|
|
|
|
For path(s) from assertion of line 686 to assertion of line 686:
|
|
|
|
procedure_create_nxdomain_response_8.
|
|
H1: answer_count = 0 .
|
|
H2: amount_trimmed >= 0 .
|
|
H3: amount_trimmed < rr_type__wirestringtypeindex__last .
|
|
H4: output_bytes <= dns_types__packet_length_range__last .
|
|
H5: current_qname_location <= output_bytes .
|
|
H6: start_byte >= dns_types__packet_bytes_range__first .
|
|
H7: start_byte <= dns_types__packet_bytes_range__last .
|
|
H8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H9: qname_location >= dns_types__qname_ptr_range__first .
|
|
H10: qname_location <= dns_types__qname_ptr_range__last .
|
|
H11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H12: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H17: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H18: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H19: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H20: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H21: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: true .
|
|
H26: true .
|
|
H27: true .
|
|
H28: true .
|
|
H29: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H30: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H31: true .
|
|
H32: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H33: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H34: start_byte <= dns_types__packet_size .
|
|
H35: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
current_name, [i___1]) >= character__first) and (element(
|
|
current_name, [i___1]) <= character__last))) .
|
|
H36: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H37: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H38: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H39: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H40: current_qname_location <=
|
|
dns_types__packet_length_range__last .
|
|
H41: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H42: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H43: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H44: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H45: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H46: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H47: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H48: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H49: answer_count >= dns_types__unsigned_short__first .
|
|
H50: answer_count <= dns_types__unsigned_short__last .
|
|
H51: answer_count >= dns_types__unsigned_short__first .
|
|
H52: answer_count <= dns_types__unsigned_short__last .
|
|
H53: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H54: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H55: start_byte >= dns_types__packet_bytes_range__first .
|
|
H56: start_byte <= dns_types__packet_bytes_range__last .
|
|
H57: start_byte <= dns_types__packet_size .
|
|
H58: answer_count <= dns_types__unsigned_short__last -
|
|
rr_type__maxnumrecords .
|
|
H59: output_bytes__2 >= dns_types__header_bits div 8 + 1 .
|
|
H60: output_bytes__2 <= dns_types__packet_size .
|
|
H61: answer_count__2 <= answer_count +
|
|
rr_type__maxnumrecords .
|
|
H62: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet__2), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet__2), [i___1]) <= dns_types__byte__last))) .
|
|
H63: fld_arcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H64: fld_arcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H65: fld_nscount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H66: fld_nscount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H67: fld_ancount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H68: fld_ancount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H69: fld_qdcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H70: fld_qdcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H71: fld_rcode(fld_header(output_packet__2)) >=
|
|
dns_types__response_code__first .
|
|
H72: fld_rcode(fld_header(output_packet__2)) <=
|
|
dns_types__response_code__last .
|
|
H73: true .
|
|
H74: true .
|
|
H75: true .
|
|
H76: true .
|
|
H77: true .
|
|
H78: true .
|
|
H79: true .
|
|
H80: fld_opcode(fld_header(output_packet__2)) >=
|
|
dns_types__opcode_type__first .
|
|
H81: fld_opcode(fld_header(output_packet__2)) <=
|
|
dns_types__opcode_type__last .
|
|
H82: true .
|
|
H83: fld_messageid(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H84: fld_messageid(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H85: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H86: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H87: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H88: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H89: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H90: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H91: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H92: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H93: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H94: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H95: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H96: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H97: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H98: amount_trimmed >= natural__first .
|
|
H99: amount_trimmed <= natural__last .
|
|
H100: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >=
|
|
natural__first .
|
|
H101: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <=
|
|
natural__last .
|
|
H102: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >=
|
|
natural__first .
|
|
H103: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <=
|
|
natural__last .
|
|
H104: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
|
|
H105: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
|
|
H106: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H107: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H108: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H109: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H110: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H111: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H112: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >=
|
|
natural__first .
|
|
H113: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <=
|
|
natural__last .
|
|
H114: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H115: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H116: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H117: output_bytes__2 >= dns_types__qname_ptr_range__first .
|
|
H118: output_bytes__2 <= dns_types__qname_ptr_range__last .
|
|
H119: element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) >=
|
|
natural__first .
|
|
H120: element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <=
|
|
natural__last .
|
|
H121: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H122: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H123: answer_count__2 = 0 .
|
|
H124: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <
|
|
rr_type__wirestringtypeindex__last .
|
|
H125: element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <>
|
|
0 .
|
|
H126: new_qname_location__1 <= output_bytes__2 .
|
|
->
|
|
C1: answer_count__2 = 0 .
|
|
C2: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >= 0 .
|
|
C3: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <
|
|
rr_type__wirestringtypeindex__last .
|
|
C4: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
C5: new_qname_location__1 <= output_bytes__2 .
|
|
C6: start_byte >= dns_types__packet_bytes_range__first .
|
|
C7: start_byte <= dns_types__packet_bytes_range__last .
|
|
C8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
C9: qname_location >= dns_types__qname_ptr_range__first .
|
|
C10: qname_location <= dns_types__qname_ptr_range__last .
|
|
C11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet__2), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet__2), [i___1]) <= dns_types__byte__last))) .
|
|
C12: fld_arcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
C13: fld_arcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
C14: fld_nscount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
C15: fld_nscount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
C16: fld_ancount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
C17: fld_ancount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
C18: fld_qdcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
C19: fld_qdcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
C20: fld_rcode(fld_header(output_packet__2)) >=
|
|
dns_types__response_code__first .
|
|
C21: fld_rcode(fld_header(output_packet__2)) <=
|
|
dns_types__response_code__last .
|
|
C22: true .
|
|
C23: true .
|
|
C24: true .
|
|
C25: true .
|
|
C26: true .
|
|
C27: true .
|
|
C28: true .
|
|
C29: fld_opcode(fld_header(output_packet__2)) >=
|
|
dns_types__opcode_type__first .
|
|
C30: fld_opcode(fld_header(output_packet__2)) <=
|
|
dns_types__opcode_type__last .
|
|
C31: true .
|
|
C32: fld_messageid(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
C33: fld_messageid(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
C34: start_byte <= dns_types__packet_size .
|
|
|
|
|
|
For path(s) from assertion of line 686 to precondition check associated with statement of line 689:
|
|
|
|
procedure_create_nxdomain_response_9.
|
|
H1: answer_count = 0 .
|
|
H2: amount_trimmed >= 0 .
|
|
H3: amount_trimmed < rr_type__wirestringtypeindex__last .
|
|
H4: output_bytes <= dns_types__packet_length_range__last .
|
|
H5: current_qname_location <= output_bytes .
|
|
H6: start_byte >= dns_types__packet_bytes_range__first .
|
|
H7: start_byte <= dns_types__packet_bytes_range__last .
|
|
H8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H9: qname_location >= dns_types__qname_ptr_range__first .
|
|
H10: qname_location <= dns_types__qname_ptr_range__last .
|
|
H11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H12: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H17: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H18: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H19: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H20: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H21: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: true .
|
|
H26: true .
|
|
H27: true .
|
|
H28: true .
|
|
H29: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H30: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H31: true .
|
|
H32: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H33: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H34: start_byte <= dns_types__packet_size .
|
|
H35: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
current_name, [i___1]) >= character__first) and (element(
|
|
current_name, [i___1]) <= character__last))) .
|
|
H36: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H37: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
->
|
|
C1: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
C2: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
C3: current_qname_location <=
|
|
dns_types__packet_length_range__last .
|
|
|
|
|
|
For path(s) from assertion of line 686 to run-time check associated with statement of line 689:
|
|
|
|
procedure_create_nxdomain_response_10.
|
|
H1: answer_count = 0 .
|
|
H2: amount_trimmed >= 0 .
|
|
H3: amount_trimmed < rr_type__wirestringtypeindex__last .
|
|
H4: output_bytes <= dns_types__packet_length_range__last .
|
|
H5: current_qname_location <= output_bytes .
|
|
H6: start_byte >= dns_types__packet_bytes_range__first .
|
|
H7: start_byte <= dns_types__packet_bytes_range__last .
|
|
H8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H9: qname_location >= dns_types__qname_ptr_range__first .
|
|
H10: qname_location <= dns_types__qname_ptr_range__last .
|
|
H11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H12: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H17: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H18: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H19: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H20: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H21: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: true .
|
|
H26: true .
|
|
H27: true .
|
|
H28: true .
|
|
H29: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H30: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H31: true .
|
|
H32: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H33: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H34: start_byte <= dns_types__packet_size .
|
|
H35: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
current_name, [i___1]) >= character__first) and (element(
|
|
current_name, [i___1]) <= character__last))) .
|
|
H36: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H37: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H38: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H39: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H40: current_qname_location <=
|
|
dns_types__packet_length_range__last .
|
|
H41: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H42: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H43: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
->
|
|
C1: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
C2: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
|
|
|
|
For path(s) from assertion of line 686 to precondition check associated with statement of line 694:
|
|
|
|
procedure_create_nxdomain_response_11.
|
|
H1: answer_count = 0 .
|
|
H2: amount_trimmed >= 0 .
|
|
H3: amount_trimmed < rr_type__wirestringtypeindex__last .
|
|
H4: output_bytes <= dns_types__packet_length_range__last .
|
|
H5: current_qname_location <= output_bytes .
|
|
H6: start_byte >= dns_types__packet_bytes_range__first .
|
|
H7: start_byte <= dns_types__packet_bytes_range__last .
|
|
H8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H9: qname_location >= dns_types__qname_ptr_range__first .
|
|
H10: qname_location <= dns_types__qname_ptr_range__last .
|
|
H11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H12: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H17: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H18: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H19: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H20: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H21: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: true .
|
|
H26: true .
|
|
H27: true .
|
|
H28: true .
|
|
H29: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H30: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H31: true .
|
|
H32: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H33: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H34: start_byte <= dns_types__packet_size .
|
|
H35: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
current_name, [i___1]) >= character__first) and (element(
|
|
current_name, [i___1]) <= character__last))) .
|
|
H36: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H37: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H38: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H39: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H40: current_qname_location <=
|
|
dns_types__packet_length_range__last .
|
|
H41: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H42: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H43: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H44: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H45: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H46: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H47: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H48: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H49: answer_count >= dns_types__unsigned_short__first .
|
|
H50: answer_count <= dns_types__unsigned_short__last .
|
|
->
|
|
C1: answer_count >= dns_types__unsigned_short__first .
|
|
C2: answer_count <= dns_types__unsigned_short__last .
|
|
C3: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
C4: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
C5: start_byte >= dns_types__packet_bytes_range__first .
|
|
C6: start_byte <= dns_types__packet_bytes_range__last .
|
|
C7: start_byte <= dns_types__packet_size .
|
|
C8: answer_count <= dns_types__unsigned_short__last -
|
|
rr_type__maxnumrecords .
|
|
|
|
|
|
For path(s) from assertion of line 686 to run-time check associated with statement of line 694:
|
|
|
|
procedure_create_nxdomain_response_12.
|
|
H1: answer_count = 0 .
|
|
H2: amount_trimmed >= 0 .
|
|
H3: amount_trimmed < rr_type__wirestringtypeindex__last .
|
|
H4: output_bytes <= dns_types__packet_length_range__last .
|
|
H5: current_qname_location <= output_bytes .
|
|
H6: start_byte >= dns_types__packet_bytes_range__first .
|
|
H7: start_byte <= dns_types__packet_bytes_range__last .
|
|
H8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H9: qname_location >= dns_types__qname_ptr_range__first .
|
|
H10: qname_location <= dns_types__qname_ptr_range__last .
|
|
H11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H12: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H17: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H18: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H19: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H20: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H21: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: true .
|
|
H26: true .
|
|
H27: true .
|
|
H28: true .
|
|
H29: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H30: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H31: true .
|
|
H32: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H33: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H34: start_byte <= dns_types__packet_size .
|
|
H35: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
current_name, [i___1]) >= character__first) and (element(
|
|
current_name, [i___1]) <= character__last))) .
|
|
H36: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H37: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H38: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H39: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H40: current_qname_location <=
|
|
dns_types__packet_length_range__last .
|
|
H41: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H42: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H43: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H44: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H45: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H46: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H47: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H48: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H49: answer_count >= dns_types__unsigned_short__first .
|
|
H50: answer_count <= dns_types__unsigned_short__last .
|
|
H51: answer_count >= dns_types__unsigned_short__first .
|
|
H52: answer_count <= dns_types__unsigned_short__last .
|
|
H53: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H54: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H55: start_byte >= dns_types__packet_bytes_range__first .
|
|
H56: start_byte <= dns_types__packet_bytes_range__last .
|
|
H57: start_byte <= dns_types__packet_size .
|
|
H58: answer_count <= dns_types__unsigned_short__last -
|
|
rr_type__maxnumrecords .
|
|
H59: output_bytes__2 >= dns_types__header_bits div 8 + 1 .
|
|
H60: output_bytes__2 <= dns_types__packet_size .
|
|
H61: answer_count__2 <= answer_count +
|
|
rr_type__maxnumrecords .
|
|
H62: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet__2), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet__2), [i___1]) <= dns_types__byte__last))) .
|
|
H63: fld_arcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H64: fld_arcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H65: fld_nscount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H66: fld_nscount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H67: fld_ancount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H68: fld_ancount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H69: fld_qdcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H70: fld_qdcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H71: fld_rcode(fld_header(output_packet__2)) >=
|
|
dns_types__response_code__first .
|
|
H72: fld_rcode(fld_header(output_packet__2)) <=
|
|
dns_types__response_code__last .
|
|
H73: true .
|
|
H74: true .
|
|
H75: true .
|
|
H76: true .
|
|
H77: true .
|
|
H78: true .
|
|
H79: true .
|
|
H80: fld_opcode(fld_header(output_packet__2)) >=
|
|
dns_types__opcode_type__first .
|
|
H81: fld_opcode(fld_header(output_packet__2)) <=
|
|
dns_types__opcode_type__last .
|
|
H82: true .
|
|
H83: fld_messageid(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H84: fld_messageid(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H85: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H86: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H87: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H88: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
->
|
|
C1: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
C2: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
C3: answer_count__2 >= dns_types__unsigned_short__first .
|
|
C4: answer_count__2 <= dns_types__unsigned_short__last .
|
|
|
|
|
|
For path(s) from assertion of line 686 to run-time check associated with statement of line 702:
|
|
|
|
procedure_create_nxdomain_response_13.
|
|
H1: answer_count = 0 .
|
|
H2: amount_trimmed >= 0 .
|
|
H3: amount_trimmed < rr_type__wirestringtypeindex__last .
|
|
H4: output_bytes <= dns_types__packet_length_range__last .
|
|
H5: current_qname_location <= output_bytes .
|
|
H6: start_byte >= dns_types__packet_bytes_range__first .
|
|
H7: start_byte <= dns_types__packet_bytes_range__last .
|
|
H8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H9: qname_location >= dns_types__qname_ptr_range__first .
|
|
H10: qname_location <= dns_types__qname_ptr_range__last .
|
|
H11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H12: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H17: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H18: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H19: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H20: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H21: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: true .
|
|
H26: true .
|
|
H27: true .
|
|
H28: true .
|
|
H29: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H30: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H31: true .
|
|
H32: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H33: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H34: start_byte <= dns_types__packet_size .
|
|
H35: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
current_name, [i___1]) >= character__first) and (element(
|
|
current_name, [i___1]) <= character__last))) .
|
|
H36: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H37: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H38: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H39: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H40: current_qname_location <=
|
|
dns_types__packet_length_range__last .
|
|
H41: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H42: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H43: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H44: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H45: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H46: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H47: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H48: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H49: answer_count >= dns_types__unsigned_short__first .
|
|
H50: answer_count <= dns_types__unsigned_short__last .
|
|
H51: answer_count >= dns_types__unsigned_short__first .
|
|
H52: answer_count <= dns_types__unsigned_short__last .
|
|
H53: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H54: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H55: start_byte >= dns_types__packet_bytes_range__first .
|
|
H56: start_byte <= dns_types__packet_bytes_range__last .
|
|
H57: start_byte <= dns_types__packet_size .
|
|
H58: answer_count <= dns_types__unsigned_short__last -
|
|
rr_type__maxnumrecords .
|
|
H59: output_bytes__2 >= dns_types__header_bits div 8 + 1 .
|
|
H60: output_bytes__2 <= dns_types__packet_size .
|
|
H61: answer_count__2 <= answer_count +
|
|
rr_type__maxnumrecords .
|
|
H62: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet__2), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet__2), [i___1]) <= dns_types__byte__last))) .
|
|
H63: fld_arcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H64: fld_arcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H65: fld_nscount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H66: fld_nscount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H67: fld_ancount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H68: fld_ancount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H69: fld_qdcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H70: fld_qdcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H71: fld_rcode(fld_header(output_packet__2)) >=
|
|
dns_types__response_code__first .
|
|
H72: fld_rcode(fld_header(output_packet__2)) <=
|
|
dns_types__response_code__last .
|
|
H73: true .
|
|
H74: true .
|
|
H75: true .
|
|
H76: true .
|
|
H77: true .
|
|
H78: true .
|
|
H79: true .
|
|
H80: fld_opcode(fld_header(output_packet__2)) >=
|
|
dns_types__opcode_type__first .
|
|
H81: fld_opcode(fld_header(output_packet__2)) <=
|
|
dns_types__opcode_type__last .
|
|
H82: true .
|
|
H83: fld_messageid(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H84: fld_messageid(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H85: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H86: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H87: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H88: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H89: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H90: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H91: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H92: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H93: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H94: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H95: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
->
|
|
C1: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
C2: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
|
|
|
|
For path(s) from assertion of line 686 to run-time check associated with statement of line 703:
|
|
|
|
procedure_create_nxdomain_response_14.
|
|
H1: answer_count = 0 .
|
|
H2: amount_trimmed >= 0 .
|
|
H3: amount_trimmed < rr_type__wirestringtypeindex__last .
|
|
H4: output_bytes <= dns_types__packet_length_range__last .
|
|
H5: current_qname_location <= output_bytes .
|
|
H6: start_byte >= dns_types__packet_bytes_range__first .
|
|
H7: start_byte <= dns_types__packet_bytes_range__last .
|
|
H8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H9: qname_location >= dns_types__qname_ptr_range__first .
|
|
H10: qname_location <= dns_types__qname_ptr_range__last .
|
|
H11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H12: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H17: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H18: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H19: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H20: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H21: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: true .
|
|
H26: true .
|
|
H27: true .
|
|
H28: true .
|
|
H29: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H30: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H31: true .
|
|
H32: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H33: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H34: start_byte <= dns_types__packet_size .
|
|
H35: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
current_name, [i___1]) >= character__first) and (element(
|
|
current_name, [i___1]) <= character__last))) .
|
|
H36: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H37: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H38: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H39: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H40: current_qname_location <=
|
|
dns_types__packet_length_range__last .
|
|
H41: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H42: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H43: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H44: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H45: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H46: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H47: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H48: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H49: answer_count >= dns_types__unsigned_short__first .
|
|
H50: answer_count <= dns_types__unsigned_short__last .
|
|
H51: answer_count >= dns_types__unsigned_short__first .
|
|
H52: answer_count <= dns_types__unsigned_short__last .
|
|
H53: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H54: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H55: start_byte >= dns_types__packet_bytes_range__first .
|
|
H56: start_byte <= dns_types__packet_bytes_range__last .
|
|
H57: start_byte <= dns_types__packet_size .
|
|
H58: answer_count <= dns_types__unsigned_short__last -
|
|
rr_type__maxnumrecords .
|
|
H59: output_bytes__2 >= dns_types__header_bits div 8 + 1 .
|
|
H60: output_bytes__2 <= dns_types__packet_size .
|
|
H61: answer_count__2 <= answer_count +
|
|
rr_type__maxnumrecords .
|
|
H62: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet__2), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet__2), [i___1]) <= dns_types__byte__last))) .
|
|
H63: fld_arcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H64: fld_arcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H65: fld_nscount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H66: fld_nscount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H67: fld_ancount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H68: fld_ancount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H69: fld_qdcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H70: fld_qdcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H71: fld_rcode(fld_header(output_packet__2)) >=
|
|
dns_types__response_code__first .
|
|
H72: fld_rcode(fld_header(output_packet__2)) <=
|
|
dns_types__response_code__last .
|
|
H73: true .
|
|
H74: true .
|
|
H75: true .
|
|
H76: true .
|
|
H77: true .
|
|
H78: true .
|
|
H79: true .
|
|
H80: fld_opcode(fld_header(output_packet__2)) >=
|
|
dns_types__opcode_type__first .
|
|
H81: fld_opcode(fld_header(output_packet__2)) <=
|
|
dns_types__opcode_type__last .
|
|
H82: true .
|
|
H83: fld_messageid(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H84: fld_messageid(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H85: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H86: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H87: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H88: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H89: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H90: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H91: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H92: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H93: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H94: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H95: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H96: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H97: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H98: amount_trimmed >= natural__first .
|
|
H99: amount_trimmed <= natural__last .
|
|
->
|
|
C1: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >=
|
|
natural__first .
|
|
C2: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <=
|
|
natural__last .
|
|
C3: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >=
|
|
natural__first .
|
|
C4: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <=
|
|
natural__last .
|
|
C5: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
|
|
C6: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
|
|
C7: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
C8: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 708:
|
|
|
|
procedure_create_nxdomain_response_15.
|
|
H1: start_byte <= dns_types__packet_size .
|
|
H2: start_byte >= dns_types__packet_bytes_range__first .
|
|
H3: start_byte <= dns_types__packet_bytes_range__last .
|
|
H4: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H5: qname_location >= dns_types__qname_ptr_range__first .
|
|
H6: qname_location <= dns_types__qname_ptr_range__last .
|
|
H7: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H8: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H9: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H10: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H11: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H12: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H17: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H18: true .
|
|
H19: true .
|
|
H20: true .
|
|
H21: true .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H26: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H27: true .
|
|
H28: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H29: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H30: qname_location >= dns_types__qname_ptr_range__first .
|
|
H31: qname_location <= dns_types__qname_ptr_range__last .
|
|
H32: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H33: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H34: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H35: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H36: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__base__first .
|
|
H37: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__base__last .
|
|
H38: dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__first .
|
|
H39: dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__last .
|
|
H40: dns_types__header_bits div 8 >= system__min_int .
|
|
H41: dns_types__header_bits div 8 <= system__max_int .
|
|
H42: 8 <> 0 .
|
|
H43: dns_types__name_error >= dns_types__response_code__first .
|
|
H44: dns_types__name_error <= dns_types__response_code__last .
|
|
H45: 0 >= dns_types__unsigned_short__first .
|
|
H46: 0 <= dns_types__unsigned_short__last .
|
|
H47: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H48: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H49: 0 >= dns_types__unsigned_short__first .
|
|
H50: 0 <= dns_types__unsigned_short__last .
|
|
H51: 0 >= natural__first .
|
|
H52: 0 <= natural__last .
|
|
H53: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H54: qname_location >= dns_types__qname_ptr_range__first .
|
|
H55: qname_location <= dns_types__qname_ptr_range__last .
|
|
H56: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__qname_ptr_range__first .
|
|
H57: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__qname_ptr_range__last .
|
|
H58: element(domainname, [rr_type__wirestringtypeindex__first]) >=
|
|
natural__first .
|
|
H59: element(domainname, [rr_type__wirestringtypeindex__first]) <=
|
|
natural__last .
|
|
H60: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H61: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H62: not ((0 = 0) and (((0 < rr_type__wirestringtypeindex__last) and (element(
|
|
domainname, [rr_type__wirestringtypeindex__first]) <> 0)) and (
|
|
qname_location <= start_byte +
|
|
dns_types__header_bits div 8))) .
|
|
H63: 0 >= dns_types__unsigned_short__first .
|
|
H64: 0 <= dns_types__unsigned_short__last .
|
|
H65: 0 >= 1 .
|
|
H66: 0 >= dns_types__unsigned_short__first .
|
|
H67: 0 <= dns_types__unsigned_short__last .
|
|
->
|
|
C1: 0 >= dns_types__unsigned_short__first .
|
|
C2: 0 <= dns_types__unsigned_short__last .
|
|
|
|
|
|
procedure_create_nxdomain_response_16.
|
|
H1: start_byte <= dns_types__packet_size .
|
|
H2: start_byte >= dns_types__packet_bytes_range__first .
|
|
H3: start_byte <= dns_types__packet_bytes_range__last .
|
|
H4: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H5: qname_location >= dns_types__qname_ptr_range__first .
|
|
H6: qname_location <= dns_types__qname_ptr_range__last .
|
|
H7: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H8: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H9: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H10: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H11: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H12: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H17: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H18: true .
|
|
H19: true .
|
|
H20: true .
|
|
H21: true .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H26: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H27: true .
|
|
H28: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H29: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H30: qname_location >= dns_types__qname_ptr_range__first .
|
|
H31: qname_location <= dns_types__qname_ptr_range__last .
|
|
H32: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H33: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H34: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H35: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H36: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__base__first .
|
|
H37: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__base__last .
|
|
H38: dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__first .
|
|
H39: dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__last .
|
|
H40: dns_types__header_bits div 8 >= system__min_int .
|
|
H41: dns_types__header_bits div 8 <= system__max_int .
|
|
H42: 8 <> 0 .
|
|
H43: dns_types__name_error >= dns_types__response_code__first .
|
|
H44: dns_types__name_error <= dns_types__response_code__last .
|
|
H45: 0 >= dns_types__unsigned_short__first .
|
|
H46: 0 <= dns_types__unsigned_short__last .
|
|
H47: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H48: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H49: 0 >= dns_types__unsigned_short__first .
|
|
H50: 0 <= dns_types__unsigned_short__last .
|
|
H51: 0 >= natural__first .
|
|
H52: 0 <= natural__last .
|
|
H53: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H54: qname_location >= dns_types__qname_ptr_range__first .
|
|
H55: qname_location <= dns_types__qname_ptr_range__last .
|
|
H56: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__qname_ptr_range__first .
|
|
H57: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__qname_ptr_range__last .
|
|
H58: element(domainname, [rr_type__wirestringtypeindex__first]) >=
|
|
natural__first .
|
|
H59: element(domainname, [rr_type__wirestringtypeindex__first]) <=
|
|
natural__last .
|
|
H60: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H61: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H62: not ((0 = 0) and (((0 < rr_type__wirestringtypeindex__last) and (element(
|
|
domainname, [rr_type__wirestringtypeindex__first]) <> 0)) and (
|
|
qname_location <= start_byte +
|
|
dns_types__header_bits div 8))) .
|
|
H63: 0 >= dns_types__unsigned_short__first .
|
|
H64: 0 <= dns_types__unsigned_short__last .
|
|
H65: not (0 >= 1) .
|
|
H66: 0 >= dns_types__unsigned_short__first .
|
|
H67: 0 <= dns_types__unsigned_short__last .
|
|
->
|
|
C1: 0 >= dns_types__unsigned_short__first .
|
|
C2: 0 <= dns_types__unsigned_short__last .
|
|
|
|
|
|
For path(s) from assertion of line 686 to run-time check associated with statement of line 708:
|
|
|
|
procedure_create_nxdomain_response_17.
|
|
H1: answer_count = 0 .
|
|
H2: amount_trimmed >= 0 .
|
|
H3: amount_trimmed < rr_type__wirestringtypeindex__last .
|
|
H4: output_bytes <= dns_types__packet_length_range__last .
|
|
H5: current_qname_location <= output_bytes .
|
|
H6: start_byte >= dns_types__packet_bytes_range__first .
|
|
H7: start_byte <= dns_types__packet_bytes_range__last .
|
|
H8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H9: qname_location >= dns_types__qname_ptr_range__first .
|
|
H10: qname_location <= dns_types__qname_ptr_range__last .
|
|
H11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H12: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H17: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H18: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H19: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H20: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H21: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: true .
|
|
H26: true .
|
|
H27: true .
|
|
H28: true .
|
|
H29: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H30: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H31: true .
|
|
H32: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H33: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H34: start_byte <= dns_types__packet_size .
|
|
H35: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
current_name, [i___1]) >= character__first) and (element(
|
|
current_name, [i___1]) <= character__last))) .
|
|
H36: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H37: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H38: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H39: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H40: current_qname_location <=
|
|
dns_types__packet_length_range__last .
|
|
H41: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H42: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H43: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H44: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H45: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H46: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H47: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H48: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H49: answer_count >= dns_types__unsigned_short__first .
|
|
H50: answer_count <= dns_types__unsigned_short__last .
|
|
H51: answer_count >= dns_types__unsigned_short__first .
|
|
H52: answer_count <= dns_types__unsigned_short__last .
|
|
H53: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H54: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H55: start_byte >= dns_types__packet_bytes_range__first .
|
|
H56: start_byte <= dns_types__packet_bytes_range__last .
|
|
H57: start_byte <= dns_types__packet_size .
|
|
H58: answer_count <= dns_types__unsigned_short__last -
|
|
rr_type__maxnumrecords .
|
|
H59: output_bytes__2 >= dns_types__header_bits div 8 + 1 .
|
|
H60: output_bytes__2 <= dns_types__packet_size .
|
|
H61: answer_count__2 <= answer_count +
|
|
rr_type__maxnumrecords .
|
|
H62: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet__2), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet__2), [i___1]) <= dns_types__byte__last))) .
|
|
H63: fld_arcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H64: fld_arcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H65: fld_nscount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H66: fld_nscount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H67: fld_ancount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H68: fld_ancount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H69: fld_qdcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H70: fld_qdcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H71: fld_rcode(fld_header(output_packet__2)) >=
|
|
dns_types__response_code__first .
|
|
H72: fld_rcode(fld_header(output_packet__2)) <=
|
|
dns_types__response_code__last .
|
|
H73: true .
|
|
H74: true .
|
|
H75: true .
|
|
H76: true .
|
|
H77: true .
|
|
H78: true .
|
|
H79: true .
|
|
H80: fld_opcode(fld_header(output_packet__2)) >=
|
|
dns_types__opcode_type__first .
|
|
H81: fld_opcode(fld_header(output_packet__2)) <=
|
|
dns_types__opcode_type__last .
|
|
H82: true .
|
|
H83: fld_messageid(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H84: fld_messageid(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H85: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H86: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H87: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H88: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H89: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H90: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H91: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H92: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H93: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H94: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H95: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H96: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H97: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H98: amount_trimmed >= natural__first .
|
|
H99: amount_trimmed <= natural__last .
|
|
H100: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >=
|
|
natural__first .
|
|
H101: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <=
|
|
natural__last .
|
|
H102: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >=
|
|
natural__first .
|
|
H103: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <=
|
|
natural__last .
|
|
H104: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
|
|
H105: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
|
|
H106: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H107: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H108: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H109: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H110: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H111: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H112: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >=
|
|
natural__first .
|
|
H113: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <=
|
|
natural__last .
|
|
H114: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H115: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H116: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H117: output_bytes__2 >= dns_types__qname_ptr_range__first .
|
|
H118: output_bytes__2 <= dns_types__qname_ptr_range__last .
|
|
H119: element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) >=
|
|
natural__first .
|
|
H120: element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <=
|
|
natural__last .
|
|
H121: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H122: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H123: not ((answer_count__2 = 0) and (((amount_trimmed + (element(
|
|
domainname, [rr_type__wirestringtypeindex__first]) + 1) <
|
|
rr_type__wirestringtypeindex__last) and (element(
|
|
trimmed_name__1, [rr_type__wirestringtypeindex__first]) <> 0)) and (
|
|
new_qname_location__1 <= output_bytes__2))) .
|
|
H124: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H125: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H126: answer_count__2 >= 1 .
|
|
H127: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H128: answer_count__2 <= dns_types__unsigned_short__last .
|
|
->
|
|
C1: answer_count__2 >= dns_types__unsigned_short__first .
|
|
C2: answer_count__2 <= dns_types__unsigned_short__last .
|
|
|
|
|
|
procedure_create_nxdomain_response_18.
|
|
H1: answer_count = 0 .
|
|
H2: amount_trimmed >= 0 .
|
|
H3: amount_trimmed < rr_type__wirestringtypeindex__last .
|
|
H4: output_bytes <= dns_types__packet_length_range__last .
|
|
H5: current_qname_location <= output_bytes .
|
|
H6: start_byte >= dns_types__packet_bytes_range__first .
|
|
H7: start_byte <= dns_types__packet_bytes_range__last .
|
|
H8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H9: qname_location >= dns_types__qname_ptr_range__first .
|
|
H10: qname_location <= dns_types__qname_ptr_range__last .
|
|
H11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H12: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H17: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H18: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H19: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H20: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H21: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: true .
|
|
H26: true .
|
|
H27: true .
|
|
H28: true .
|
|
H29: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H30: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H31: true .
|
|
H32: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H33: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H34: start_byte <= dns_types__packet_size .
|
|
H35: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
current_name, [i___1]) >= character__first) and (element(
|
|
current_name, [i___1]) <= character__last))) .
|
|
H36: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H37: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H38: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H39: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H40: current_qname_location <=
|
|
dns_types__packet_length_range__last .
|
|
H41: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H42: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H43: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H44: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H45: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H46: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H47: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H48: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H49: answer_count >= dns_types__unsigned_short__first .
|
|
H50: answer_count <= dns_types__unsigned_short__last .
|
|
H51: answer_count >= dns_types__unsigned_short__first .
|
|
H52: answer_count <= dns_types__unsigned_short__last .
|
|
H53: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H54: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H55: start_byte >= dns_types__packet_bytes_range__first .
|
|
H56: start_byte <= dns_types__packet_bytes_range__last .
|
|
H57: start_byte <= dns_types__packet_size .
|
|
H58: answer_count <= dns_types__unsigned_short__last -
|
|
rr_type__maxnumrecords .
|
|
H59: output_bytes__2 >= dns_types__header_bits div 8 + 1 .
|
|
H60: output_bytes__2 <= dns_types__packet_size .
|
|
H61: answer_count__2 <= answer_count +
|
|
rr_type__maxnumrecords .
|
|
H62: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet__2), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet__2), [i___1]) <= dns_types__byte__last))) .
|
|
H63: fld_arcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H64: fld_arcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H65: fld_nscount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H66: fld_nscount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H67: fld_ancount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H68: fld_ancount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H69: fld_qdcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H70: fld_qdcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H71: fld_rcode(fld_header(output_packet__2)) >=
|
|
dns_types__response_code__first .
|
|
H72: fld_rcode(fld_header(output_packet__2)) <=
|
|
dns_types__response_code__last .
|
|
H73: true .
|
|
H74: true .
|
|
H75: true .
|
|
H76: true .
|
|
H77: true .
|
|
H78: true .
|
|
H79: true .
|
|
H80: fld_opcode(fld_header(output_packet__2)) >=
|
|
dns_types__opcode_type__first .
|
|
H81: fld_opcode(fld_header(output_packet__2)) <=
|
|
dns_types__opcode_type__last .
|
|
H82: true .
|
|
H83: fld_messageid(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H84: fld_messageid(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H85: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H86: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H87: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H88: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H89: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H90: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H91: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H92: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H93: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H94: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H95: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H96: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H97: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H98: amount_trimmed >= natural__first .
|
|
H99: amount_trimmed <= natural__last .
|
|
H100: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >=
|
|
natural__first .
|
|
H101: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <=
|
|
natural__last .
|
|
H102: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >=
|
|
natural__first .
|
|
H103: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <=
|
|
natural__last .
|
|
H104: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
|
|
H105: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
|
|
H106: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H107: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H108: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H109: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H110: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H111: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H112: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >=
|
|
natural__first .
|
|
H113: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <=
|
|
natural__last .
|
|
H114: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H115: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H116: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H117: output_bytes__2 >= dns_types__qname_ptr_range__first .
|
|
H118: output_bytes__2 <= dns_types__qname_ptr_range__last .
|
|
H119: element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) >=
|
|
natural__first .
|
|
H120: element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <=
|
|
natural__last .
|
|
H121: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H122: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H123: not ((answer_count__2 = 0) and (((amount_trimmed + (element(
|
|
domainname, [rr_type__wirestringtypeindex__first]) + 1) <
|
|
rr_type__wirestringtypeindex__last) and (element(
|
|
trimmed_name__1, [rr_type__wirestringtypeindex__first]) <> 0)) and (
|
|
new_qname_location__1 <= output_bytes__2))) .
|
|
H124: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H125: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H126: not (answer_count__2 >= 1) .
|
|
H127: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H128: answer_count__2 <= dns_types__unsigned_short__last .
|
|
->
|
|
C1: answer_count__2 >= dns_types__unsigned_short__first .
|
|
C2: answer_count__2 <= dns_types__unsigned_short__last .
|
|
|
|
|
|
For path(s) from start to finish:
|
|
|
|
procedure_create_nxdomain_response_19.
|
|
H1: start_byte <= dns_types__packet_size .
|
|
H2: start_byte >= dns_types__packet_bytes_range__first .
|
|
H3: start_byte <= dns_types__packet_bytes_range__last .
|
|
H4: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H5: qname_location >= dns_types__qname_ptr_range__first .
|
|
H6: qname_location <= dns_types__qname_ptr_range__last .
|
|
H7: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H8: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H9: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H10: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H11: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H12: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H17: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H18: true .
|
|
H19: true .
|
|
H20: true .
|
|
H21: true .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H26: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H27: true .
|
|
H28: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H29: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H30: qname_location >= dns_types__qname_ptr_range__first .
|
|
H31: qname_location <= dns_types__qname_ptr_range__last .
|
|
H32: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H33: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H34: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H35: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H36: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__base__first .
|
|
H37: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__base__last .
|
|
H38: dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__first .
|
|
H39: dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__last .
|
|
H40: dns_types__header_bits div 8 >= system__min_int .
|
|
H41: dns_types__header_bits div 8 <= system__max_int .
|
|
H42: 8 <> 0 .
|
|
H43: dns_types__name_error >= dns_types__response_code__first .
|
|
H44: dns_types__name_error <= dns_types__response_code__last .
|
|
H45: 0 >= dns_types__unsigned_short__first .
|
|
H46: 0 <= dns_types__unsigned_short__last .
|
|
H47: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H48: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H49: 0 >= dns_types__unsigned_short__first .
|
|
H50: 0 <= dns_types__unsigned_short__last .
|
|
H51: 0 >= natural__first .
|
|
H52: 0 <= natural__last .
|
|
H53: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H54: qname_location >= dns_types__qname_ptr_range__first .
|
|
H55: qname_location <= dns_types__qname_ptr_range__last .
|
|
H56: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__qname_ptr_range__first .
|
|
H57: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__qname_ptr_range__last .
|
|
H58: element(domainname, [rr_type__wirestringtypeindex__first]) >=
|
|
natural__first .
|
|
H59: element(domainname, [rr_type__wirestringtypeindex__first]) <=
|
|
natural__last .
|
|
H60: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H61: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H62: not ((0 = 0) and (((0 < rr_type__wirestringtypeindex__last) and (element(
|
|
domainname, [rr_type__wirestringtypeindex__first]) <> 0)) and (
|
|
qname_location <= start_byte +
|
|
dns_types__header_bits div 8))) .
|
|
H63: 0 >= dns_types__unsigned_short__first .
|
|
H64: 0 <= dns_types__unsigned_short__last .
|
|
H65: 0 >= 1 .
|
|
H66: 0 >= dns_types__unsigned_short__first .
|
|
H67: 0 <= dns_types__unsigned_short__last .
|
|
H68: 0 >= dns_types__unsigned_short__first .
|
|
H69: 0 <= dns_types__unsigned_short__last .
|
|
->
|
|
C1: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__header_bits div 8 + 1 .
|
|
C2: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_size .
|
|
|
|
|
|
procedure_create_nxdomain_response_20.
|
|
H1: start_byte <= dns_types__packet_size .
|
|
H2: start_byte >= dns_types__packet_bytes_range__first .
|
|
H3: start_byte <= dns_types__packet_bytes_range__last .
|
|
H4: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H5: qname_location >= dns_types__qname_ptr_range__first .
|
|
H6: qname_location <= dns_types__qname_ptr_range__last .
|
|
H7: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H8: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H9: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H10: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H11: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H12: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H17: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H18: true .
|
|
H19: true .
|
|
H20: true .
|
|
H21: true .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H26: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H27: true .
|
|
H28: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H29: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H30: qname_location >= dns_types__qname_ptr_range__first .
|
|
H31: qname_location <= dns_types__qname_ptr_range__last .
|
|
H32: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H33: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H34: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H35: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H36: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__base__first .
|
|
H37: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__base__last .
|
|
H38: dns_types__header_bits div 8 >=
|
|
dns_types__packet_bytes_range__first .
|
|
H39: dns_types__header_bits div 8 <=
|
|
dns_types__packet_bytes_range__last .
|
|
H40: dns_types__header_bits div 8 >= system__min_int .
|
|
H41: dns_types__header_bits div 8 <= system__max_int .
|
|
H42: 8 <> 0 .
|
|
H43: dns_types__name_error >= dns_types__response_code__first .
|
|
H44: dns_types__name_error <= dns_types__response_code__last .
|
|
H45: 0 >= dns_types__unsigned_short__first .
|
|
H46: 0 <= dns_types__unsigned_short__last .
|
|
H47: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__packet_length_range__first .
|
|
H48: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_length_range__last .
|
|
H49: 0 >= dns_types__unsigned_short__first .
|
|
H50: 0 <= dns_types__unsigned_short__last .
|
|
H51: 0 >= natural__first .
|
|
H52: 0 <= natural__last .
|
|
H53: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H54: qname_location >= dns_types__qname_ptr_range__first .
|
|
H55: qname_location <= dns_types__qname_ptr_range__last .
|
|
H56: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__qname_ptr_range__first .
|
|
H57: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__qname_ptr_range__last .
|
|
H58: element(domainname, [rr_type__wirestringtypeindex__first]) >=
|
|
natural__first .
|
|
H59: element(domainname, [rr_type__wirestringtypeindex__first]) <=
|
|
natural__last .
|
|
H60: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H61: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H62: not ((0 = 0) and (((0 < rr_type__wirestringtypeindex__last) and (element(
|
|
domainname, [rr_type__wirestringtypeindex__first]) <> 0)) and (
|
|
qname_location <= start_byte +
|
|
dns_types__header_bits div 8))) .
|
|
H63: 0 >= dns_types__unsigned_short__first .
|
|
H64: 0 <= dns_types__unsigned_short__last .
|
|
H65: not (0 >= 1) .
|
|
H66: 0 >= dns_types__unsigned_short__first .
|
|
H67: 0 <= dns_types__unsigned_short__last .
|
|
H68: 0 >= dns_types__unsigned_short__first .
|
|
H69: 0 <= dns_types__unsigned_short__last .
|
|
->
|
|
C1: start_byte + dns_types__header_bits div 8 >=
|
|
dns_types__header_bits div 8 + 1 .
|
|
C2: start_byte + dns_types__header_bits div 8 <=
|
|
dns_types__packet_size .
|
|
|
|
|
|
For path(s) from assertion of line 686 to finish:
|
|
|
|
procedure_create_nxdomain_response_21.
|
|
H1: answer_count = 0 .
|
|
H2: amount_trimmed >= 0 .
|
|
H3: amount_trimmed < rr_type__wirestringtypeindex__last .
|
|
H4: output_bytes <= dns_types__packet_length_range__last .
|
|
H5: current_qname_location <= output_bytes .
|
|
H6: start_byte >= dns_types__packet_bytes_range__first .
|
|
H7: start_byte <= dns_types__packet_bytes_range__last .
|
|
H8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H9: qname_location >= dns_types__qname_ptr_range__first .
|
|
H10: qname_location <= dns_types__qname_ptr_range__last .
|
|
H11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H12: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H17: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H18: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H19: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H20: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H21: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: true .
|
|
H26: true .
|
|
H27: true .
|
|
H28: true .
|
|
H29: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H30: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H31: true .
|
|
H32: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H33: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H34: start_byte <= dns_types__packet_size .
|
|
H35: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
current_name, [i___1]) >= character__first) and (element(
|
|
current_name, [i___1]) <= character__last))) .
|
|
H36: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H37: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H38: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H39: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H40: current_qname_location <=
|
|
dns_types__packet_length_range__last .
|
|
H41: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H42: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H43: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H44: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H45: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H46: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H47: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H48: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H49: answer_count >= dns_types__unsigned_short__first .
|
|
H50: answer_count <= dns_types__unsigned_short__last .
|
|
H51: answer_count >= dns_types__unsigned_short__first .
|
|
H52: answer_count <= dns_types__unsigned_short__last .
|
|
H53: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H54: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H55: start_byte >= dns_types__packet_bytes_range__first .
|
|
H56: start_byte <= dns_types__packet_bytes_range__last .
|
|
H57: start_byte <= dns_types__packet_size .
|
|
H58: answer_count <= dns_types__unsigned_short__last -
|
|
rr_type__maxnumrecords .
|
|
H59: output_bytes__2 >= dns_types__header_bits div 8 + 1 .
|
|
H60: output_bytes__2 <= dns_types__packet_size .
|
|
H61: answer_count__2 <= answer_count +
|
|
rr_type__maxnumrecords .
|
|
H62: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet__2), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet__2), [i___1]) <= dns_types__byte__last))) .
|
|
H63: fld_arcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H64: fld_arcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H65: fld_nscount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H66: fld_nscount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H67: fld_ancount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H68: fld_ancount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H69: fld_qdcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H70: fld_qdcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H71: fld_rcode(fld_header(output_packet__2)) >=
|
|
dns_types__response_code__first .
|
|
H72: fld_rcode(fld_header(output_packet__2)) <=
|
|
dns_types__response_code__last .
|
|
H73: true .
|
|
H74: true .
|
|
H75: true .
|
|
H76: true .
|
|
H77: true .
|
|
H78: true .
|
|
H79: true .
|
|
H80: fld_opcode(fld_header(output_packet__2)) >=
|
|
dns_types__opcode_type__first .
|
|
H81: fld_opcode(fld_header(output_packet__2)) <=
|
|
dns_types__opcode_type__last .
|
|
H82: true .
|
|
H83: fld_messageid(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H84: fld_messageid(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H85: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H86: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H87: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H88: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H89: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H90: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H91: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H92: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H93: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H94: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H95: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H96: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H97: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H98: amount_trimmed >= natural__first .
|
|
H99: amount_trimmed <= natural__last .
|
|
H100: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >=
|
|
natural__first .
|
|
H101: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <=
|
|
natural__last .
|
|
H102: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >=
|
|
natural__first .
|
|
H103: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <=
|
|
natural__last .
|
|
H104: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
|
|
H105: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
|
|
H106: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H107: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H108: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H109: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H110: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H111: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H112: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >=
|
|
natural__first .
|
|
H113: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <=
|
|
natural__last .
|
|
H114: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H115: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H116: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H117: output_bytes__2 >= dns_types__qname_ptr_range__first .
|
|
H118: output_bytes__2 <= dns_types__qname_ptr_range__last .
|
|
H119: element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) >=
|
|
natural__first .
|
|
H120: element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <=
|
|
natural__last .
|
|
H121: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H122: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H123: not ((answer_count__2 = 0) and (((amount_trimmed + (element(
|
|
domainname, [rr_type__wirestringtypeindex__first]) + 1) <
|
|
rr_type__wirestringtypeindex__last) and (element(
|
|
trimmed_name__1, [rr_type__wirestringtypeindex__first]) <> 0)) and (
|
|
new_qname_location__1 <= output_bytes__2))) .
|
|
H124: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H125: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H126: answer_count__2 >= 1 .
|
|
H127: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H128: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H129: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H130: answer_count__2 <= dns_types__unsigned_short__last .
|
|
->
|
|
C1: output_bytes__2 >= dns_types__header_bits div 8 + 1 .
|
|
C2: output_bytes__2 <= dns_types__packet_size .
|
|
|
|
|
|
procedure_create_nxdomain_response_22.
|
|
H1: answer_count = 0 .
|
|
H2: amount_trimmed >= 0 .
|
|
H3: amount_trimmed < rr_type__wirestringtypeindex__last .
|
|
H4: output_bytes <= dns_types__packet_length_range__last .
|
|
H5: current_qname_location <= output_bytes .
|
|
H6: start_byte >= dns_types__packet_bytes_range__first .
|
|
H7: start_byte <= dns_types__packet_bytes_range__last .
|
|
H8: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
domainname, [i___1]) >= character__first) and (element(
|
|
domainname, [i___1]) <= character__last))) .
|
|
H9: qname_location >= dns_types__qname_ptr_range__first .
|
|
H10: qname_location <= dns_types__qname_ptr_range__last .
|
|
H11: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet), [i___1]) <= dns_types__byte__last))) .
|
|
H12: fld_arcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H13: fld_arcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H14: fld_nscount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H15: fld_nscount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H16: fld_ancount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H17: fld_ancount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H18: fld_qdcount(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H19: fld_qdcount(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H20: fld_rcode(fld_header(output_packet)) >=
|
|
dns_types__response_code__first .
|
|
H21: fld_rcode(fld_header(output_packet)) <=
|
|
dns_types__response_code__last .
|
|
H22: true .
|
|
H23: true .
|
|
H24: true .
|
|
H25: true .
|
|
H26: true .
|
|
H27: true .
|
|
H28: true .
|
|
H29: fld_opcode(fld_header(output_packet)) >=
|
|
dns_types__opcode_type__first .
|
|
H30: fld_opcode(fld_header(output_packet)) <=
|
|
dns_types__opcode_type__last .
|
|
H31: true .
|
|
H32: fld_messageid(fld_header(output_packet)) >=
|
|
dns_types__unsigned_short__first .
|
|
H33: fld_messageid(fld_header(output_packet)) <=
|
|
dns_types__unsigned_short__last .
|
|
H34: start_byte <= dns_types__packet_size .
|
|
H35: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
current_name, [i___1]) >= character__first) and (element(
|
|
current_name, [i___1]) <= character__last))) .
|
|
H36: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H37: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H38: current_qname_location >= dns_types__qname_ptr_range__first .
|
|
H39: current_qname_location <= dns_types__qname_ptr_range__last .
|
|
H40: current_qname_location <=
|
|
dns_types__packet_length_range__last .
|
|
H41: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H42: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H43: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H44: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H45: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H46: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H47: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H48: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H49: answer_count >= dns_types__unsigned_short__first .
|
|
H50: answer_count <= dns_types__unsigned_short__last .
|
|
H51: answer_count >= dns_types__unsigned_short__first .
|
|
H52: answer_count <= dns_types__unsigned_short__last .
|
|
H53: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H54: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H55: start_byte >= dns_types__packet_bytes_range__first .
|
|
H56: start_byte <= dns_types__packet_bytes_range__last .
|
|
H57: start_byte <= dns_types__packet_size .
|
|
H58: answer_count <= dns_types__unsigned_short__last -
|
|
rr_type__maxnumrecords .
|
|
H59: output_bytes__2 >= dns_types__header_bits div 8 + 1 .
|
|
H60: output_bytes__2 <= dns_types__packet_size .
|
|
H61: answer_count__2 <= answer_count +
|
|
rr_type__maxnumrecords .
|
|
H62: for_all(i___1: dns_types__packet_bytes_range, ((
|
|
i___1 >= dns_types__packet_bytes_range__first) and (
|
|
i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
|
|
fld_bytes(output_packet__2), [i___1]) >=
|
|
dns_types__byte__first) and (element(fld_bytes(
|
|
output_packet__2), [i___1]) <= dns_types__byte__last))) .
|
|
H63: fld_arcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H64: fld_arcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H65: fld_nscount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H66: fld_nscount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H67: fld_ancount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H68: fld_ancount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H69: fld_qdcount(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H70: fld_qdcount(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H71: fld_rcode(fld_header(output_packet__2)) >=
|
|
dns_types__response_code__first .
|
|
H72: fld_rcode(fld_header(output_packet__2)) <=
|
|
dns_types__response_code__last .
|
|
H73: true .
|
|
H74: true .
|
|
H75: true .
|
|
H76: true .
|
|
H77: true .
|
|
H78: true .
|
|
H79: true .
|
|
H80: fld_opcode(fld_header(output_packet__2)) >=
|
|
dns_types__opcode_type__first .
|
|
H81: fld_opcode(fld_header(output_packet__2)) <=
|
|
dns_types__opcode_type__last .
|
|
H82: true .
|
|
H83: fld_messageid(fld_header(output_packet__2)) >=
|
|
dns_types__unsigned_short__first .
|
|
H84: fld_messageid(fld_header(output_packet__2)) <=
|
|
dns_types__unsigned_short__last .
|
|
H85: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H86: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H87: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H88: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H89: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H90: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H91: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H92: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H93: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H94: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H95: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H96: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H97: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H98: amount_trimmed >= natural__first .
|
|
H99: amount_trimmed <= natural__last .
|
|
H100: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >=
|
|
natural__first .
|
|
H101: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <=
|
|
natural__last .
|
|
H102: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >=
|
|
natural__first .
|
|
H103: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <=
|
|
natural__last .
|
|
H104: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
|
|
H105: element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
|
|
H106: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H107: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H108: output_bytes__2 >= dns_types__packet_length_range__first .
|
|
H109: output_bytes__2 <= dns_types__packet_length_range__last .
|
|
H110: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H111: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H112: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) >=
|
|
natural__first .
|
|
H113: amount_trimmed + (element(domainname, [
|
|
rr_type__wirestringtypeindex__first]) + 1) <=
|
|
natural__last .
|
|
H114: for_all(i___1: integer, ((i___1 >=
|
|
rr_type__wirestringtypeindex__first) and (i___1 <=
|
|
rr_type__wirestringtypeindex__last)) -> ((element(
|
|
trimmed_name__1, [i___1]) >= character__first) and (element(
|
|
trimmed_name__1, [i___1]) <= character__last))) .
|
|
H115: new_qname_location__1 >= dns_types__qname_ptr_range__first .
|
|
H116: new_qname_location__1 <= dns_types__qname_ptr_range__last .
|
|
H117: output_bytes__2 >= dns_types__qname_ptr_range__first .
|
|
H118: output_bytes__2 <= dns_types__qname_ptr_range__last .
|
|
H119: element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) >=
|
|
natural__first .
|
|
H120: element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <=
|
|
natural__last .
|
|
H121: rr_type__wirestringtypeindex__first >=
|
|
rr_type__wirestringtypeindex__first .
|
|
H122: rr_type__wirestringtypeindex__first <=
|
|
rr_type__wirestringtypeindex__last .
|
|
H123: not ((answer_count__2 = 0) and (((amount_trimmed + (element(
|
|
domainname, [rr_type__wirestringtypeindex__first]) + 1) <
|
|
rr_type__wirestringtypeindex__last) and (element(
|
|
trimmed_name__1, [rr_type__wirestringtypeindex__first]) <> 0)) and (
|
|
new_qname_location__1 <= output_bytes__2))) .
|
|
H124: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H125: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H126: not (answer_count__2 >= 1) .
|
|
H127: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H128: answer_count__2 <= dns_types__unsigned_short__last .
|
|
H129: answer_count__2 >= dns_types__unsigned_short__first .
|
|
H130: answer_count__2 <= dns_types__unsigned_short__last .
|
|
->
|
|
C1: output_bytes__2 >= dns_types__header_bits div 8 + 1 .
|
|
C2: output_bytes__2 <= dns_types__packet_size .
|
|
|
|
|