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