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