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.F
14
15
16
17
18For path(s) from start to run-time check associated with statement of line 9:
19
20function_f_1.
21*** true .          /* all conclusions proved */
22
23
24For path(s) from start to run-time check associated with statement of line 10:
25
26function_f_2.
27H1:    x >= 0 .
28H2:    x <= 4294967295 .
29H3:    y >= 0 .
30H4:    y <= 4294967295 .
31H5:    z >= 0 .
32H6:    z <= 4294967295 .
33H7:    16 <= j .
34H8:    j <= 31 .
35H9:    interfaces__unsigned_32__size >= 0 .
36H10:   word__size >= 0 .
37H11:   round_index__size >= 0 .
38H12:   round_index__base__first <= round_index__base__last .
39H13:   round_index__base__first <= 0 .
40H14:   round_index__base__last >= 79 .
41       ->
42C1:    bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) >= 0 .
43C2:    bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) <= 4294967295 .
44
45
46For path(s) from start to run-time check associated with statement of line 11:
47
48function_f_3.
49H1:    x >= 0 .
50H2:    x <= 4294967295 .
51H3:    y >= 0 .
52H4:    y <= 4294967295 .
53H5:    z >= 0 .
54H6:    z <= 4294967295 .
55H7:    32 <= j .
56H8:    j <= 47 .
57H9:    interfaces__unsigned_32__size >= 0 .
58H10:   word__size >= 0 .
59H11:   round_index__size >= 0 .
60H12:   round_index__base__first <= round_index__base__last .
61H13:   round_index__base__first <= 0 .
62H14:   round_index__base__last >= 79 .
63       ->
64C1:    bit__xor(bit__or(x, 4294967295 - y), z) >= 0 .
65C2:    bit__xor(bit__or(x, 4294967295 - y), z) <= 4294967295 .
66
67
68For path(s) from start to run-time check associated with statement of line 12:
69
70function_f_4.
71H1:    x >= 0 .
72H2:    x <= 4294967295 .
73H3:    y >= 0 .
74H4:    y <= 4294967295 .
75H5:    z >= 0 .
76H6:    z <= 4294967295 .
77H7:    48 <= j .
78H8:    j <= 63 .
79H9:    interfaces__unsigned_32__size >= 0 .
80H10:   word__size >= 0 .
81H11:   round_index__size >= 0 .
82H12:   round_index__base__first <= round_index__base__last .
83H13:   round_index__base__first <= 0 .
84H14:   round_index__base__last >= 79 .
85       ->
86C1:    bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) >= 0 .
87C2:    bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) <= 4294967295 .
88
89
90For path(s) from start to run-time check associated with statement of line 13:
91
92function_f_5.
93H1:    j >= 0 .
94H2:    j <= 79 .
95H3:    x >= 0 .
96H4:    x <= 4294967295 .
97H5:    y >= 0 .
98H6:    y <= 4294967295 .
99H7:    z >= 0 .
100H8:    z <= 4294967295 .
101H9:    15 < j .
102H10:   31 < j .
103H11:   47 < j .
104H12:   63 < j .
105H13:   interfaces__unsigned_32__size >= 0 .
106H14:   word__size >= 0 .
107H15:   round_index__size >= 0 .
108H16:   round_index__base__first <= round_index__base__last .
109H17:   round_index__base__first <= 0 .
110H18:   round_index__base__last >= 79 .
111       ->
112C1:    bit__xor(x, bit__or(y, 4294967295 - z)) >= 0 .
113C2:    bit__xor(x, bit__or(y, 4294967295 - z)) <= 4294967295 .
114
115
116For path(s) from start to finish:
117
118function_f_6.
119H1:    j >= 0 .
120H2:    x >= 0 .
121H3:    x <= 4294967295 .
122H4:    y >= 0 .
123H5:    y <= 4294967295 .
124H6:    z >= 0 .
125H7:    z <= 4294967295 .
126H8:    j <= 15 .
127H9:    bit__xor(x, bit__xor(y, z)) >= 0 .
128H10:   bit__xor(x, bit__xor(y, z)) <= 4294967295 .
129H11:   interfaces__unsigned_32__size >= 0 .
130H12:   word__size >= 0 .
131H13:   round_index__size >= 0 .
132H14:   round_index__base__first <= round_index__base__last .
133H15:   round_index__base__first <= 0 .
134H16:   round_index__base__last >= 79 .
135       ->
136C1:    bit__xor(x, bit__xor(y, z)) = f_spec(j, x, y, z) .
137
138
139function_f_7.
140H1:    x >= 0 .
141H2:    x <= 4294967295 .
142H3:    y >= 0 .
143H4:    y <= 4294967295 .
144H5:    z >= 0 .
145H6:    z <= 4294967295 .
146H7:    16 <= j .
147H8:    j <= 31 .
148H9:    bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) >= 0 .
149H10:   bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) <= 4294967295 .
150H11:   interfaces__unsigned_32__size >= 0 .
151H12:   word__size >= 0 .
152H13:   round_index__size >= 0 .
153H14:   round_index__base__first <= round_index__base__last .
154H15:   round_index__base__first <= 0 .
155H16:   round_index__base__last >= 79 .
156       ->
157C1:    bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) = f_spec(j, x, y, z)
158           .
159
160
161function_f_8.
162H1:    x >= 0 .
163H2:    x <= 4294967295 .
164H3:    y >= 0 .
165H4:    y <= 4294967295 .
166H5:    z >= 0 .
167H6:    z <= 4294967295 .
168H7:    32 <= j .
169H8:    j <= 47 .
170H9:    bit__xor(bit__or(x, 4294967295 - y), z) >= 0 .
171H10:   bit__xor(bit__or(x, 4294967295 - y), z) <= 4294967295 .
172H11:   interfaces__unsigned_32__size >= 0 .
173H12:   word__size >= 0 .
174H13:   round_index__size >= 0 .
175H14:   round_index__base__first <= round_index__base__last .
176H15:   round_index__base__first <= 0 .
177H16:   round_index__base__last >= 79 .
178       ->
179C1:    bit__xor(bit__or(x, 4294967295 - y), z) = f_spec(j, x, y, z) .
180
181
182function_f_9.
183H1:    x >= 0 .
184H2:    x <= 4294967295 .
185H3:    y >= 0 .
186H4:    y <= 4294967295 .
187H5:    z >= 0 .
188H6:    z <= 4294967295 .
189H7:    48 <= j .
190H8:    j <= 63 .
191H9:    bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) >= 0 .
192H10:   bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) <= 4294967295 .
193H11:   interfaces__unsigned_32__size >= 0 .
194H12:   word__size >= 0 .
195H13:   round_index__size >= 0 .
196H14:   round_index__base__first <= round_index__base__last .
197H15:   round_index__base__first <= 0 .
198H16:   round_index__base__last >= 79 .
199       ->
200C1:    bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) = f_spec(j, x, y, z)
201           .
202
203
204function_f_10.
205H1:    j >= 0 .
206H2:    j <= 79 .
207H3:    x >= 0 .
208H4:    x <= 4294967295 .
209H5:    y >= 0 .
210H6:    y <= 4294967295 .
211H7:    z >= 0 .
212H8:    z <= 4294967295 .
213H9:    15 < j .
214H10:   31 < j .
215H11:   47 < j .
216H12:   63 < j .
217H13:   bit__xor(x, bit__or(y, 4294967295 - z)) >= 0 .
218H14:   bit__xor(x, bit__or(y, 4294967295 - z)) <= 4294967295 .
219H15:   interfaces__unsigned_32__size >= 0 .
220H16:   word__size >= 0 .
221H17:   round_index__size >= 0 .
222H18:   round_index__base__first <= round_index__base__last .
223H19:   round_index__base__first <= 0 .
224H20:   round_index__base__last >= 79 .
225       ->
226C1:    bit__xor(x, bit__or(y, 4294967295 - z)) = f_spec(j, x, y, z) .
227
228
229