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