1*****************************************************************************
2                       Semantic Analysis of SPARK Text
3    Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
4             Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
5*****************************************************************************
6
7
8CREATED 29-NOV-2010, 14:30:19  SIMPLIFIED 29-NOV-2010, 14:30:28
9
10SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
11Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
12
13function RMD.K_L
14
15
16
17
18For path(s) from start to run-time check associated with statement of line 24:
19
20function_k_l_1.
21*** true .          /* all conclusions proved */
22
23
24For path(s) from start to run-time check associated with statement of line 25:
25
26function_k_l_2.
27*** true .          /* all conclusions proved */
28
29
30For path(s) from start to run-time check associated with statement of line 26:
31
32function_k_l_3.
33*** true .          /* all conclusions proved */
34
35
36For path(s) from start to run-time check associated with statement of line 27:
37
38function_k_l_4.
39*** true .          /* all conclusions proved */
40
41
42For path(s) from start to run-time check associated with statement of line 28:
43
44function_k_l_5.
45*** true .          /* all conclusions proved */
46
47
48For path(s) from start to finish:
49
50function_k_l_6.
51H1:    j >= 0 .
52H2:    j <= 15 .
53H3:    interfaces__unsigned_32__size >= 0 .
54H4:    word__size >= 0 .
55H5:    round_index__size >= 0 .
56H6:    round_index__base__first <= round_index__base__last .
57H7:    round_index__base__first <= 0 .
58H8:    round_index__base__last >= 79 .
59       ->
60C1:    0 = k_l_spec(j) .
61
62
63function_k_l_7.
64H1:    16 <= j .
65H2:    j <= 31 .
66H3:    interfaces__unsigned_32__size >= 0 .
67H4:    word__size >= 0 .
68H5:    round_index__size >= 0 .
69H6:    round_index__base__first <= round_index__base__last .
70H7:    round_index__base__first <= 0 .
71H8:    round_index__base__last >= 79 .
72       ->
73C1:    1518500249 = k_l_spec(j) .
74
75
76function_k_l_8.
77H1:    32 <= j .
78H2:    j <= 47 .
79H3:    interfaces__unsigned_32__size >= 0 .
80H4:    word__size >= 0 .
81H5:    round_index__size >= 0 .
82H6:    round_index__base__first <= round_index__base__last .
83H7:    round_index__base__first <= 0 .
84H8:    round_index__base__last >= 79 .
85       ->
86C1:    1859775393 = k_l_spec(j) .
87
88
89function_k_l_9.
90H1:    48 <= j .
91H2:    j <= 63 .
92H3:    interfaces__unsigned_32__size >= 0 .
93H4:    word__size >= 0 .
94H5:    round_index__size >= 0 .
95H6:    round_index__base__first <= round_index__base__last .
96H7:    round_index__base__first <= 0 .
97H8:    round_index__base__last >= 79 .
98       ->
99C1:    2400959708 = k_l_spec(j) .
100
101
102function_k_l_10.
103H1:    j >= 0 .
104H2:    j <= 79 .
105H3:    15 < j .
106H4:    31 < j .
107H5:    47 < j .
108H6:    63 < j .
109H7:    interfaces__unsigned_32__size >= 0 .
110H8:    word__size >= 0 .
111H9:    round_index__size >= 0 .
112H10:   round_index__base__first <= round_index__base__last .
113H11:   round_index__base__first <= 0 .
114H12:   round_index__base__last >= 79 .
115       ->
116C1:    2840853838 = k_l_spec(j) .
117
118
119