File ‹rmd/f.siv›
*****************************************************************************
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:19 SIMPLIFIED 29-NOV-2010, 14:30:28
SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
function RMD.F
For path(s) from start to run-time check associated with statement of line 9:
function_f_1.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 10:
function_f_2.
H1: x >= 0 .
H2: x <= 4294967295 .
H3: y >= 0 .
H4: y <= 4294967295 .
H5: z >= 0 .
H6: z <= 4294967295 .
H7: 16 <= j .
H8: j <= 31 .
H9: interfaces__unsigned_32__size >= 0 .
H10: word__size >= 0 .
H11: round_index__size >= 0 .
H12: round_index__base__first <= round_index__base__last .
H13: round_index__base__first <= 0 .
H14: round_index__base__last >= 79 .
->
C1: bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) >= 0 .
C2: bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) <= 4294967295 .
For path(s) from start to run-time check associated with statement of line 11:
function_f_3.
H1: x >= 0 .
H2: x <= 4294967295 .
H3: y >= 0 .
H4: y <= 4294967295 .
H5: z >= 0 .
H6: z <= 4294967295 .
H7: 32 <= j .
H8: j <= 47 .
H9: interfaces__unsigned_32__size >= 0 .
H10: word__size >= 0 .
H11: round_index__size >= 0 .
H12: round_index__base__first <= round_index__base__last .
H13: round_index__base__first <= 0 .
H14: round_index__base__last >= 79 .
->
C1: bit__xor(bit__or(x, 4294967295 - y), z) >= 0 .
C2: bit__xor(bit__or(x, 4294967295 - y), z) <= 4294967295 .
For path(s) from start to run-time check associated with statement of line 12:
function_f_4.
H1: x >= 0 .
H2: x <= 4294967295 .
H3: y >= 0 .
H4: y <= 4294967295 .
H5: z >= 0 .
H6: z <= 4294967295 .
H7: 48 <= j .
H8: j <= 63 .
H9: interfaces__unsigned_32__size >= 0 .
H10: word__size >= 0 .
H11: round_index__size >= 0 .
H12: round_index__base__first <= round_index__base__last .
H13: round_index__base__first <= 0 .
H14: round_index__base__last >= 79 .
->
C1: bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) >= 0 .
C2: bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) <= 4294967295 .
For path(s) from start to run-time check associated with statement of line 13:
function_f_5.
H1: j >= 0 .
H2: j <= 79 .
H3: x >= 0 .
H4: x <= 4294967295 .
H5: y >= 0 .
H6: y <= 4294967295 .
H7: z >= 0 .
H8: z <= 4294967295 .
H9: 15 < j .
H10: 31 < j .
H11: 47 < j .
H12: 63 < j .
H13: interfaces__unsigned_32__size >= 0 .
H14: word__size >= 0 .
H15: round_index__size >= 0 .
H16: round_index__base__first <= round_index__base__last .
H17: round_index__base__first <= 0 .
H18: round_index__base__last >= 79 .
->
C1: bit__xor(x, bit__or(y, 4294967295 - z)) >= 0 .
C2: bit__xor(x, bit__or(y, 4294967295 - z)) <= 4294967295 .
For path(s) from start to finish:
function_f_6.
H1: j >= 0 .
H2: x >= 0 .
H3: x <= 4294967295 .
H4: y >= 0 .
H5: y <= 4294967295 .
H6: z >= 0 .
H7: z <= 4294967295 .
H8: j <= 15 .
H9: bit__xor(x, bit__xor(y, z)) >= 0 .
H10: bit__xor(x, bit__xor(y, z)) <= 4294967295 .
H11: interfaces__unsigned_32__size >= 0 .
H12: word__size >= 0 .
H13: round_index__size >= 0 .
H14: round_index__base__first <= round_index__base__last .
H15: round_index__base__first <= 0 .
H16: round_index__base__last >= 79 .
->
C1: bit__xor(x, bit__xor(y, z)) = f_spec(j, x, y, z) .
function_f_7.
H1: x >= 0 .
H2: x <= 4294967295 .
H3: y >= 0 .
H4: y <= 4294967295 .
H5: z >= 0 .
H6: z <= 4294967295 .
H7: 16 <= j .
H8: j <= 31 .
H9: bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) >= 0 .
H10: bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) <= 4294967295 .
H11: interfaces__unsigned_32__size >= 0 .
H12: word__size >= 0 .
H13: round_index__size >= 0 .
H14: round_index__base__first <= round_index__base__last .
H15: round_index__base__first <= 0 .
H16: round_index__base__last >= 79 .
->
C1: bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) = f_spec(j, x, y, z)
.
function_f_8.
H1: x >= 0 .
H2: x <= 4294967295 .
H3: y >= 0 .
H4: y <= 4294967295 .
H5: z >= 0 .
H6: z <= 4294967295 .
H7: 32 <= j .
H8: j <= 47 .
H9: bit__xor(bit__or(x, 4294967295 - y), z) >= 0 .
H10: bit__xor(bit__or(x, 4294967295 - y), z) <= 4294967295 .
H11: interfaces__unsigned_32__size >= 0 .
H12: word__size >= 0 .
H13: round_index__size >= 0 .
H14: round_index__base__first <= round_index__base__last .
H15: round_index__base__first <= 0 .
H16: round_index__base__last >= 79 .
->
C1: bit__xor(bit__or(x, 4294967295 - y), z) = f_spec(j, x, y, z) .
function_f_9.
H1: x >= 0 .
H2: x <= 4294967295 .
H3: y >= 0 .
H4: y <= 4294967295 .
H5: z >= 0 .
H6: z <= 4294967295 .
H7: 48 <= j .
H8: j <= 63 .
H9: bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) >= 0 .
H10: bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) <= 4294967295 .
H11: interfaces__unsigned_32__size >= 0 .
H12: word__size >= 0 .
H13: round_index__size >= 0 .
H14: round_index__base__first <= round_index__base__last .
H15: round_index__base__first <= 0 .
H16: round_index__base__last >= 79 .
->
C1: bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) = f_spec(j, x, y, z)
.
function_f_10.
H1: j >= 0 .
H2: j <= 79 .
H3: x >= 0 .
H4: x <= 4294967295 .
H5: y >= 0 .
H6: y <= 4294967295 .
H7: z >= 0 .
H8: z <= 4294967295 .
H9: 15 < j .
H10: 31 < j .
H11: 47 < j .
H12: 63 < j .
H13: bit__xor(x, bit__or(y, 4294967295 - z)) >= 0 .
H14: bit__xor(x, bit__or(y, 4294967295 - z)) <= 4294967295 .
H15: interfaces__unsigned_32__size >= 0 .
H16: word__size >= 0 .
H17: round_index__size >= 0 .
H18: round_index__base__first <= round_index__base__last .
H19: round_index__base__first <= 0 .
H20: round_index__base__last >= 79 .
->
C1: bit__xor(x, bit__or(y, 4294967295 - z)) = f_spec(j, x, y, z) .