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:21
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_R
14
15
16
17
18For path(s) from start to run-time check associated with statement of line 38:
19
20function_k_r_1.
21*** true .          /* all conclusions proved */
22
23
24For path(s) from start to run-time check associated with statement of line 39:
25
26function_k_r_2.
27*** true .          /* all conclusions proved */
28
29
30For path(s) from start to run-time check associated with statement of line 40:
31
32function_k_r_3.
33*** true .          /* all conclusions proved */
34
35
36For path(s) from start to run-time check associated with statement of line 41:
37
38function_k_r_4.
39*** true .          /* all conclusions proved */
40
41
42For path(s) from start to run-time check associated with statement of line 42:
43
44function_k_r_5.
45*** true .          /* all conclusions proved */
46
47
48For path(s) from start to finish:
49
50function_k_r_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:    1352829926 = k_r_spec(j) .
61
62
63function_k_r_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:    1548603684 = k_r_spec(j) .
74
75
76function_k_r_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:    1836072691 = k_r_spec(j) .
87
88
89function_k_r_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:    2053994217 = k_r_spec(j) .
100
101
102function_k_r_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:    0 = k_r_spec(j) .
117
118
119