354 lines
17 KiB
Plaintext
354 lines
17 KiB
Plaintext
*****************************************************************************
|
|
Semantic Analysis of SPARK Text
|
|
Examiner GPL Edition
|
|
|
|
*****************************************************************************
|
|
|
|
|
|
|
|
SPARK Simplifier GPL 2011
|
|
Copyright (C) 2011 Altran Praxis Limited, Bath, U.K.
|
|
|
|
function dns_table_pkg.DNS_Table_Type.To_Lower
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@@@@@@@@@@ VC: function_to_lower_1. @@@@@@@@@@
|
|
%%% Simplified H2 on reading formula in, to give:
|
|
%%% H2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
|
|
character__first <= element(domainname, [i___1]) and element(
|
|
domainname, [i___1]) <= character__last)
|
|
%%% Simplified H5 on reading formula in, to give:
|
|
%%% H5: rr_type__wirenamelength(domainname) =
|
|
rr_type__maxdomainnamelength + 1 or element(domainname, [
|
|
rr_type__wirenamelength(domainname)]) = 0 and for_all(q_ : integer, 1
|
|
<= q_ and q_ <= rr_type__wirenamelength(domainname) - 1 -> element(
|
|
domainname, [q_]) <> 0)
|
|
*** Proved C1: rr_type__wirenamelength(domainname) >=
|
|
rr_type__wirestringtypeindex__first
|
|
using hypothesis H3.
|
|
*** Proved C2: rr_type__wirenamelength(domainname) <=
|
|
rr_type__wirestringtypeindex__last
|
|
using hypothesis H4.
|
|
*** PROVED VC.
|
|
|
|
|
|
@@@@@@@@@@ VC: function_to_lower_2. @@@@@@@@@@
|
|
%%% Simplified H2 on reading formula in, to give:
|
|
%%% H2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
|
|
character__first <= element(domainname, [i___1]) and element(
|
|
domainname, [i___1]) <= character__last)
|
|
%%% Simplified H5 on reading formula in, to give:
|
|
%%% H5: rr_type__wirenamelength(domainname) =
|
|
rr_type__maxdomainnamelength + 1 or element(domainname, [
|
|
rr_type__wirenamelength(domainname)]) = 0 and for_all(q_ : integer, 1
|
|
<= q_ and q_ <= rr_type__wirenamelength(domainname) - 1 -> element(
|
|
domainname, [q_]) <> 0)
|
|
--- Hypothesis H6 has been replaced by "true". (It is already present, as H3).
|
|
--- Hypothesis H7 has been replaced by "true". (It is already present, as H4).
|
|
--- Hypothesis H8 has been replaced by "true". (It is already present, as H3).
|
|
--- Hypothesis H9 has been replaced by "true". (It is already present, as H4).
|
|
-S- Applied substitution rule to_lower_rules(3).
|
|
This was achieved by replacing all occurrences of integer__first by:
|
|
- 2147483648.
|
|
<S> New C1: rr_type__wirenamelength(domainname) >= - 2147483648
|
|
<S> New C3: true
|
|
-S- Applied substitution rule to_lower_rules(4).
|
|
This was achieved by replacing all occurrences of integer__last by:
|
|
2147483647.
|
|
<S> New C2: rr_type__wirenamelength(domainname) <= 2147483647
|
|
<S> New C4: true
|
|
*** Proved C3: true
|
|
*** Proved C4: true
|
|
-S- Applied substitution rule to_lower_rules(1).
|
|
This was achieved by replacing all occurrences of
|
|
rr_type__maxdomainnamelength by:
|
|
128.
|
|
<S> New H5: rr_type__wirenamelength(domainname) = 129 or element(domainname, [
|
|
rr_type__wirenamelength(domainname)]) = 0 and for_all(q_ : integer, 1
|
|
<= q_ and q_ <= rr_type__wirenamelength(domainname) - 1 -> element(
|
|
domainname, [q_]) <> 0)
|
|
-S- Applied substitution rule to_lower_rules(8).
|
|
This was achieved by replacing all occurrences of character__first by:
|
|
0.
|
|
<S> New H2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
|
|
domainname, [i___1]) and element(domainname, [i___1]) <=
|
|
character__last)
|
|
-S- Applied substitution rule to_lower_rules(9).
|
|
This was achieved by replacing all occurrences of character__last by:
|
|
255.
|
|
<S> New H2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
|
|
domainname, [i___1]) and element(domainname, [i___1]) <= 255)
|
|
-S- Applied substitution rule to_lower_rules(18).
|
|
This was achieved by replacing all occurrences of
|
|
rr_type__wirestringtypeindex__first by:
|
|
1.
|
|
<S> New H3: rr_type__wirenamelength(domainname) >= 1
|
|
<S> New H2: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
|
|
rr_type__wirestringtypeindex__last -> 0 <= element(domainname, [i___1]
|
|
) and element(domainname, [i___1]) <= 255)
|
|
-S- Applied substitution rule to_lower_rules(19).
|
|
This was achieved by replacing all occurrences of
|
|
rr_type__wirestringtypeindex__last by:
|
|
129.
|
|
<S> New H4: rr_type__wirenamelength(domainname) <= 129
|
|
<S> New H2: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <=
|
|
element(domainname, [i___1]) and element(domainname, [i___1]) <= 255)
|
|
*** Proved C1: rr_type__wirenamelength(domainname) >= - 2147483648
|
|
using hypothesis H3.
|
|
*** Proved C2: rr_type__wirenamelength(domainname) <= 2147483647
|
|
using hypothesis H4.
|
|
*** PROVED VC.
|
|
|
|
|
|
@@@@@@@@@@ VC: function_to_lower_3. @@@@@@@@@@
|
|
%%% Simplified H2 on reading formula in, to give:
|
|
%%% H2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
|
|
character__first <= element(domainname, [i___1]) and element(
|
|
domainname, [i___1]) <= character__last)
|
|
%%% Simplified H5 on reading formula in, to give:
|
|
%%% H5: rr_type__wirenamelength(domainname) =
|
|
rr_type__maxdomainnamelength + 1 or element(domainname, [
|
|
rr_type__wirenamelength(domainname)]) = 0 and for_all(q_ : integer, 1
|
|
<= q_ and q_ <= rr_type__wirenamelength(domainname) - 1 -> element(
|
|
domainname, [q_]) <> 0)
|
|
--- Hypothesis H6 has been replaced by "true". (It is already present, as H3).
|
|
--- Hypothesis H7 has been replaced by "true". (It is already present, as H4).
|
|
--- Hypothesis H8 has been replaced by "true". (It is already present, as H3).
|
|
--- Hypothesis H9 has been replaced by "true". (It is already present, as H4).
|
|
*** Proved C1: 1 <= rr_type__wirenamelength(domainname) ->
|
|
rr_type__wirenamelength(domainname) >= integer__first and
|
|
rr_type__wirenamelength(domainname) <= integer__last
|
|
using hypotheses H10 & H11.
|
|
*** Proved C2: 1 <= rr_type__wirenamelength(domainname) -> 1 >=
|
|
integer__first and 1 <= integer__last
|
|
using hypotheses H12 & H13.
|
|
*** PROVED VC.
|
|
|
|
|
|
@@@@@@@@@@ VC: function_to_lower_4. @@@@@@@@@@
|
|
%%% Simplified H2 on reading formula in, to give:
|
|
%%% H2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
|
|
character__first <= element(domainname, [i___1]) and element(
|
|
domainname, [i___1]) <= character__last)
|
|
%%% Simplified H5 on reading formula in, to give:
|
|
%%% H5: rr_type__wirenamelength(domainname) =
|
|
rr_type__maxdomainnamelength + 1 or element(domainname, [
|
|
rr_type__wirenamelength(domainname)]) = 0 and for_all(q_ : integer, 1
|
|
<= q_ and q_ <= rr_type__wirenamelength(domainname) - 1 -> element(
|
|
domainname, [q_]) <> 0)
|
|
--- Hypothesis H6 has been replaced by "true". (It is already present, as H3).
|
|
--- Hypothesis H7 has been replaced by "true". (It is already present, as H4).
|
|
--- Hypothesis H8 has been replaced by "true". (It is already present, as H3).
|
|
--- Hypothesis H9 has been replaced by "true". (It is already present, as H4).
|
|
--- Hypothesis H16 has been replaced by "true". (It is already present, as H3)
|
|
.
|
|
--- Hypothesis H17 has been replaced by "true". (It is already present, as H4)
|
|
.
|
|
%%% Simplified C2 on reading formula in, to give:
|
|
%%% C2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
|
|
character__first <= element(domainname, [i___1]) and element(
|
|
domainname, [i___1]) <= character__last)
|
|
%%% Simplified C5 on reading formula in, to give:
|
|
%%% C5: true
|
|
*** Proved C1: true
|
|
*** Proved C2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first
|
|
<= i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
|
|
character__first <= element(domainname, [i___1]) and element(
|
|
domainname, [i___1]) <= character__last)
|
|
using hypothesis H2.
|
|
*** Proved C3: 1 >= integer__first
|
|
using hypothesis H12.
|
|
*** Proved C4: 1 <= integer__last
|
|
using hypothesis H13.
|
|
*** Proved C5: true
|
|
*** Proved C6: 1 <= rr_type__wirenamelength(domainname)
|
|
using hypothesis H18.
|
|
*** Proved C7: rr_type__wirenamelength(domainname) >=
|
|
rr_type__wirestringtypeindex__first
|
|
using hypothesis H3.
|
|
*** Proved C8: rr_type__wirenamelength(domainname) <=
|
|
rr_type__wirestringtypeindex__last
|
|
using hypothesis H4.
|
|
*** PROVED VC.
|
|
|
|
|
|
@@@@@@@@@@ VC: function_to_lower_5. @@@@@@@@@@
|
|
%%% Simplified H2 on reading formula in, to give:
|
|
%%% H2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
|
|
character__first <= element(domainname, [i___1]) and element(
|
|
domainname, [i___1]) <= character__last)
|
|
--- Hypothesis H13 has been replaced by "true". (It is already present, as
|
|
H11).
|
|
--- Hypothesis H14 has been replaced by "true". (It is already present, as
|
|
H12).
|
|
--- Hypothesis H17 has been replaced by "true". (It is already present, as
|
|
H15).
|
|
--- Hypothesis H18 has been replaced by "true". (It is already present, as
|
|
H16).
|
|
%%% Simplified C2 on reading formula in, to give:
|
|
%%% C2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
|
|
character__first <= element(domainname, [i___1]) and element(
|
|
domainname, [i___1]) <= character__last)
|
|
%%% Simplified C5 on reading formula in, to give:
|
|
%%% C5: loop__1__i >= 0
|
|
*** Proved C1: true
|
|
*** Proved C2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first
|
|
<= i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
|
|
character__first <= element(domainname, [i___1]) and element(
|
|
domainname, [i___1]) <= character__last)
|
|
using hypothesis H2.
|
|
*** Proved C3: loop__1__i + 1 >= integer__first
|
|
using hypothesis H3.
|
|
*** Proved C5: loop__1__i >= 0
|
|
using hypothesis H5.
|
|
*** Proved C7: length__entry__loop__1 >= rr_type__wirestringtypeindex__first
|
|
using hypothesis H7.
|
|
*** Proved C8: length__entry__loop__1 <= rr_type__wirestringtypeindex__last
|
|
using hypothesis H8.
|
|
-S- Applied substitution rule to_lower_rules(4).
|
|
This was achieved by replacing all occurrences of integer__last by:
|
|
2147483647.
|
|
<S> New H4: loop__1__i <= 2147483647
|
|
<S> New C4: loop__1__i <= 2147483646
|
|
>>> Restructured hypothesis H19 into:
|
|
>>> H19: loop__1__i <> length__entry__loop__1
|
|
-S- Applied substitution rule to_lower_rules(3).
|
|
This was achieved by replacing all occurrences of integer__first by:
|
|
- 2147483648.
|
|
<S> New H3: loop__1__i >= - 2147483648
|
|
-S- Applied substitution rule to_lower_rules(8).
|
|
This was achieved by replacing all occurrences of character__first by:
|
|
0.
|
|
<S> New H2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
|
|
domainname, [i___1]) and element(domainname, [i___1]) <=
|
|
character__last)
|
|
<S> New H9: element(domainname, [loop__1__i]) >= 0
|
|
<S> New H15: ada__characters__handling__to_lower(element(domainname, [
|
|
loop__1__i])) >= 0
|
|
-S- Applied substitution rule to_lower_rules(9).
|
|
This was achieved by replacing all occurrences of character__last by:
|
|
255.
|
|
<S> New H10: element(domainname, [loop__1__i]) <= 255
|
|
<S> New H16: ada__characters__handling__to_lower(element(domainname, [
|
|
loop__1__i])) <= 255
|
|
<S> New H2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
|
|
domainname, [i___1]) and element(domainname, [i___1]) <= 255)
|
|
-S- Applied substitution rule to_lower_rules(18).
|
|
This was achieved by replacing all occurrences of
|
|
rr_type__wirestringtypeindex__first by:
|
|
1.
|
|
<S> New H7: length__entry__loop__1 >= 1
|
|
<S> New H11: loop__1__i >= 1
|
|
<S> New H2: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
|
|
rr_type__wirestringtypeindex__last -> 0 <= element(domainname, [i___1]
|
|
) and element(domainname, [i___1]) <= 255)
|
|
-S- Applied substitution rule to_lower_rules(19).
|
|
This was achieved by replacing all occurrences of
|
|
rr_type__wirestringtypeindex__last by:
|
|
129.
|
|
<S> New H8: length__entry__loop__1 <= 129
|
|
<S> New H12: loop__1__i <= 129
|
|
<S> New H2: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <=
|
|
element(domainname, [i___1]) and element(domainname, [i___1]) <= 255)
|
|
%%% Hypotheses H6 & H19 together imply that
|
|
loop__1__i < length__entry__loop__1.
|
|
H6 & H19 have therefore been deleted and a new H20 added to this effect.
|
|
*** Proved C6: loop__1__i + 1 <= length__entry__loop__1
|
|
via its standard form, which is:
|
|
Std.Fm C6: length__entry__loop__1 - loop__1__i > 0
|
|
using hypothesis H20.
|
|
*** Proved C4: loop__1__i <= 2147483646
|
|
using hypothesis H12.
|
|
*** PROVED VC.
|
|
|
|
|
|
@@@@@@@@@@ VC: function_to_lower_6. @@@@@@@@@@
|
|
%%% Simplified H2 on reading formula in, to give:
|
|
%%% H2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
|
|
character__first <= element(domainname, [i___1]) and element(
|
|
domainname, [i___1]) <= character__last)
|
|
*** Proved C4: loop__1__i <= rr_type__wirestringtypeindex__last
|
|
using hypotheses H6 & H8.
|
|
*** Proved C6: loop__1__i <= rr_type__wirestringtypeindex__last
|
|
using hypotheses H6 & H8.
|
|
-S- Applied substitution rule to_lower_rules(8).
|
|
This was achieved by replacing all occurrences of character__first by:
|
|
0.
|
|
<S> New H2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
|
|
domainname, [i___1]) and element(domainname, [i___1]) <=
|
|
character__last)
|
|
<S> New C1: element(domainname, [loop__1__i]) >= 0
|
|
-S- Applied substitution rule to_lower_rules(9).
|
|
This was achieved by replacing all occurrences of character__last by:
|
|
255.
|
|
<S> New H2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
|
|
domainname, [i___1]) and element(domainname, [i___1]) <= 255)
|
|
<S> New C2: element(domainname, [loop__1__i]) <= 255
|
|
-S- Applied substitution rule to_lower_rules(18).
|
|
This was achieved by replacing all occurrences of
|
|
rr_type__wirestringtypeindex__first by:
|
|
1.
|
|
<S> New H7: length__entry__loop__1 >= 1
|
|
<S> New H2: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
|
|
rr_type__wirestringtypeindex__last -> 0 <= element(domainname, [i___1]
|
|
) and element(domainname, [i___1]) <= 255)
|
|
<S> New C3: loop__1__i >= 1
|
|
<S> New C5: loop__1__i >= 1
|
|
*** Proved C1: element(domainname, [loop__1__i]) >= 0
|
|
using hypotheses H2, H5, H6 & H8.
|
|
*** Proved C2: element(domainname, [loop__1__i]) <= 255
|
|
using hypotheses H2, H5, H6 & H8.
|
|
*** Proved C3: loop__1__i >= 1
|
|
using hypothesis H5.
|
|
*** Proved C5: loop__1__i >= 1
|
|
using hypothesis H5.
|
|
*** PROVED VC.
|
|
|
|
|
|
@@@@@@@@@@ VC: function_to_lower_7. @@@@@@@@@@
|
|
%%% Simplified H2 on reading formula in, to give:
|
|
%%% H2: for_all(i___1 : integer, rr_type__wirestringtypeindex__first <=
|
|
i___1 and i___1 <= rr_type__wirestringtypeindex__last ->
|
|
character__first <= element(domainname, [i___1]) and element(
|
|
domainname, [i___1]) <= character__last)
|
|
--- Hypothesis H13 has been replaced by "true". (It is already present, as
|
|
H11).
|
|
--- Hypothesis H14 has been replaced by "true". (It is already present, as
|
|
H12).
|
|
*** Proved C1: ada__characters__handling__to_lower(element(domainname, [
|
|
loop__1__i])) >= character__first
|
|
using hypothesis H15.
|
|
*** Proved C2: ada__characters__handling__to_lower(element(domainname, [
|
|
loop__1__i])) <= character__last
|
|
using hypothesis H16.
|
|
*** PROVED VC.
|
|
|
|
|
|
@@@@@@@@@@ VC: function_to_lower_8. @@@@@@@@@@
|
|
*** Proved C1: true
|
|
*** PROVED VC.
|
|
|
|
|
|
@@@@@@@@@@ VC: function_to_lower_9. @@@@@@@@@@
|
|
*** Proved C1: true
|
|
*** PROVED VC.
|
|
|