230 lines
13 KiB
Plaintext
230 lines
13 KiB
Plaintext
/*********************************************************/
|
|
/*Proof Rule Declarations*/
|
|
/*Examiner GPL Edition*/
|
|
|
|
/*********************************************************/
|
|
|
|
|
|
/*procedure Process_Dns_Request.Create_NXDOMAIN_Response*/
|
|
|
|
|
|
rule_family create_nxdom_rules:
|
|
X requires [X:any] &
|
|
X <= Y requires [X:ire, Y:ire] &
|
|
X >= Y requires [X:ire, Y:ire].
|
|
|
|
create_nxdom_rules(1): dns_types__packet_size may_be_replaced_by 8192.
|
|
create_nxdom_rules(2): dns_types__header_bits may_be_replaced_by 96.
|
|
create_nxdom_rules(3): rr_type__maxnumrecords may_be_replaced_by 64.
|
|
create_nxdom_rules(4): system__min_int may_be_replaced_by -9223372036854775808.
|
|
create_nxdom_rules(5): system__max_int may_be_replaced_by 9223372036854775807.
|
|
create_nxdom_rules(6): integer__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(7): integer__first may_be_replaced_by -2147483648.
|
|
create_nxdom_rules(8): integer__last may_be_replaced_by 2147483647.
|
|
create_nxdom_rules(9): integer__base__first may_be_replaced_by -2147483648.
|
|
create_nxdom_rules(10): integer__base__last may_be_replaced_by 2147483647.
|
|
create_nxdom_rules(11): character__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(12): character__first may_be_replaced_by 0.
|
|
create_nxdom_rules(13): character__last may_be_replaced_by 255.
|
|
create_nxdom_rules(14): character__base__first may_be_replaced_by 0.
|
|
create_nxdom_rules(15): character__base__last may_be_replaced_by 255.
|
|
create_nxdom_rules(16): natural__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(17): natural__first may_be_replaced_by 0.
|
|
create_nxdom_rules(18): natural__last may_be_replaced_by 2147483647.
|
|
create_nxdom_rules(19): natural__base__first may_be_replaced_by -2147483648.
|
|
create_nxdom_rules(20): natural__base__last may_be_replaced_by 2147483647.
|
|
create_nxdom_rules(21): positive__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(22): positive__first may_be_replaced_by 1.
|
|
create_nxdom_rules(23): positive__last may_be_replaced_by 2147483647.
|
|
create_nxdom_rules(24): positive__base__first may_be_replaced_by -2147483648.
|
|
create_nxdom_rules(25): positive__base__last may_be_replaced_by 2147483647.
|
|
create_nxdom_rules(26): dns_types__qname_ptr_range__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(27): dns_types__qname_ptr_range__first may_be_replaced_by 0.
|
|
create_nxdom_rules(28): dns_types__qname_ptr_range__last may_be_replaced_by 16383.
|
|
create_nxdom_rules(29): dns_types__qname_ptr_range__base__first <=
|
|
dns_types__qname_ptr_range__base__last may_be_deduced.
|
|
create_nxdom_rules(30): dns_types__qname_ptr_range__base__first <=
|
|
dns_types__qname_ptr_range__first may_be_deduced.
|
|
create_nxdom_rules(31): dns_types__qname_ptr_range__base__last >=
|
|
dns_types__qname_ptr_range__last may_be_deduced.
|
|
create_nxdom_rules(32): dns_types__packet_length_range__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(33): dns_types__packet_length_range__first may_be_replaced_by 0.
|
|
create_nxdom_rules(34): dns_types__packet_length_range__last may_be_replaced_by 8192.
|
|
create_nxdom_rules(35): dns_types__packet_length_range__base__first may_be_replaced_by -2147483648.
|
|
create_nxdom_rules(36): dns_types__packet_length_range__base__last may_be_replaced_by 2147483647.
|
|
create_nxdom_rules(37): dns_types__packet_bytes_range__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(38): dns_types__packet_bytes_range__first may_be_replaced_by 1.
|
|
create_nxdom_rules(39): dns_types__packet_bytes_range__last may_be_replaced_by 8180.
|
|
create_nxdom_rules(40): dns_types__packet_bytes_range__base__first may_be_replaced_by -2147483648.
|
|
create_nxdom_rules(41): dns_types__packet_bytes_range__base__last may_be_replaced_by 2147483647.
|
|
create_nxdom_rules(42): dns_types__byte__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(43): dns_types__byte__size may_be_replaced_by 8.
|
|
create_nxdom_rules(44): dns_types__byte__first may_be_replaced_by 0.
|
|
create_nxdom_rules(45): dns_types__byte__last may_be_replaced_by 255.
|
|
create_nxdom_rules(46): dns_types__byte__base__first may_be_replaced_by 0.
|
|
create_nxdom_rules(47): dns_types__byte__base__last may_be_replaced_by 255.
|
|
create_nxdom_rules(48): dns_types__byte__modulus may_be_replaced_by 256.
|
|
create_nxdom_rules(49): dns_types__unsigned_short__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(50): dns_types__unsigned_short__size may_be_replaced_by 16.
|
|
create_nxdom_rules(51): dns_types__unsigned_short__first may_be_replaced_by 0.
|
|
create_nxdom_rules(52): dns_types__unsigned_short__last may_be_replaced_by 65535.
|
|
create_nxdom_rules(53): dns_types__unsigned_short__base__first may_be_replaced_by -2147483648.
|
|
create_nxdom_rules(54): dns_types__unsigned_short__base__last may_be_replaced_by 2147483647.
|
|
create_nxdom_rules(55): dns_types__opcode_type__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(56): dns_types__opcode_type__size may_be_replaced_by 4.
|
|
create_nxdom_rules(57): dns_types__opcode_type__first may_be_replaced_by dns_types__query.
|
|
create_nxdom_rules(58): dns_types__opcode_type__last may_be_replaced_by dns_types__status.
|
|
create_nxdom_rules(59): dns_types__opcode_type__base__first may_be_replaced_by dns_types__query.
|
|
create_nxdom_rules(60): dns_types__opcode_type__base__last may_be_replaced_by dns_types__status.
|
|
create_nxdom_rules(61): dns_types__opcode_type__pos(
|
|
dns_types__opcode_type__first) may_be_replaced_by 0.
|
|
create_nxdom_rules(62): dns_types__opcode_type__pos(
|
|
dns_types__query) may_be_replaced_by 0.
|
|
create_nxdom_rules(63): dns_types__opcode_type__val(0) may_be_replaced_by
|
|
dns_types__query.
|
|
create_nxdom_rules(64): dns_types__opcode_type__pos(
|
|
dns_types__iquery) may_be_replaced_by 1.
|
|
create_nxdom_rules(65): dns_types__opcode_type__val(1) may_be_replaced_by
|
|
dns_types__iquery.
|
|
create_nxdom_rules(66): dns_types__opcode_type__pos(
|
|
dns_types__status) may_be_replaced_by 2.
|
|
create_nxdom_rules(67): dns_types__opcode_type__val(2) may_be_replaced_by
|
|
dns_types__status.
|
|
create_nxdom_rules(68): dns_types__opcode_type__pos(
|
|
dns_types__opcode_type__last) may_be_replaced_by 2.
|
|
create_nxdom_rules(69): dns_types__opcode_type__pos(succ(X)) may_be_replaced_by
|
|
dns_types__opcode_type__pos(X) + 1
|
|
if [X <=dns_types__status, X <> dns_types__status].
|
|
create_nxdom_rules(70): dns_types__opcode_type__pos(pred(X)) may_be_replaced_by
|
|
dns_types__opcode_type__pos(X) - 1
|
|
if [X >=dns_types__query, X <> dns_types__query].
|
|
create_nxdom_rules(71): dns_types__opcode_type__pos(X) >= 0 may_be_deduced_from
|
|
[dns_types__query <= X, X <= dns_types__status].
|
|
create_nxdom_rules(72): dns_types__opcode_type__pos(X) <= 2 may_be_deduced_from
|
|
[dns_types__query <= X, X <= dns_types__status].
|
|
create_nxdom_rules(73): dns_types__opcode_type__val(X) >=
|
|
dns_types__query may_be_deduced_from
|
|
[0 <= X, X <= 2].
|
|
create_nxdom_rules(74): dns_types__opcode_type__val(X) <=
|
|
dns_types__status may_be_deduced_from
|
|
[0 <= X, X <= 2].
|
|
create_nxdom_rules(75): succ(dns_types__opcode_type__val(X)) may_be_replaced_by
|
|
dns_types__opcode_type__val(X+1)
|
|
if [0 <= X, X < 2].
|
|
create_nxdom_rules(76): pred(dns_types__opcode_type__val(X)) may_be_replaced_by
|
|
dns_types__opcode_type__val(X-1)
|
|
if [0 < X, X <= 2].
|
|
create_nxdom_rules(77): dns_types__opcode_type__pos(
|
|
dns_types__opcode_type__val(X)) may_be_replaced_by X
|
|
if [0 <= X, X <= 2].
|
|
create_nxdom_rules(78): dns_types__opcode_type__val(
|
|
dns_types__opcode_type__pos(X)) may_be_replaced_by X
|
|
if [dns_types__query <= X, X <= dns_types__status].
|
|
create_nxdom_rules(79): dns_types__opcode_type__pos(X) <=
|
|
dns_types__opcode_type__pos(Y) & X <= Y are_interchangeable
|
|
if [dns_types__query <= X, X <= dns_types__status,
|
|
dns_types__query <= Y, Y <= dns_types__status].
|
|
create_nxdom_rules(80): dns_types__opcode_type__val(X) <=
|
|
dns_types__opcode_type__val(Y) & X <= Y are_interchangeable
|
|
if [0 <= X, X <= 2, 0 <= Y, Y <= 2].
|
|
create_nxdom_rules(81): dns_types__response_code__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(82): dns_types__response_code__size may_be_replaced_by 4.
|
|
create_nxdom_rules(83): dns_types__response_code__first may_be_replaced_by dns_types__no_error.
|
|
create_nxdom_rules(84): dns_types__response_code__last may_be_replaced_by dns_types__refused.
|
|
create_nxdom_rules(85): dns_types__response_code__base__first may_be_replaced_by dns_types__no_error.
|
|
create_nxdom_rules(86): dns_types__response_code__base__last may_be_replaced_by dns_types__refused.
|
|
create_nxdom_rules(87): dns_types__response_code__pos(
|
|
dns_types__response_code__first) may_be_replaced_by 0.
|
|
create_nxdom_rules(88): dns_types__response_code__pos(
|
|
dns_types__no_error) may_be_replaced_by 0.
|
|
create_nxdom_rules(89): dns_types__response_code__val(0) may_be_replaced_by
|
|
dns_types__no_error.
|
|
create_nxdom_rules(90): dns_types__response_code__pos(
|
|
dns_types__format_error) may_be_replaced_by 1.
|
|
create_nxdom_rules(91): dns_types__response_code__val(1) may_be_replaced_by
|
|
dns_types__format_error.
|
|
create_nxdom_rules(92): dns_types__response_code__pos(
|
|
dns_types__server_failure) may_be_replaced_by 2.
|
|
create_nxdom_rules(93): dns_types__response_code__val(2) may_be_replaced_by
|
|
dns_types__server_failure.
|
|
create_nxdom_rules(94): dns_types__response_code__pos(
|
|
dns_types__name_error) may_be_replaced_by 3.
|
|
create_nxdom_rules(95): dns_types__response_code__val(3) may_be_replaced_by
|
|
dns_types__name_error.
|
|
create_nxdom_rules(96): dns_types__response_code__pos(
|
|
dns_types__not_implemented) may_be_replaced_by 4.
|
|
create_nxdom_rules(97): dns_types__response_code__val(4) may_be_replaced_by
|
|
dns_types__not_implemented.
|
|
create_nxdom_rules(98): dns_types__response_code__pos(
|
|
dns_types__refused) may_be_replaced_by 5.
|
|
create_nxdom_rules(99): dns_types__response_code__val(5) may_be_replaced_by
|
|
dns_types__refused.
|
|
create_nxdom_rules(100): dns_types__response_code__pos(
|
|
dns_types__response_code__last) may_be_replaced_by 5.
|
|
create_nxdom_rules(101): dns_types__response_code__pos(succ(X)) may_be_replaced_by
|
|
dns_types__response_code__pos(X) + 1
|
|
if [X <=dns_types__refused, X <> dns_types__refused].
|
|
create_nxdom_rules(102): dns_types__response_code__pos(pred(X)) may_be_replaced_by
|
|
dns_types__response_code__pos(X) - 1
|
|
if [X >=dns_types__no_error, X <> dns_types__no_error].
|
|
create_nxdom_rules(103): dns_types__response_code__pos(X) >= 0 may_be_deduced_from
|
|
[dns_types__no_error <= X, X <= dns_types__refused].
|
|
create_nxdom_rules(104): dns_types__response_code__pos(X) <= 5 may_be_deduced_from
|
|
[dns_types__no_error <= X, X <= dns_types__refused].
|
|
create_nxdom_rules(105): dns_types__response_code__val(X) >=
|
|
dns_types__no_error may_be_deduced_from
|
|
[0 <= X, X <= 5].
|
|
create_nxdom_rules(106): dns_types__response_code__val(X) <=
|
|
dns_types__refused may_be_deduced_from
|
|
[0 <= X, X <= 5].
|
|
create_nxdom_rules(107): succ(dns_types__response_code__val(X)) may_be_replaced_by
|
|
dns_types__response_code__val(X+1)
|
|
if [0 <= X, X < 5].
|
|
create_nxdom_rules(108): pred(dns_types__response_code__val(X)) may_be_replaced_by
|
|
dns_types__response_code__val(X-1)
|
|
if [0 < X, X <= 5].
|
|
create_nxdom_rules(109): dns_types__response_code__pos(
|
|
dns_types__response_code__val(X)) may_be_replaced_by X
|
|
if [0 <= X, X <= 5].
|
|
create_nxdom_rules(110): dns_types__response_code__val(
|
|
dns_types__response_code__pos(X)) may_be_replaced_by X
|
|
if [dns_types__no_error <= X, X <= dns_types__refused].
|
|
create_nxdom_rules(111): dns_types__response_code__pos(X) <=
|
|
dns_types__response_code__pos(Y) & X <= Y are_interchangeable
|
|
if [dns_types__no_error <= X, X <= dns_types__refused,
|
|
dns_types__no_error <= Y, Y <= dns_types__refused].
|
|
create_nxdom_rules(112): dns_types__response_code__val(X) <=
|
|
dns_types__response_code__val(Y) & X <= Y are_interchangeable
|
|
if [0 <= X, X <= 5, 0 <= Y, Y <= 5].
|
|
create_nxdom_rules(113): dns_types__header_type__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(114): dns_types__header_type__size may_be_replaced_by 96.
|
|
create_nxdom_rules(115): A = B may_be_deduced_from
|
|
[goal(checktype(A,dns_types__header_type)),
|
|
goal(checktype(B,dns_types__header_type)),
|
|
fld_messageid(A) = fld_messageid(B),
|
|
fld_qr(A) = fld_qr(B),
|
|
fld_opcode(A) = fld_opcode(B),
|
|
fld_aa(A) = fld_aa(B),
|
|
fld_tc(A) = fld_tc(B),
|
|
fld_rd(A) = fld_rd(B),
|
|
fld_ra(A) = fld_ra(B),
|
|
fld_res1(A) = fld_res1(B),
|
|
fld_res2(A) = fld_res2(B),
|
|
fld_res3(A) = fld_res3(B),
|
|
fld_rcode(A) = fld_rcode(B),
|
|
fld_qdcount(A) = fld_qdcount(B),
|
|
fld_ancount(A) = fld_ancount(B),
|
|
fld_nscount(A) = fld_nscount(B),
|
|
fld_arcount(A) = fld_arcount(B)].
|
|
create_nxdom_rules(116): dns_types__dns_packet__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(117): A = B may_be_deduced_from
|
|
[goal(checktype(A,dns_types__dns_packet)),
|
|
goal(checktype(B,dns_types__dns_packet)),
|
|
fld_header(A) = fld_header(B),
|
|
fld_bytes(A) = fld_bytes(B)].
|
|
create_nxdom_rules(118): rr_type__wirestringtypeindex__size >= 0 may_be_deduced.
|
|
create_nxdom_rules(119): rr_type__wirestringtypeindex__first may_be_replaced_by 1.
|
|
create_nxdom_rules(120): rr_type__wirestringtypeindex__last may_be_replaced_by 129.
|
|
create_nxdom_rules(121): rr_type__wirestringtypeindex__base__first may_be_replaced_by -2147483648.
|
|
create_nxdom_rules(122): rr_type__wirestringtypeindex__base__last may_be_replaced_by 2147483647.
|