***************************************************************************** Semantic Analysis of SPARK Text Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039 Copyright (C) 2010 Altran Praxis Limited, Bath, U.K. ***************************************************************************** CREATED 29-NOV-2010, 14:30:20 SIMPLIFIED 29-NOV-2010, 14:30:20 SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039 Copyright (C) 2010 Altran Praxis Limited, Bath, U.K. function RMD.Hash For path(s) from start to run-time check associated with statement of line 170: function_hash_1. *** true . /* all conclusions proved */ For path(s) from start to run-time check associated with statement of line 171: function_hash_2. *** true . /* all conclusions proved */ For path(s) from start to run-time check associated with statement of line 172: function_hash_3. *** true . /* all conclusions proved */ For path(s) from start to run-time check associated with statement of line 173: function_hash_4. *** true . /* all conclusions proved */ For path(s) from start to run-time check associated with statement of line 174: function_hash_5. *** true . /* all conclusions proved */ For path(s) from start to run-time check associated with statement of line 175: function_hash_6. *** true . /* all conclusions proved */ For path(s) from start to run-time check associated with statement of line 175: function_hash_7. *** true . /* all conclusions proved */ For path(s) from start to run-time check associated with statement of line 177: function_hash_8. *** true . /* all conclusions proved */ For path(s) from assertion of line 178 to run-time check associated with statement of line 177: function_hash_9. *** true . /* all conclusions proved */ For path(s) from start to run-time check associated with statement of line 177: function_hash_10. *** true . /* all conclusions proved */ For path(s) from assertion of line 178 to run-time check associated with statement of line 177: function_hash_11. *** true . /* all conclusions proved */ For path(s) from start to assertion of line 178: function_hash_12. H1: x__index__subtype__1__first = 0 . H2: for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : integer, x__index__subtype__1__first <= i___1 and i___1 <= x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [ i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) . H3: x__index__subtype__1__last >= 0 . H4: x__index__subtype__1__last <= 4294967296 . H5: x__index__subtype__1__first <= x__index__subtype__1__last . H6: mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := ce__1) = round_spec(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 := 271733878, h4 := 3285377520), element(x, [ x__index__subtype__1__first])) . H7: ca__1 >= 0 . H8: ca__1 <= 4294967295 . H9: cb__1 >= 0 . H10: cb__1 <= 4294967295 . H11: cc__1 >= 0 . H12: cc__1 <= 4294967295 . H13: cd__1 >= 0 . H14: cd__1 <= 4294967295 . H15: ce__1 >= 0 . H16: ce__1 <= 4294967295 . -> C1: mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := ce__1) = rounds(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 := 271733878, h4 := 3285377520), x__index__subtype__1__first + 1, x) . For path(s) from assertion of line 178 to assertion of line 178: function_hash_13. H1: mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rounds( mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 := 271733878, h4 := 3285377520), loop__1__i + 1, x) . H2: for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : integer, x__index__subtype__1__first <= i___1 and i___1 <= x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [ i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) . H3: x__index__subtype__1__first = 0 . H4: loop__1__i >= 0 . H5: loop__1__i <= 4294967296 . H6: loop__1__i >= x__index__subtype__1__first . H7: ca >= 0 . H8: ca <= 4294967295 . H9: cb >= 0 . H10: cb <= 4294967295 . H11: cc >= 0 . H12: cc <= 4294967295 . H13: cd >= 0 . H14: cd <= 4294967295 . H15: ce >= 0 . H16: ce <= 4294967295 . H17: loop__1__i + 1 <= x__index__subtype__1__last . H18: mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := ce__1) = round_spec(mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce), element(x, [loop__1__i + 1])) . H19: ca__1 >= 0 . H20: ca__1 <= 4294967295 . H21: cb__1 >= 0 . H22: cb__1 <= 4294967295 . H23: cc__1 >= 0 . H24: cc__1 <= 4294967295 . H25: cd__1 >= 0 . H26: cd__1 <= 4294967295 . H27: ce__1 >= 0 . H28: ce__1 <= 4294967295 . H29: interfaces__unsigned_32__size >= 0 . H30: word__size >= 0 . H31: chain__size >= 0 . H32: block_index__size >= 0 . H33: block_index__base__first <= block_index__base__last . H34: message_index__size >= 0 . H35: message_index__base__first <= message_index__base__last . H36: x__index__subtype__1__first <= x__index__subtype__1__last . H37: block_index__base__first <= 0 . H38: block_index__base__last >= 15 . H39: message_index__base__first <= 0 . H40: x__index__subtype__1__first >= 0 . H41: x__index__subtype__1__last >= 0 . H42: message_index__base__last >= 4294967296 . H43: x__index__subtype__1__last <= 4294967296 . H44: x__index__subtype__1__first <= 4294967296 . -> C1: mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := ce__1) = rounds(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 := 271733878, h4 := 3285377520), loop__1__i + 2, x) . For path(s) from start to run-time check associated with statement of line 183: function_hash_14. *** true . /* all conclusions proved */ For path(s) from assertion of line 178 to run-time check associated with statement of line 183: function_hash_15. *** true . /* all conclusions proved */ For path(s) from start to finish: function_hash_16. *** true . /* contradiction within hypotheses. */ For path(s) from assertion of line 178 to finish: function_hash_17. H1: mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rounds( mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 := 271733878, h4 := 3285377520), x__index__subtype__1__last + 1, x) . H2: for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : integer, x__index__subtype__1__first <= i___1 and i___1 <= x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [ i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) . H3: x__index__subtype__1__first = 0 . H4: x__index__subtype__1__last >= 0 . H5: x__index__subtype__1__last <= 4294967296 . H6: x__index__subtype__1__last >= x__index__subtype__1__first . H7: ca >= 0 . H8: ca <= 4294967295 . H9: cb >= 0 . H10: cb <= 4294967295 . H11: cc >= 0 . H12: cc <= 4294967295 . H13: cd >= 0 . H14: cd <= 4294967295 . H15: ce >= 0 . H16: ce <= 4294967295 . H17: interfaces__unsigned_32__size >= 0 . H18: word__size >= 0 . H19: chain__size >= 0 . H20: block_index__size >= 0 . H21: block_index__base__first <= block_index__base__last . H22: message_index__size >= 0 . H23: message_index__base__first <= message_index__base__last . H24: x__index__subtype__1__first <= x__index__subtype__1__last . H25: block_index__base__first <= 0 . H26: block_index__base__last >= 15 . H27: message_index__base__first <= 0 . H28: x__index__subtype__1__first >= 0 . H29: message_index__base__last >= 4294967296 . H30: x__index__subtype__1__first <= 4294967296 . -> C1: mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rmd_hash( x, x__index__subtype__1__last + 1) .