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:20 SIMPLIFIED 29-NOV-2010, 14:30:20 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.Hash 14 15 16 17 18For path(s) from start to run-time check associated with statement of line 170: 19 20function_hash_1. 21*** true . /* all conclusions proved */ 22 23 24For path(s) from start to run-time check associated with statement of line 171: 25 26function_hash_2. 27*** true . /* all conclusions proved */ 28 29 30For path(s) from start to run-time check associated with statement of line 172: 31 32function_hash_3. 33*** true . /* all conclusions proved */ 34 35 36For path(s) from start to run-time check associated with statement of line 173: 37 38function_hash_4. 39*** true . /* all conclusions proved */ 40 41 42For path(s) from start to run-time check associated with statement of line 174: 43 44function_hash_5. 45*** true . /* all conclusions proved */ 46 47 48For path(s) from start to run-time check associated with statement of line 175: 49 50function_hash_6. 51*** true . /* all conclusions proved */ 52 53 54For path(s) from start to run-time check associated with statement of line 175: 55 56function_hash_7. 57*** true . /* all conclusions proved */ 58 59 60For path(s) from start to run-time check associated with statement of line 177: 61 62function_hash_8. 63*** true . /* all conclusions proved */ 64 65 66For path(s) from assertion of line 178 to run-time check associated with 67 statement of line 177: 68 69function_hash_9. 70*** true . /* all conclusions proved */ 71 72 73For path(s) from start to run-time check associated with statement of line 177: 74 75function_hash_10. 76*** true . /* all conclusions proved */ 77 78 79For path(s) from assertion of line 178 to run-time check associated with 80 statement of line 177: 81 82function_hash_11. 83*** true . /* all conclusions proved */ 84 85 86For path(s) from start to assertion of line 178: 87 88function_hash_12. 89H1: x__index__subtype__1__first = 0 . 90H2: for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : 91 integer, x__index__subtype__1__first <= i___1 and i___1 <= 92 x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [ 93 i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) . 94H3: x__index__subtype__1__last >= 0 . 95H4: x__index__subtype__1__last <= 4294967296 . 96H5: x__index__subtype__1__first <= x__index__subtype__1__last . 97H6: mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 98 ce__1) = round_spec(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 99 := 2562383102, h3 := 271733878, h4 := 3285377520), element(x, [ 100 x__index__subtype__1__first])) . 101H7: ca__1 >= 0 . 102H8: ca__1 <= 4294967295 . 103H9: cb__1 >= 0 . 104H10: cb__1 <= 4294967295 . 105H11: cc__1 >= 0 . 106H12: cc__1 <= 4294967295 . 107H13: cd__1 >= 0 . 108H14: cd__1 <= 4294967295 . 109H15: ce__1 >= 0 . 110H16: ce__1 <= 4294967295 . 111 -> 112C1: mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 113 ce__1) = rounds(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 114 2562383102, h3 := 271733878, h4 := 3285377520), 115 x__index__subtype__1__first + 1, x) . 116 117 118For path(s) from assertion of line 178 to assertion of line 178: 119 120function_hash_13. 121H1: mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rounds( 122 mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 := 123 271733878, h4 := 3285377520), loop__1__i + 1, x) . 124H2: for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : 125 integer, x__index__subtype__1__first <= i___1 and i___1 <= 126 x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [ 127 i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) . 128H3: x__index__subtype__1__first = 0 . 129H4: loop__1__i >= 0 . 130H5: loop__1__i <= 4294967296 . 131H6: loop__1__i >= x__index__subtype__1__first . 132H7: ca >= 0 . 133H8: ca <= 4294967295 . 134H9: cb >= 0 . 135H10: cb <= 4294967295 . 136H11: cc >= 0 . 137H12: cc <= 4294967295 . 138H13: cd >= 0 . 139H14: cd <= 4294967295 . 140H15: ce >= 0 . 141H16: ce <= 4294967295 . 142H17: loop__1__i + 1 <= x__index__subtype__1__last . 143H18: mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 144 ce__1) = round_spec(mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, 145 h4 := ce), element(x, [loop__1__i + 1])) . 146H19: ca__1 >= 0 . 147H20: ca__1 <= 4294967295 . 148H21: cb__1 >= 0 . 149H22: cb__1 <= 4294967295 . 150H23: cc__1 >= 0 . 151H24: cc__1 <= 4294967295 . 152H25: cd__1 >= 0 . 153H26: cd__1 <= 4294967295 . 154H27: ce__1 >= 0 . 155H28: ce__1 <= 4294967295 . 156H29: interfaces__unsigned_32__size >= 0 . 157H30: word__size >= 0 . 158H31: chain__size >= 0 . 159H32: block_index__size >= 0 . 160H33: block_index__base__first <= block_index__base__last . 161H34: message_index__size >= 0 . 162H35: message_index__base__first <= message_index__base__last . 163H36: x__index__subtype__1__first <= x__index__subtype__1__last . 164H37: block_index__base__first <= 0 . 165H38: block_index__base__last >= 15 . 166H39: message_index__base__first <= 0 . 167H40: x__index__subtype__1__first >= 0 . 168H41: x__index__subtype__1__last >= 0 . 169H42: message_index__base__last >= 4294967296 . 170H43: x__index__subtype__1__last <= 4294967296 . 171H44: x__index__subtype__1__first <= 4294967296 . 172 -> 173C1: mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 174 ce__1) = rounds(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 175 2562383102, h3 := 271733878, h4 := 3285377520), loop__1__i + 2, x) . 176 177 178For path(s) from start to run-time check associated with statement of line 183: 179 180function_hash_14. 181*** true . /* all conclusions proved */ 182 183 184For path(s) from assertion of line 178 to run-time check associated with 185 statement of line 183: 186 187function_hash_15. 188*** true . /* all conclusions proved */ 189 190 191For path(s) from start to finish: 192 193function_hash_16. 194*** true . /* contradiction within hypotheses. */ 195 196 197 198For path(s) from assertion of line 178 to finish: 199 200function_hash_17. 201H1: mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rounds( 202 mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 := 203 271733878, h4 := 3285377520), x__index__subtype__1__last + 1, x) . 204H2: for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : 205 integer, x__index__subtype__1__first <= i___1 and i___1 <= 206 x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [ 207 i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) . 208H3: x__index__subtype__1__first = 0 . 209H4: x__index__subtype__1__last >= 0 . 210H5: x__index__subtype__1__last <= 4294967296 . 211H6: x__index__subtype__1__last >= x__index__subtype__1__first . 212H7: ca >= 0 . 213H8: ca <= 4294967295 . 214H9: cb >= 0 . 215H10: cb <= 4294967295 . 216H11: cc >= 0 . 217H12: cc <= 4294967295 . 218H13: cd >= 0 . 219H14: cd <= 4294967295 . 220H15: ce >= 0 . 221H16: ce <= 4294967295 . 222H17: interfaces__unsigned_32__size >= 0 . 223H18: word__size >= 0 . 224H19: chain__size >= 0 . 225H20: block_index__size >= 0 . 226H21: block_index__base__first <= block_index__base__last . 227H22: message_index__size >= 0 . 228H23: message_index__base__first <= message_index__base__last . 229H24: x__index__subtype__1__first <= x__index__subtype__1__last . 230H25: block_index__base__first <= 0 . 231H26: block_index__base__last >= 15 . 232H27: message_index__base__first <= 0 . 233H28: x__index__subtype__1__first >= 0 . 234H29: message_index__base__last >= 4294967296 . 235H30: x__index__subtype__1__first <= 4294967296 . 236 -> 237C1: mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rmd_hash( 238 x, x__index__subtype__1__last + 1) . 239 240 241