rtyler
/
ironsides
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
ironsides/process_dns_request/set_ttl_data_ptr_response.slg

1197 lines
61 KiB
Plaintext
Raw Permalink Blame History

*****************************************************************************
Semantic Analysis of SPARK Text
Examiner GPL Edition
*****************************************************************************
SPARK Simplifier GPL 2011
Copyright (C) 2011 Altran Praxis Limited, Bath, U.K.
procedure Process_Dns_Request.Set_TTL_Data_PTR_Response
@@@@@@@@@@ VC: procedure_set_ttl_data_ptr_response_1. @@@@@@@@@@
%%% Simplified H4 on reading formula in, to give:
%%% H4: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
i___1]) <= dns_types__byte__last)
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
character__first <= element(fld_domainname(ptr_record), [i___1]) and
element(fld_domainname(ptr_record), [i___1]) <= character__last)
%%% Simplified H8 on reading formula in, to give:
%%% H8: rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
--- Hypothesis H13 has been replaced by "true". (It is already present, as H2)
.
*** Proved C1: fld_ttlinseconds(fld_inherit(ptr_record)) >=
unsigned_types__unsigned32__first
using hypothesis H10.
*** Proved C2: fld_ttlinseconds(fld_inherit(ptr_record)) <=
unsigned_types__unsigned32__last
using hypothesis H11.
*** Proved C3: start_byte >= dns_types__packet_bytes_range__first
using hypothesis H5.
*** Proved C4: start_byte <= dns_types__packet_bytes_range__last
using hypothesis H6.
-S- Applied substitution rule set_ttl_data_rules(7).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
ptr_record), [i___1]) <= character__last)
-S- Applied substitution rule set_ttl_data_rules(8).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
ptr_record), [i___1]) <= 255)
-S- Applied substitution rule set_ttl_data_rules(17).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__first by:
1.
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
dns_types__packet_bytes_range__last -> dns_types__byte__first <=
element(bytes, [i___1]) and element(bytes, [i___1]) <=
dns_types__byte__last)
<S> New H5: start_byte >= 1
-S- Applied substitution rule set_ttl_data_rules(18).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__last by:
8180.
<S> New H3: start_byte <= 8174 - current_name_length
<S> New H6: start_byte <= 8180
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 ->
dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
i___1]) <= dns_types__byte__last)
<S> New C5: start_byte <= 8177
-S- Applied substitution rule set_ttl_data_rules(23).
This was achieved by replacing all occurrences of dns_types__byte__first
by:
0.
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes, [i___1]) and element(bytes, [i___1]) <=
dns_types__byte__last)
-S- Applied substitution rule set_ttl_data_rules(24).
This was achieved by replacing all occurrences of dns_types__byte__last by:
255.
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
-S- Applied substitution rule set_ttl_data_rules(35).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New H10: fld_ttlinseconds(fld_inherit(ptr_record)) >= 0
-S- Applied substitution rule set_ttl_data_rules(36).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__last by:
4294967295.
<S> New H11: fld_ttlinseconds(fld_inherit(ptr_record)) <= 4294967295
-S- Applied substitution rule set_ttl_data_rules(41).
This was achieved by replacing all occurrences of
rr_type__classtype__first by:
rr_type__internet.
<S> New H8: rr_type__internet <= fld_class(fld_inherit(ptr_record))
-S- Applied substitution rule set_ttl_data_rules(42).
This was achieved by replacing all occurrences of rr_type__classtype__last
by:
rr_type__hs.
<S> New H9: fld_class(fld_inherit(ptr_record)) <= rr_type__hs
-S- Applied substitution rule set_ttl_data_rules(68).
This was achieved by replacing all occurrences of
rr_type__wirestringtypeindex__first by:
1.
<S> New H12: current_name_length >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
rr_type__wirestringtypeindex__last -> 0 <= element(fld_domainname(
ptr_record), [i___1]) and element(fld_domainname(ptr_record), [i___1])
<= 255)
-S- Applied substitution rule set_ttl_data_rules(69).
This was achieved by replacing all occurrences of
rr_type__wirestringtypeindex__last by:
129.
<S> New H2: current_name_length <= 129
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <=
element(fld_domainname(ptr_record), [i___1]) and element(
fld_domainname(ptr_record), [i___1]) <= 255)
--- Eliminated hypothesis H13 (true-hypothesis).
--- Eliminated hypothesis H1 (redundant, given H12).
--- Eliminated hypothesis H6 (redundant, given H3 & H12).
+++ New H14: integer__size >= 0
+++ New H15: character__size >= 0
+++ New H16: positive__size >= 0
+++ New H17: dns_types__packet_bytes_range__size >= 0
+++ New H18: unsigned_types__unsigned16__size >= 0
+++ New H19: unsigned_types__unsigned32__size >= 0
+++ New H20: rr_type__classtype__size >= 0
+++ New H21: rr_type__wirestringtypeindex__size >= 0
+++ New H22: rr_type__resourcerecordtype__size >= 0
+++ New H23: rr_type__ptr_record_type__ptrrecordtype__size >= 0
@@@@@@@@@@ VC: procedure_set_ttl_data_ptr_response_2. @@@@@@@@@@
%%% Simplified H4 on reading formula in, to give:
%%% H4: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
i___1]) <= dns_types__byte__last)
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
character__first <= element(fld_domainname(ptr_record), [i___1]) and
element(fld_domainname(ptr_record), [i___1]) <= character__last)
%%% Simplified H8 on reading formula in, to give:
%%% H8: rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
--- Hypothesis H13 has been replaced by "true". (It is already present, as H2)
.
--- Hypothesis H14 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H15 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as H5)
.
--- Hypothesis H17 has been replaced by "true". (It is already present, as H6)
.
%%% Simplified H19 on reading formula in, to give:
%%% H19: for_all(i___1 : integer, dns_types__packet_bytes_range__first
<= i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes__1, [i___1]) and element(
bytes__1, [i___1]) <= dns_types__byte__last)
*** Proved C3: start_byte + 4 >= dns_types__packet_bytes_range__first
using hypothesis H5.
-S- Applied substitution rule set_ttl_data_rules(29).
This was achieved by replacing all occurrences of
unsigned_types__unsigned16__first by:
0.
<S> New C1: current_name_length >= 0
<S> New C6: current_name_length >= 0
-S- Applied substitution rule set_ttl_data_rules(30).
This was achieved by replacing all occurrences of
unsigned_types__unsigned16__last by:
65535.
<S> New C2: current_name_length <= 65535
<S> New C7: current_name_length <= 65535
-S- Applied substitution rule set_ttl_data_rules(18).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__last by:
8180.
<S> New H3: start_byte <= 8174 - current_name_length
<S> New H4: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= 8180 -> dns_types__byte__first <= element(bytes, [
i___1]) and element(bytes, [i___1]) <= dns_types__byte__last)
<S> New H6: start_byte <= 8180
<S> New H18: start_byte <= 8177
<S> New H19: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= 8180 -> dns_types__byte__first <= element(
bytes__1, [i___1]) and element(bytes__1, [i___1]) <=
dns_types__byte__last)
<S> New C4: start_byte <= 8176
<S> New C5: start_byte <= 8175
-S- Applied substitution rule set_ttl_data_rules(19).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__base__first by:
- 2147483648.
<S> New C8: start_byte >= - 2147483652
-S- Applied substitution rule set_ttl_data_rules(20).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__base__last by:
2147483647.
<S> New C9: start_byte <= 2147483643
*** Proved C1: current_name_length >= 0
using hypothesis H1.
*** Proved C6: current_name_length >= 0
using hypothesis H1.
*** Proved C9: start_byte <= 2147483643
using hypothesis H6.
-S- Applied substitution rule set_ttl_data_rules(7).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
ptr_record), [i___1]) <= character__last)
-S- Applied substitution rule set_ttl_data_rules(8).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
ptr_record), [i___1]) <= 255)
-S- Applied substitution rule set_ttl_data_rules(17).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__first by:
1.
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 ->
dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
i___1]) <= dns_types__byte__last)
<S> New H5: start_byte >= 1
<S> New H19: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 ->
dns_types__byte__first <= element(bytes__1, [i___1]) and element(
bytes__1, [i___1]) <= dns_types__byte__last)
-S- Applied substitution rule set_ttl_data_rules(23).
This was achieved by replacing all occurrences of dns_types__byte__first
by:
0.
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes, [i___1]) and element(bytes, [i___1]) <=
dns_types__byte__last)
<S> New H19: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <=
dns_types__byte__last)
-S- Applied substitution rule set_ttl_data_rules(24).
This was achieved by replacing all occurrences of dns_types__byte__last by:
255.
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
<S> New H19: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 255)
-S- Applied substitution rule set_ttl_data_rules(35).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New H10: fld_ttlinseconds(fld_inherit(ptr_record)) >= 0
-S- Applied substitution rule set_ttl_data_rules(36).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__last by:
4294967295.
<S> New H11: fld_ttlinseconds(fld_inherit(ptr_record)) <= 4294967295
-S- Applied substitution rule set_ttl_data_rules(41).
This was achieved by replacing all occurrences of
rr_type__classtype__first by:
rr_type__internet.
<S> New H8: rr_type__internet <= fld_class(fld_inherit(ptr_record))
-S- Applied substitution rule set_ttl_data_rules(42).
This was achieved by replacing all occurrences of rr_type__classtype__last
by:
rr_type__hs.
<S> New H9: fld_class(fld_inherit(ptr_record)) <= rr_type__hs
-S- Applied substitution rule set_ttl_data_rules(68).
This was achieved by replacing all occurrences of
rr_type__wirestringtypeindex__first by:
1.
<S> New H12: current_name_length >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
rr_type__wirestringtypeindex__last -> 0 <= element(fld_domainname(
ptr_record), [i___1]) and element(fld_domainname(ptr_record), [i___1])
<= 255)
-S- Applied substitution rule set_ttl_data_rules(69).
This was achieved by replacing all occurrences of
rr_type__wirestringtypeindex__last by:
129.
<S> New H2: current_name_length <= 129
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <=
element(fld_domainname(ptr_record), [i___1]) and element(
fld_domainname(ptr_record), [i___1]) <= 255)
*** Proved C2: current_name_length <= 65535
using hypothesis H2.
*** Proved C7: current_name_length <= 65535
using hypothesis H2.
*** Proved C8: start_byte >= - 2147483652
using hypothesis H5.
--- Eliminated hypothesis H13 (true-hypothesis).
--- Eliminated hypothesis H14 (true-hypothesis).
--- Eliminated hypothesis H15 (true-hypothesis).
--- Eliminated hypothesis H16 (true-hypothesis).
--- Eliminated hypothesis H17 (true-hypothesis).
--- Eliminated hypothesis H1 (redundant, given H12).
--- Eliminated hypothesis H6 (redundant, given H18).
--- Eliminated hypothesis H18 (redundant, given H3 & H12).
+++ New H20: integer__size >= 0
+++ New H21: character__size >= 0
+++ New H22: positive__size >= 0
+++ New H23: dns_types__packet_bytes_range__size >= 0
+++ New H24: unsigned_types__unsigned16__size >= 0
+++ New H25: unsigned_types__unsigned32__size >= 0
+++ New H26: rr_type__classtype__size >= 0
+++ New H27: rr_type__wirestringtypeindex__size >= 0
+++ New H28: rr_type__resourcerecordtype__size >= 0
+++ New H29: rr_type__ptr_record_type__ptrrecordtype__size >= 0
@@@@@@@@@@ VC: procedure_set_ttl_data_ptr_response_3. @@@@@@@@@@
%%% Simplified H4 on reading formula in, to give:
%%% H4: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
i___1]) <= dns_types__byte__last)
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
character__first <= element(fld_domainname(ptr_record), [i___1]) and
element(fld_domainname(ptr_record), [i___1]) <= character__last)
%%% Simplified H8 on reading formula in, to give:
%%% H8: rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
--- Hypothesis H13 has been replaced by "true". (It is already present, as H2)
.
--- Hypothesis H14 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H15 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as H5)
.
--- Hypothesis H17 has been replaced by "true". (It is already present, as H6)
.
%%% Simplified H19 on reading formula in, to give:
%%% H19: for_all(i___1 : integer, dns_types__packet_bytes_range__first
<= i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes__1, [i___1]) and element(
bytes__1, [i___1]) <= dns_types__byte__last)
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H20).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H21).
%%% Simplified H29 on reading formula in, to give:
%%% H29: for_all(i___1 : integer, dns_types__packet_bytes_range__first
<= i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes__2, [i___1]) and element(
bytes__2, [i___1]) <= dns_types__byte__last)
-S- Applied substitution rule set_ttl_data_rules(2).
This was achieved by replacing all occurrences of integer__first by:
- 2147483648.
<S> New C1: current_name_length >= - 2147483648
<S> New C3: true
-S- Applied substitution rule set_ttl_data_rules(3).
This was achieved by replacing all occurrences of integer__last by:
2147483647.
<S> New C2: current_name_length <= 2147483647
<S> New C4: true
*** Proved C1: current_name_length >= - 2147483648
using hypothesis H1.
*** Proved C3: true
*** Proved C4: true
-S- Applied substitution rule set_ttl_data_rules(7).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
ptr_record), [i___1]) <= character__last)
-S- Applied substitution rule set_ttl_data_rules(8).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
ptr_record), [i___1]) <= 255)
-S- Applied substitution rule set_ttl_data_rules(17).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__first by:
1.
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
dns_types__packet_bytes_range__last -> dns_types__byte__first <=
element(bytes, [i___1]) and element(bytes, [i___1]) <=
dns_types__byte__last)
<S> New H5: start_byte >= 1
<S> New H19: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
dns_types__packet_bytes_range__last -> dns_types__byte__first <=
element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <=
dns_types__byte__last)
<S> New H22: start_byte >= - 3
<S> New H29: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
dns_types__packet_bytes_range__last -> dns_types__byte__first <=
element(bytes__2, [i___1]) and element(bytes__2, [i___1]) <=
dns_types__byte__last)
-S- Applied substitution rule set_ttl_data_rules(18).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__last by:
8180.
<S> New H3: start_byte <= 8174 - current_name_length
<S> New H6: start_byte <= 8180
<S> New H18: start_byte <= 8177
<S> New H23: start_byte <= 8176
<S> New H24: start_byte <= 8175
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 ->
dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
i___1]) <= dns_types__byte__last)
<S> New H19: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 ->
dns_types__byte__first <= element(bytes__1, [i___1]) and element(
bytes__1, [i___1]) <= dns_types__byte__last)
<S> New H29: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 ->
dns_types__byte__first <= element(bytes__2, [i___1]) and element(
bytes__2, [i___1]) <= dns_types__byte__last)
-S- Applied substitution rule set_ttl_data_rules(19).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__base__first by:
- 2147483648.
<S> New H27: start_byte >= - 2147483652
-S- Applied substitution rule set_ttl_data_rules(20).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__base__last by:
2147483647.
<S> New H28: start_byte <= 2147483643
-S- Applied substitution rule set_ttl_data_rules(23).
This was achieved by replacing all occurrences of dns_types__byte__first
by:
0.
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes, [i___1]) and element(bytes, [i___1]) <=
dns_types__byte__last)
<S> New H19: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <=
dns_types__byte__last)
<S> New H29: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes__2, [i___1]) and element(bytes__2, [i___1]) <=
dns_types__byte__last)
-S- Applied substitution rule set_ttl_data_rules(24).
This was achieved by replacing all occurrences of dns_types__byte__last by:
255.
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
<S> New H19: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 255)
<S> New H29: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes__2, [i___1]) and element(bytes__2, [i___1]) <= 255)
-S- Applied substitution rule set_ttl_data_rules(29).
This was achieved by replacing all occurrences of
unsigned_types__unsigned16__first by:
0.
<S> New H20: current_name_length >= 0
-S- Applied substitution rule set_ttl_data_rules(30).
This was achieved by replacing all occurrences of
unsigned_types__unsigned16__last by:
65535.
<S> New H21: current_name_length <= 65535
-S- Applied substitution rule set_ttl_data_rules(35).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New H10: fld_ttlinseconds(fld_inherit(ptr_record)) >= 0
-S- Applied substitution rule set_ttl_data_rules(36).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__last by:
4294967295.
<S> New H11: fld_ttlinseconds(fld_inherit(ptr_record)) <= 4294967295
-S- Applied substitution rule set_ttl_data_rules(41).
This was achieved by replacing all occurrences of
rr_type__classtype__first by:
rr_type__internet.
<S> New H8: rr_type__internet <= fld_class(fld_inherit(ptr_record))
-S- Applied substitution rule set_ttl_data_rules(42).
This was achieved by replacing all occurrences of rr_type__classtype__last
by:
rr_type__hs.
<S> New H9: fld_class(fld_inherit(ptr_record)) <= rr_type__hs
-S- Applied substitution rule set_ttl_data_rules(68).
This was achieved by replacing all occurrences of
rr_type__wirestringtypeindex__first by:
1.
<S> New H12: current_name_length >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
rr_type__wirestringtypeindex__last -> 0 <= element(fld_domainname(
ptr_record), [i___1]) and element(fld_domainname(ptr_record), [i___1])
<= 255)
-S- Applied substitution rule set_ttl_data_rules(69).
This was achieved by replacing all occurrences of
rr_type__wirestringtypeindex__last by:
129.
<S> New H2: current_name_length <= 129
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <=
element(fld_domainname(ptr_record), [i___1]) and element(
fld_domainname(ptr_record), [i___1]) <= 255)
*** Proved C2: current_name_length <= 2147483647
using hypothesis H21.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_set_ttl_data_ptr_response_4. @@@@@@@@@@
%%% Simplified H4 on reading formula in, to give:
%%% H4: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
i___1]) <= dns_types__byte__last)
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
character__first <= element(fld_domainname(ptr_record), [i___1]) and
element(fld_domainname(ptr_record), [i___1]) <= character__last)
%%% Simplified H8 on reading formula in, to give:
%%% H8: rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
--- Hypothesis H13 has been replaced by "true". (It is already present, as H2)
.
--- Hypothesis H14 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H15 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as H5)
.
--- Hypothesis H17 has been replaced by "true". (It is already present, as H6)
.
%%% Simplified H19 on reading formula in, to give:
%%% H19: for_all(i___1 : integer, dns_types__packet_bytes_range__first
<= i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes__1, [i___1]) and element(
bytes__1, [i___1]) <= dns_types__byte__last)
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H20).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H21).
%%% Simplified H29 on reading formula in, to give:
%%% H29: for_all(i___1 : integer, dns_types__packet_bytes_range__first
<= i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes__2, [i___1]) and element(
bytes__2, [i___1]) <= dns_types__byte__last)
*** Proved C1: 1 <= current_name_length -> current_name_length >=
rr_type__wirestringtypeindex__first and current_name_length <=
rr_type__wirestringtypeindex__last
using hypotheses H2 & H12.
-S- Applied substitution rule set_ttl_data_rules(2).
This was achieved by replacing all occurrences of integer__first by:
- 2147483648.
<S> New H30: current_name_length >= - 2147483648
<S> New H32: true
-S- Applied substitution rule set_ttl_data_rules(3).
This was achieved by replacing all occurrences of integer__last by:
2147483647.
<S> New H31: current_name_length <= 2147483647
<S> New H33: true
-S- Applied substitution rule set_ttl_data_rules(7).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
ptr_record), [i___1]) <= character__last)
-S- Applied substitution rule set_ttl_data_rules(8).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
ptr_record), [i___1]) <= 255)
-S- Applied substitution rule set_ttl_data_rules(17).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__first by:
1.
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
dns_types__packet_bytes_range__last -> dns_types__byte__first <=
element(bytes, [i___1]) and element(bytes, [i___1]) <=
dns_types__byte__last)
<S> New H5: start_byte >= 1
<S> New H19: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
dns_types__packet_bytes_range__last -> dns_types__byte__first <=
element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <=
dns_types__byte__last)
<S> New H22: start_byte >= - 3
<S> New H29: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
dns_types__packet_bytes_range__last -> dns_types__byte__first <=
element(bytes__2, [i___1]) and element(bytes__2, [i___1]) <=
dns_types__byte__last)
-S- Applied substitution rule set_ttl_data_rules(18).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__last by:
8180.
<S> New H3: start_byte <= 8174 - current_name_length
<S> New H6: start_byte <= 8180
<S> New H18: start_byte <= 8177
<S> New H23: start_byte <= 8176
<S> New H24: start_byte <= 8175
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 ->
dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
i___1]) <= dns_types__byte__last)
<S> New H19: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 ->
dns_types__byte__first <= element(bytes__1, [i___1]) and element(
bytes__1, [i___1]) <= dns_types__byte__last)
<S> New H29: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 ->
dns_types__byte__first <= element(bytes__2, [i___1]) and element(
bytes__2, [i___1]) <= dns_types__byte__last)
-S- Applied substitution rule set_ttl_data_rules(19).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__base__first by:
- 2147483648.
<S> New H27: start_byte >= - 2147483652
-S- Applied substitution rule set_ttl_data_rules(20).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__base__last by:
2147483647.
<S> New H28: start_byte <= 2147483643
-S- Applied substitution rule set_ttl_data_rules(23).
This was achieved by replacing all occurrences of dns_types__byte__first
by:
0.
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes, [i___1]) and element(bytes, [i___1]) <=
dns_types__byte__last)
<S> New H19: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <=
dns_types__byte__last)
<S> New H29: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes__2, [i___1]) and element(bytes__2, [i___1]) <=
dns_types__byte__last)
-S- Applied substitution rule set_ttl_data_rules(24).
This was achieved by replacing all occurrences of dns_types__byte__last by:
255.
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
<S> New H19: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 255)
<S> New H29: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes__2, [i___1]) and element(bytes__2, [i___1]) <= 255)
-S- Applied substitution rule set_ttl_data_rules(29).
This was achieved by replacing all occurrences of
unsigned_types__unsigned16__first by:
0.
<S> New H20: current_name_length >= 0
-S- Applied substitution rule set_ttl_data_rules(30).
This was achieved by replacing all occurrences of
unsigned_types__unsigned16__last by:
65535.
<S> New H21: current_name_length <= 65535
-S- Applied substitution rule set_ttl_data_rules(35).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New H10: fld_ttlinseconds(fld_inherit(ptr_record)) >= 0
-S- Applied substitution rule set_ttl_data_rules(36).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__last by:
4294967295.
<S> New H11: fld_ttlinseconds(fld_inherit(ptr_record)) <= 4294967295
-S- Applied substitution rule set_ttl_data_rules(41).
This was achieved by replacing all occurrences of
rr_type__classtype__first by:
rr_type__internet.
<S> New H8: rr_type__internet <= fld_class(fld_inherit(ptr_record))
-S- Applied substitution rule set_ttl_data_rules(42).
This was achieved by replacing all occurrences of rr_type__classtype__last
by:
rr_type__hs.
<S> New H9: fld_class(fld_inherit(ptr_record)) <= rr_type__hs
-S- Applied substitution rule set_ttl_data_rules(68).
This was achieved by replacing all occurrences of
rr_type__wirestringtypeindex__first by:
1.
<S> New H12: current_name_length >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
rr_type__wirestringtypeindex__last -> 0 <= element(fld_domainname(
ptr_record), [i___1]) and element(fld_domainname(ptr_record), [i___1])
<= 255)
<S> New C2: 1 <= current_name_length -> 1 <=
rr_type__wirestringtypeindex__last
-S- Applied substitution rule set_ttl_data_rules(69).
This was achieved by replacing all occurrences of
rr_type__wirestringtypeindex__last by:
129.
<S> New H2: current_name_length <= 129
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <=
element(fld_domainname(ptr_record), [i___1]) and element(
fld_domainname(ptr_record), [i___1]) <= 255)
<S> New C2: true
*** Proved C2: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_set_ttl_data_ptr_response_5. @@@@@@@@@@
%%% Simplified H4 on reading formula in, to give:
%%% H4: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
i___1]) <= dns_types__byte__last)
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
character__first <= element(fld_domainname(ptr_record), [i___1]) and
element(fld_domainname(ptr_record), [i___1]) <= character__last)
%%% Simplified H8 on reading formula in, to give:
%%% H8: rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
--- Hypothesis H13 has been replaced by "true". (It is already present, as H2)
.
--- Hypothesis H14 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H15 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as H5)
.
--- Hypothesis H17 has been replaced by "true". (It is already present, as H6)
.
%%% Simplified H19 on reading formula in, to give:
%%% H19: for_all(i___1 : integer, dns_types__packet_bytes_range__first
<= i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes__1, [i___1]) and element(
bytes__1, [i___1]) <= dns_types__byte__last)
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H20).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H21).
%%% Simplified H29 on reading formula in, to give:
%%% H29: for_all(i___1 : integer, dns_types__packet_bytes_range__first
<= i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes__2, [i___1]) and element(
bytes__2, [i___1]) <= dns_types__byte__last)
%%% Simplified C4 on reading formula in, to give:
%%% C4: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes__2, [i___1]) and element(
bytes__2, [i___1]) <= dns_types__byte__last)
%%% Simplified C7 on reading formula in, to give:
%%% C7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
character__first <= element(fld_domainname(ptr_record), [i___1]) and
element(fld_domainname(ptr_record), [i___1]) <= character__last)
%%% Simplified C8 on reading formula in, to give:
%%% C8: rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
%%% Simplified C19 on reading formula in, to give:
%%% C19: true
*** Proved C1: start_byte <= dns_types__packet_bytes_range__last - 6 -
current_name_length
using hypothesis H3.
*** Proved C3: 1 <= rr_type__wirestringtypeindex__last
using hypotheses H2 & H36.
*** Proved C4: for_all(i___1 : integer, dns_types__packet_bytes_range__first
<= i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes__2, [i___1]) and element(
bytes__2, [i___1]) <= dns_types__byte__last)
using hypothesis H29.
*** Proved C5: start_byte >= dns_types__packet_bytes_range__first
using hypothesis H5.
*** Proved C6: start_byte <= dns_types__packet_bytes_range__last
using hypothesis H6.
*** Proved C7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first
<= i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
character__first <= element(fld_domainname(ptr_record), [i___1]) and
element(fld_domainname(ptr_record), [i___1]) <= character__last)
using hypothesis H7.
*** Proved C8: rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
using hypothesis H8.
*** Proved C9: fld_class(fld_inherit(ptr_record)) <= rr_type__classtype__last
using hypothesis H9.
*** Proved C10: fld_ttlinseconds(fld_inherit(ptr_record)) >=
unsigned_types__unsigned32__first
using hypothesis H10.
*** Proved C11: fld_ttlinseconds(fld_inherit(ptr_record)) <=
unsigned_types__unsigned32__last
using hypothesis H11.
*** Proved C12: current_name_length >= rr_type__wirestringtypeindex__first
using hypothesis H12.
*** Proved C13: current_name_length <= rr_type__wirestringtypeindex__last
using hypothesis H2.
*** Proved C14: current_name_length >= 0
using hypothesis H1.
*** Proved C15: current_name_length <= rr_type__wirestringtypeindex__last
using hypothesis H2.
*** Proved C16: start_byte <= dns_types__packet_bytes_range__last - 6 -
current_name_length
using hypothesis H3.
*** Proved C18: 1 <= rr_type__wirestringtypeindex__last
using hypotheses H2 & H36.
*** Proved C19: true
*** Proved C20: 1 <= current_name_length
using hypothesis H36.
-S- Applied substitution rule set_ttl_data_rules(68).
This was achieved by replacing all occurrences of
rr_type__wirestringtypeindex__first by:
1.
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
rr_type__wirestringtypeindex__last -> character__first <= element(
fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
ptr_record), [i___1]) <= character__last)
<S> New H12: current_name_length >= 1
<S> New H34: 1 <= current_name_length -> current_name_length >= 1 and
current_name_length <= rr_type__wirestringtypeindex__last
<S> New H35: 1 <= current_name_length -> 1 <=
rr_type__wirestringtypeindex__last
<S> New C2: true
<S> New C17: true
*** Proved C2: true
*** Proved C17: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_set_ttl_data_ptr_response_6. @@@@@@@@@@
%%% Simplified H4 on reading formula in, to give:
%%% H4: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
i___1]) <= dns_types__byte__last)
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
character__first <= element(fld_domainname(ptr_record), [i___1]) and
element(fld_domainname(ptr_record), [i___1]) <= character__last)
%%% Simplified H8 on reading formula in, to give:
%%% H8: rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
--- Hypothesis H15 has been replaced by "true". (It is already present, as
H13).
--- Hypothesis H16 has been replaced by "true". (It is already present, as H1)
.
--- Hypothesis H17 has been replaced by "true". (It is already present, as H2)
.
--- Hypothesis H18 has been replaced by "true". (It is already present, as H3)
.
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H21).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H22).
--- Hypothesis H25 has been replaced by "true". (It is already present, as H2)
.
--- Hypothesis H26 has been replaced by "true". (It is already present, as H3)
.
%%% Simplified C4 on reading formula in, to give:
%%% C4: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(update(bytes, [start_byte + 5 +
loop__1__i], element(fld_domainname(ptr_record), [loop__1__i])), [
i___1]) and element(update(bytes, [start_byte + 5 + loop__1__i],
element(fld_domainname(ptr_record), [loop__1__i])), [i___1]) <=
dns_types__byte__last)
%%% Simplified C7 on reading formula in, to give:
%%% C7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
character__first <= element(fld_domainname(ptr_record), [i___1]) and
element(fld_domainname(ptr_record), [i___1]) <= character__last)
%%% Simplified C8 on reading formula in, to give:
%%% C8: rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
%%% Simplified C19 on reading formula in, to give:
%%% C19: loop__1__i >= 0
*** Proved C1: start_byte <= dns_types__packet_bytes_range__last - 6 -
current_name_length
using hypothesis H1.
*** Proved C2: loop__1__i + 1 >= rr_type__wirestringtypeindex__first
using hypothesis H2.
*** Proved C4: for_all(i___1 : integer, dns_types__packet_bytes_range__first
<= i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(update(bytes, [start_byte + 5 +
loop__1__i], element(fld_domainname(ptr_record), [loop__1__i])), [
i___1]) and element(update(bytes, [start_byte + 5 + loop__1__i],
element(fld_domainname(ptr_record), [loop__1__i])), [i___1]) <=
dns_types__byte__last)
using hypotheses H4, H21, H22, H27 & H28.
*** Proved C5: start_byte >= dns_types__packet_bytes_range__first
using hypothesis H5.
*** Proved C6: start_byte <= dns_types__packet_bytes_range__last
using hypothesis H6.
*** Proved C7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first
<= i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
character__first <= element(fld_domainname(ptr_record), [i___1]) and
element(fld_domainname(ptr_record), [i___1]) <= character__last)
using hypothesis H7.
*** Proved C8: rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
using hypothesis H8.
*** Proved C9: fld_class(fld_inherit(ptr_record)) <= rr_type__classtype__last
using hypothesis H9.
*** Proved C10: fld_ttlinseconds(fld_inherit(ptr_record)) >=
unsigned_types__unsigned32__first
using hypothesis H10.
*** Proved C11: fld_ttlinseconds(fld_inherit(ptr_record)) <=
unsigned_types__unsigned32__last
using hypothesis H11.
*** Proved C12: current_name_length >= rr_type__wirestringtypeindex__first
using hypothesis H12.
*** Proved C13: current_name_length <= rr_type__wirestringtypeindex__last
using hypothesis H13.
*** Proved C14: current_name_length >= 0
using hypothesis H14.
*** Proved C15: current_name_length <= rr_type__wirestringtypeindex__last
using hypothesis H13.
*** Proved C16: start_byte <= dns_types__packet_bytes_range__last - 6 -
current_name_length
using hypothesis H1.
*** Proved C17: loop__1__i + 1 >= rr_type__wirestringtypeindex__first
using hypothesis H2.
*** Proved C19: loop__1__i >= 0
using hypothesis H19.
-S- Applied substitution rule set_ttl_data_rules(69).
This was achieved by replacing all occurrences of
rr_type__wirestringtypeindex__last by:
129.
<S> New H3: loop__1__i <= 129
<S> New H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= 129 -> character__first <= element(fld_domainname(
ptr_record), [i___1]) and element(fld_domainname(ptr_record), [i___1])
<= character__last)
<S> New H13: current_name_length <= 129
<S> New C3: loop__1__i <= 128
<S> New C18: loop__1__i <= 128
*** Proved C3: loop__1__i <= 128
using hypotheses H13, H20 & H35.
*** Proved C18: loop__1__i <= 128
using hypotheses H13, H20 & H35.
>>> Restructured hypothesis H35 into:
>>> H35: loop__1__i <> current_name_length
-S- Applied substitution rule set_ttl_data_rules(7).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= 129 -> 0 <= element(fld_domainname(ptr_record), [
i___1]) and element(fld_domainname(ptr_record), [i___1]) <=
character__last)
-S- Applied substitution rule set_ttl_data_rules(8).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= 129 -> 0 <= element(fld_domainname(ptr_record), [
i___1]) and element(fld_domainname(ptr_record), [i___1]) <= 255)
-S- Applied substitution rule set_ttl_data_rules(17).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__first by:
1.
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
dns_types__packet_bytes_range__last -> dns_types__byte__first <=
element(bytes, [i___1]) and element(bytes, [i___1]) <=
dns_types__byte__last)
<S> New H5: start_byte >= 1
<S> New H27: start_byte + 5 + loop__1__i >= 1
<S> New H31: loop__1__i >= 1
-S- Applied substitution rule set_ttl_data_rules(18).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__last by:
8180.
<S> New H1: start_byte <= 8174 - current_name_length
<S> New H6: start_byte <= 8180
<S> New H28: start_byte + 5 + loop__1__i <= 8180
<S> New H32: loop__1__i <= 8180
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 ->
dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
i___1]) <= dns_types__byte__last)
-S- Applied substitution rule set_ttl_data_rules(19).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__base__first by:
- 2147483648.
<S> New H29: start_byte + 5 + loop__1__i >= - 2147483648
<S> New H33: start_byte >= - 2147483653
-S- Applied substitution rule set_ttl_data_rules(20).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__base__last by:
2147483647.
<S> New H30: start_byte + 5 + loop__1__i <= 2147483647
<S> New H34: start_byte <= 2147483642
-S- Applied substitution rule set_ttl_data_rules(23).
This was achieved by replacing all occurrences of dns_types__byte__first
by:
0.
<S> New H21: element(fld_domainname(ptr_record), [loop__1__i]) >= 0
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes, [i___1]) and element(bytes, [i___1]) <=
dns_types__byte__last)
-S- Applied substitution rule set_ttl_data_rules(24).
This was achieved by replacing all occurrences of dns_types__byte__last by:
255.
<S> New H22: element(fld_domainname(ptr_record), [loop__1__i]) <= 255
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
-S- Applied substitution rule set_ttl_data_rules(35).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New H10: fld_ttlinseconds(fld_inherit(ptr_record)) >= 0
-S- Applied substitution rule set_ttl_data_rules(36).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__last by:
4294967295.
<S> New H11: fld_ttlinseconds(fld_inherit(ptr_record)) <= 4294967295
-S- Applied substitution rule set_ttl_data_rules(41).
This was achieved by replacing all occurrences of
rr_type__classtype__first by:
rr_type__internet.
<S> New H8: rr_type__internet <= fld_class(fld_inherit(ptr_record))
-S- Applied substitution rule set_ttl_data_rules(42).
This was achieved by replacing all occurrences of rr_type__classtype__last
by:
rr_type__hs.
<S> New H9: fld_class(fld_inherit(ptr_record)) <= rr_type__hs
-S- Applied substitution rule set_ttl_data_rules(68).
This was achieved by replacing all occurrences of
rr_type__wirestringtypeindex__first by:
1.
<S> New H2: loop__1__i >= 1
<S> New H12: current_name_length >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <=
element(fld_domainname(ptr_record), [i___1]) and element(
fld_domainname(ptr_record), [i___1]) <= 255)
%%% Hypotheses H20 & H35 together imply that
loop__1__i < current_name_length.
H20 & H35 have therefore been deleted and a new H36 added to this effect.
*** Proved C20: loop__1__i + 1 <= current_name_length
via its standard form, which is:
Std.Fm C20: current_name_length - loop__1__i > 0
using hypothesis H36.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_set_ttl_data_ptr_response_7. @@@@@@@@@@
%%% Simplified H4 on reading formula in, to give:
%%% H4: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= dns_types__packet_bytes_range__last ->
dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
i___1]) <= dns_types__byte__last)
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
character__first <= element(fld_domainname(ptr_record), [i___1]) and
element(fld_domainname(ptr_record), [i___1]) <= character__last)
%%% Simplified H8 on reading formula in, to give:
%%% H8: rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
--- Hypothesis H15 has been replaced by "true". (It is already present, as
H13).
--- Hypothesis H16 has been replaced by "true". (It is already present, as H1)
.
--- Hypothesis H17 has been replaced by "true". (It is already present, as H2)
.
--- Hypothesis H18 has been replaced by "true". (It is already present, as H3)
.
*** Proved C5: loop__1__i >= rr_type__wirestringtypeindex__first
using hypothesis H2.
*** Proved C6: loop__1__i <= rr_type__wirestringtypeindex__last
using hypothesis H3.
*** Proved C7: start_byte + 5 + loop__1__i >=
dns_types__packet_bytes_range__first
using hypotheses H5 & H19.
-S- Applied substitution rule set_ttl_data_rules(23).
This was achieved by replacing all occurrences of dns_types__byte__first
by:
0.
<S> New H4: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= dns_types__packet_bytes_range__last -> 0 <=
element(bytes, [i___1]) and element(bytes, [i___1]) <=
dns_types__byte__last)
<S> New C1: element(fld_domainname(ptr_record), [loop__1__i]) >= 0
<S> New C3: element(fld_domainname(ptr_record), [loop__1__i]) >= 0
-S- Applied substitution rule set_ttl_data_rules(24).
This was achieved by replacing all occurrences of dns_types__byte__last by:
255.
<S> New H4: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= dns_types__packet_bytes_range__last -> 0 <=
element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
<S> New C2: element(fld_domainname(ptr_record), [loop__1__i]) <= 255
<S> New C4: element(fld_domainname(ptr_record), [loop__1__i]) <= 255
-S- Applied substitution rule set_ttl_data_rules(18).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__last by:
8180.
<S> New H1: start_byte <= 8174 - current_name_length
<S> New H6: start_byte <= 8180
<S> New H4: for_all(i___1 : integer, dns_types__packet_bytes_range__first <=
i___1 and i___1 <= 8180 -> 0 <= element(bytes, [i___1]) and element(
bytes, [i___1]) <= 255)
<S> New C8: start_byte + 5 + loop__1__i <= 8180
<S> New C12: loop__1__i <= 8180
-S- Applied substitution rule set_ttl_data_rules(19).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__base__first by:
- 2147483648.
<S> New C9: start_byte + 5 + loop__1__i >= - 2147483648
<S> New C13: start_byte >= - 2147483653
-S- Applied substitution rule set_ttl_data_rules(20).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__base__last by:
2147483647.
<S> New C10: start_byte + 5 + loop__1__i <= 2147483647
<S> New C14: start_byte <= 2147483642
-S- Applied substitution rule set_ttl_data_rules(17).
This was achieved by replacing all occurrences of
dns_types__packet_bytes_range__first by:
1.
<S> New H5: start_byte >= 1
<S> New H4: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <=
element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
<S> New C11: loop__1__i >= 1
*** Proved C9: start_byte + 5 + loop__1__i >= - 2147483648
using hypotheses H5 & H19.
*** Proved C13: start_byte >= - 2147483653
using hypothesis H5.
*** Proved C14: start_byte <= 2147483642
using hypothesis H6.
*** Proved C11: loop__1__i >= 1
using hypothesis H19.
-S- Applied substitution rule set_ttl_data_rules(7).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
ptr_record), [i___1]) <= character__last)
-S- Applied substitution rule set_ttl_data_rules(8).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
ptr_record), [i___1]) <= 255)
-S- Applied substitution rule set_ttl_data_rules(35).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New H10: fld_ttlinseconds(fld_inherit(ptr_record)) >= 0
-S- Applied substitution rule set_ttl_data_rules(36).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__last by:
4294967295.
<S> New H11: fld_ttlinseconds(fld_inherit(ptr_record)) <= 4294967295
-S- Applied substitution rule set_ttl_data_rules(41).
This was achieved by replacing all occurrences of
rr_type__classtype__first by:
rr_type__internet.
<S> New H8: rr_type__internet <= fld_class(fld_inherit(ptr_record))
-S- Applied substitution rule set_ttl_data_rules(42).
This was achieved by replacing all occurrences of rr_type__classtype__last
by:
rr_type__hs.
<S> New H9: fld_class(fld_inherit(ptr_record)) <= rr_type__hs
-S- Applied substitution rule set_ttl_data_rules(68).
This was achieved by replacing all occurrences of
rr_type__wirestringtypeindex__first by:
1.
<S> New H2: loop__1__i >= 1
<S> New H12: current_name_length >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
rr_type__wirestringtypeindex__last -> 0 <= element(fld_domainname(
ptr_record), [i___1]) and element(fld_domainname(ptr_record), [i___1])
<= 255)
-S- Applied substitution rule set_ttl_data_rules(69).
This was achieved by replacing all occurrences of
rr_type__wirestringtypeindex__last by:
129.
<S> New H3: loop__1__i <= 129
<S> New H13: current_name_length <= 129
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <=
element(fld_domainname(ptr_record), [i___1]) and element(
fld_domainname(ptr_record), [i___1]) <= 255)
*** Proved C1: element(fld_domainname(ptr_record), [loop__1__i]) >= 0
using hypotheses H3, H7 & H19.
*** Proved C3: element(fld_domainname(ptr_record), [loop__1__i]) >= 0
using hypotheses H3, H7 & H19.
*** Proved C2: element(fld_domainname(ptr_record), [loop__1__i]) <= 255
using hypotheses H3, H7 & H19.
*** Proved C4: element(fld_domainname(ptr_record), [loop__1__i]) <= 255
using hypotheses H3, H7 & H19.
*** Proved C12: loop__1__i <= 8180
using hypothesis H3.
*** Proved C10: start_byte + 5 + loop__1__i <= 2147483647
using hypotheses H3 & H6.
--- Eliminated hypothesis H15 (true-hypothesis).
--- Eliminated hypothesis H16 (true-hypothesis).
--- Eliminated hypothesis H17 (true-hypothesis).
--- Eliminated hypothesis H18 (true-hypothesis).
--- Eliminated hypothesis H19 (duplicate of H2).
--- Eliminated hypothesis H6 (redundant, given H1 & H12).
--- Eliminated hypothesis H14 (redundant, given H12).
+++ New H21: integer__size >= 0
+++ New H22: character__size >= 0
+++ New H23: positive__size >= 0
+++ New H24: dns_types__packet_bytes_range__size >= 0
+++ New H25: unsigned_types__unsigned16__size >= 0
+++ New H26: unsigned_types__unsigned32__size >= 0
+++ New H27: rr_type__classtype__size >= 0
+++ New H28: rr_type__wirestringtypeindex__size >= 0
+++ New H29: rr_type__resourcerecordtype__size >= 0
+++ New H30: rr_type__ptr_record_type__ptrrecordtype__size >= 0
@@@@@@@@@@ VC: procedure_set_ttl_data_ptr_response_8. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_set_ttl_data_ptr_response_9. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
Reference in New Issue View Git Blame Copy Permalink