111 lines
3.4 KiB
Sieve
111 lines
3.4 KiB
Sieve
*****************************************************************************
|
|
Semantic Analysis of SPARK Text
|
|
Examiner GPL Edition
|
|
|
|
*****************************************************************************
|
|
|
|
|
|
|
|
SPARK Simplifier GPL 2011
|
|
Copyright (C) 2011 Altran Praxis Limited, Bath, U.K.
|
|
|
|
function Rr_Type.DomainNameLength
|
|
|
|
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 31:
|
|
|
|
function_domainnamelength_1.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 32:
|
|
|
|
function_domainnamelength_2.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 33 to run-time check associated with
|
|
statement of line 32:
|
|
|
|
function_domainnamelength_3.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to assertion of line 33:
|
|
|
|
function_domainnamelength_4.
|
|
H1: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= element(
|
|
name, [i___1]) and element(name, [i___1]) <= 255) .
|
|
H2: element(name, [1]) <> 32 .
|
|
H3: element(name, [2]) <> 32 .
|
|
H4: integer__size >= 0 .
|
|
H5: character__size >= 0 .
|
|
H6: positive__size >= 0 .
|
|
H7: domainnamestringtypeindex__size >= 0 .
|
|
->
|
|
C1: for_all(q_ : integer, 1 <= q_ and q_ <= 2 -> element(name, [q_]) <> 32) .
|
|
|
|
|
|
For path(s) from assertion of line 33 to assertion of line 33:
|
|
|
|
function_domainnamelength_5.
|
|
H1: for_all(q_ : integer, 1 <= q_ and q_ <= index + 1 -> element(name, [q_])
|
|
<> 32) .
|
|
H2: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= element(
|
|
name, [i___1]) and element(name, [i___1]) <= 255) .
|
|
H3: index >= 1 .
|
|
H4: index < 127 .
|
|
H5: element(name, [1]) <> 32 .
|
|
H6: element(name, [index + 2]) <> 32 .
|
|
H7: index >= - 1 .
|
|
H8: index <= 126 .
|
|
H9: index >= - 2147483650 .
|
|
H10: index <= 2147483645 .
|
|
H11: integer__size >= 0 .
|
|
H12: character__size >= 0 .
|
|
H13: positive__size >= 0 .
|
|
H14: domainnamestringtypeindex__size >= 0 .
|
|
->
|
|
C1: for_all(q_ : integer, 1 <= q_ and q_ <= index + 2 -> element(name, [q_])
|
|
<> 32) .
|
|
|
|
|
|
For path(s) from assertion of line 33 to run-time check associated with
|
|
statement of line 35:
|
|
|
|
function_domainnamelength_6.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to finish:
|
|
|
|
function_domainnamelength_7.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 33 to finish:
|
|
|
|
function_domainnamelength_8.
|
|
H1: index < 128 .
|
|
H2: for_all(q_ : integer, 1 <= q_ and q_ <= index + 1 -> element(name, [q_])
|
|
<> 32) .
|
|
H3: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= element(
|
|
name, [i___1]) and element(name, [i___1]) <= 255) .
|
|
H4: index >= 1 .
|
|
H5: index < 127 and element(name, [1]) <> 32 -> index >= - 1 and index <=
|
|
126 .
|
|
H6: index < 127 and element(name, [1]) <> 32 -> index >= - 2147483650 and
|
|
index <= 2147483645 .
|
|
H7: 127 <= index or element(name, [index + 2]) = 32 .
|
|
H8: integer__size >= 0 .
|
|
H9: character__size >= 0 .
|
|
H10: positive__size >= 0 .
|
|
H11: domainnamestringtypeindex__size >= 0 .
|
|
->
|
|
C1: index = 127 or element(name, [index + 2]) = 32 and for_all(q_ : integer,
|
|
1 <= q_ and q_ <= index + 1 -> element(name, [q_]) <> 32) .
|
|
|
|
|