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:30
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.S_R
14
15
16
17
18For path(s) from start to run-time check associated with statement of line 101:
19
20function_s_r_1.
21*** true .          /* all conclusions proved */
22
23
24For path(s) from start to finish:
25
26function_s_r_2.
27H1:    j >= 0 .
28H2:    j <= 79 .
29H3:    integer__size >= 0 .
30H4:    round_index__size >= 0 .
31H5:    round_index__base__first <= round_index__base__last .
32H6:    rotate_amount__size >= 0 .
33H7:    round_index__base__first <= 0 .
34H8:    round_index__base__last >= 79 .
35       ->
36C1:    element(mk__rotate_definition([0] := 8, [1] := 9, [2] := 9, [3] := 11, [
37          4] := 13, [5] := 15, [6] := 15, [7] := 5, [8] := 7, [9] := 7, [10] := 
38          8, [11] := 11, [12] := 14, [13] := 14, [14] := 12, [15] := 6, [16] := 
39          9, [17] := 13, [18] := 15, [19] := 7, [20] := 12, [21] := 8, [22] := 
40          9, [23] := 11, [24] := 7, [25] := 7, [26] := 12, [27] := 7, [28] := 
41          6, [29] := 15, [30] := 13, [31] := 11, [32] := 9, [33] := 7, [34] := 
42          15, [35] := 11, [36] := 8, [37] := 6, [38] := 6, [39] := 14, [40] := 
43          12, [41] := 13, [42] := 5, [43] := 14, [44] := 13, [45] := 13, [46] 
44          := 7, [47] := 5, [48] := 15, [49] := 5, [50] := 8, [51] := 11, [52] 
45          := 14, [53] := 14, [54] := 6, [55] := 14, [56] := 6, [57] := 9, [58] 
46          := 12, [59] := 9, [60] := 12, [61] := 5, [62] := 15, [63] := 8, [64] 
47          := 8, [65] := 5, [66] := 12, [67] := 9, [68] := 12, [69] := 5, [70] 
48          := 14, [71] := 6, [72] := 8, [73] := 13, [74] := 6, [75] := 5, [76] 
49          := 15, [77] := 13, [78] := 11, [79] := 11), [j]) = s_r_spec(j) .
50C2:    element(mk__rotate_definition([0] := 8, [1] := 9, [2] := 9, [3] := 11, [
51          4] := 13, [5] := 15, [6] := 15, [7] := 5, [8] := 7, [9] := 7, [10] := 
52          8, [11] := 11, [12] := 14, [13] := 14, [14] := 12, [15] := 6, [16] := 
53          9, [17] := 13, [18] := 15, [19] := 7, [20] := 12, [21] := 8, [22] := 
54          9, [23] := 11, [24] := 7, [25] := 7, [26] := 12, [27] := 7, [28] := 
55          6, [29] := 15, [30] := 13, [31] := 11, [32] := 9, [33] := 7, [34] := 
56          15, [35] := 11, [36] := 8, [37] := 6, [38] := 6, [39] := 14, [40] := 
57          12, [41] := 13, [42] := 5, [43] := 14, [44] := 13, [45] := 13, [46] 
58          := 7, [47] := 5, [48] := 15, [49] := 5, [50] := 8, [51] := 11, [52] 
59          := 14, [53] := 14, [54] := 6, [55] := 14, [56] := 6, [57] := 9, [58] 
60          := 12, [59] := 9, [60] := 12, [61] := 5, [62] := 15, [63] := 8, [64] 
61          := 8, [65] := 5, [66] := 12, [67] := 9, [68] := 12, [69] := 5, [70] 
62          := 14, [71] := 6, [72] := 8, [73] := 13, [74] := 6, [75] := 5, [76] 
63          := 15, [77] := 13, [78] := 11, [79] := 11), [j]) >= 0 .
64C3:    element(mk__rotate_definition([0] := 8, [1] := 9, [2] := 9, [3] := 11, [
65          4] := 13, [5] := 15, [6] := 15, [7] := 5, [8] := 7, [9] := 7, [10] := 
66          8, [11] := 11, [12] := 14, [13] := 14, [14] := 12, [15] := 6, [16] := 
67          9, [17] := 13, [18] := 15, [19] := 7, [20] := 12, [21] := 8, [22] := 
68          9, [23] := 11, [24] := 7, [25] := 7, [26] := 12, [27] := 7, [28] := 
69          6, [29] := 15, [30] := 13, [31] := 11, [32] := 9, [33] := 7, [34] := 
70          15, [35] := 11, [36] := 8, [37] := 6, [38] := 6, [39] := 14, [40] := 
71          12, [41] := 13, [42] := 5, [43] := 14, [44] := 13, [45] := 13, [46] 
72          := 7, [47] := 5, [48] := 15, [49] := 5, [50] := 8, [51] := 11, [52] 
73          := 14, [53] := 14, [54] := 6, [55] := 14, [56] := 6, [57] := 9, [58] 
74          := 12, [59] := 9, [60] := 12, [61] := 5, [62] := 15, [63] := 8, [64] 
75          := 8, [65] := 5, [66] := 12, [67] := 9, [68] := 12, [69] := 5, [70] 
76          := 14, [71] := 6, [72] := 8, [73] := 13, [74] := 6, [75] := 5, [76] 
77          := 15, [77] := 13, [78] := 11, [79] := 11), [j]) <= 15 .
78
79
80