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:28 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.F 14 15 16 17 18For path(s) from start to run-time check associated with statement of line 9: 19 20function_f_1. 21*** true . /* all conclusions proved */ 22 23 24For path(s) from start to run-time check associated with statement of line 10: 25 26function_f_2. 27H1: x >= 0 . 28H2: x <= 4294967295 . 29H3: y >= 0 . 30H4: y <= 4294967295 . 31H5: z >= 0 . 32H6: z <= 4294967295 . 33H7: 16 <= j . 34H8: j <= 31 . 35H9: interfaces__unsigned_32__size >= 0 . 36H10: word__size >= 0 . 37H11: round_index__size >= 0 . 38H12: round_index__base__first <= round_index__base__last . 39H13: round_index__base__first <= 0 . 40H14: round_index__base__last >= 79 . 41 -> 42C1: bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) >= 0 . 43C2: bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) <= 4294967295 . 44 45 46For path(s) from start to run-time check associated with statement of line 11: 47 48function_f_3. 49H1: x >= 0 . 50H2: x <= 4294967295 . 51H3: y >= 0 . 52H4: y <= 4294967295 . 53H5: z >= 0 . 54H6: z <= 4294967295 . 55H7: 32 <= j . 56H8: j <= 47 . 57H9: interfaces__unsigned_32__size >= 0 . 58H10: word__size >= 0 . 59H11: round_index__size >= 0 . 60H12: round_index__base__first <= round_index__base__last . 61H13: round_index__base__first <= 0 . 62H14: round_index__base__last >= 79 . 63 -> 64C1: bit__xor(bit__or(x, 4294967295 - y), z) >= 0 . 65C2: bit__xor(bit__or(x, 4294967295 - y), z) <= 4294967295 . 66 67 68For path(s) from start to run-time check associated with statement of line 12: 69 70function_f_4. 71H1: x >= 0 . 72H2: x <= 4294967295 . 73H3: y >= 0 . 74H4: y <= 4294967295 . 75H5: z >= 0 . 76H6: z <= 4294967295 . 77H7: 48 <= j . 78H8: j <= 63 . 79H9: interfaces__unsigned_32__size >= 0 . 80H10: word__size >= 0 . 81H11: round_index__size >= 0 . 82H12: round_index__base__first <= round_index__base__last . 83H13: round_index__base__first <= 0 . 84H14: round_index__base__last >= 79 . 85 -> 86C1: bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) >= 0 . 87C2: bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) <= 4294967295 . 88 89 90For path(s) from start to run-time check associated with statement of line 13: 91 92function_f_5. 93H1: j >= 0 . 94H2: j <= 79 . 95H3: x >= 0 . 96H4: x <= 4294967295 . 97H5: y >= 0 . 98H6: y <= 4294967295 . 99H7: z >= 0 . 100H8: z <= 4294967295 . 101H9: 15 < j . 102H10: 31 < j . 103H11: 47 < j . 104H12: 63 < j . 105H13: interfaces__unsigned_32__size >= 0 . 106H14: word__size >= 0 . 107H15: round_index__size >= 0 . 108H16: round_index__base__first <= round_index__base__last . 109H17: round_index__base__first <= 0 . 110H18: round_index__base__last >= 79 . 111 -> 112C1: bit__xor(x, bit__or(y, 4294967295 - z)) >= 0 . 113C2: bit__xor(x, bit__or(y, 4294967295 - z)) <= 4294967295 . 114 115 116For path(s) from start to finish: 117 118function_f_6. 119H1: j >= 0 . 120H2: x >= 0 . 121H3: x <= 4294967295 . 122H4: y >= 0 . 123H5: y <= 4294967295 . 124H6: z >= 0 . 125H7: z <= 4294967295 . 126H8: j <= 15 . 127H9: bit__xor(x, bit__xor(y, z)) >= 0 . 128H10: bit__xor(x, bit__xor(y, z)) <= 4294967295 . 129H11: interfaces__unsigned_32__size >= 0 . 130H12: word__size >= 0 . 131H13: round_index__size >= 0 . 132H14: round_index__base__first <= round_index__base__last . 133H15: round_index__base__first <= 0 . 134H16: round_index__base__last >= 79 . 135 -> 136C1: bit__xor(x, bit__xor(y, z)) = f_spec(j, x, y, z) . 137 138 139function_f_7. 140H1: x >= 0 . 141H2: x <= 4294967295 . 142H3: y >= 0 . 143H4: y <= 4294967295 . 144H5: z >= 0 . 145H6: z <= 4294967295 . 146H7: 16 <= j . 147H8: j <= 31 . 148H9: bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) >= 0 . 149H10: bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) <= 4294967295 . 150H11: interfaces__unsigned_32__size >= 0 . 151H12: word__size >= 0 . 152H13: round_index__size >= 0 . 153H14: round_index__base__first <= round_index__base__last . 154H15: round_index__base__first <= 0 . 155H16: round_index__base__last >= 79 . 156 -> 157C1: bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) = f_spec(j, x, y, z) 158 . 159 160 161function_f_8. 162H1: x >= 0 . 163H2: x <= 4294967295 . 164H3: y >= 0 . 165H4: y <= 4294967295 . 166H5: z >= 0 . 167H6: z <= 4294967295 . 168H7: 32 <= j . 169H8: j <= 47 . 170H9: bit__xor(bit__or(x, 4294967295 - y), z) >= 0 . 171H10: bit__xor(bit__or(x, 4294967295 - y), z) <= 4294967295 . 172H11: interfaces__unsigned_32__size >= 0 . 173H12: word__size >= 0 . 174H13: round_index__size >= 0 . 175H14: round_index__base__first <= round_index__base__last . 176H15: round_index__base__first <= 0 . 177H16: round_index__base__last >= 79 . 178 -> 179C1: bit__xor(bit__or(x, 4294967295 - y), z) = f_spec(j, x, y, z) . 180 181 182function_f_9. 183H1: x >= 0 . 184H2: x <= 4294967295 . 185H3: y >= 0 . 186H4: y <= 4294967295 . 187H5: z >= 0 . 188H6: z <= 4294967295 . 189H7: 48 <= j . 190H8: j <= 63 . 191H9: bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) >= 0 . 192H10: bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) <= 4294967295 . 193H11: interfaces__unsigned_32__size >= 0 . 194H12: word__size >= 0 . 195H13: round_index__size >= 0 . 196H14: round_index__base__first <= round_index__base__last . 197H15: round_index__base__first <= 0 . 198H16: round_index__base__last >= 79 . 199 -> 200C1: bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) = f_spec(j, x, y, z) 201 . 202 203 204function_f_10. 205H1: j >= 0 . 206H2: j <= 79 . 207H3: x >= 0 . 208H4: x <= 4294967295 . 209H5: y >= 0 . 210H6: y <= 4294967295 . 211H7: z >= 0 . 212H8: z <= 4294967295 . 213H9: 15 < j . 214H10: 31 < j . 215H11: 47 < j . 216H12: 63 < j . 217H13: bit__xor(x, bit__or(y, 4294967295 - z)) >= 0 . 218H14: bit__xor(x, bit__or(y, 4294967295 - z)) <= 4294967295 . 219H15: interfaces__unsigned_32__size >= 0 . 220H16: word__size >= 0 . 221H17: round_index__size >= 0 . 222H18: round_index__base__first <= round_index__base__last . 223H19: round_index__base__first <= 0 . 224H20: round_index__base__last >= 79 . 225 -> 226C1: bit__xor(x, bit__or(y, 4294967295 - z)) = f_spec(j, x, y, z) . 227 228 229