Spracherkennung für: .siv vermutete Sprache: BAT {BAT[109] Ada[224] Abap[231]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
*****************************************************************************
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.K_L
For path(s) from start to run-time check associated with statement of line 24:
function_k_l_1.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 25:
function_k_l_2.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 26:
function_k_l_3.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 27:
function_k_l_4.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 28:
function_k_l_5.
*** true . /* all conclusions proved */
For path(s) from start to finish:
function_k_l_6.
H1: j >= 0 .
H2: j <= 15 .
H3: interfaces__unsigned_32__size >= 0 .
H4: word__size >= 0 .
H5: round_index__size >= 0 .
H6: round_index__base__first <= round_index__base__last .
H7: round_index__base__first <= 0 .
H8: round_index__base__last >= 79 .
->
C1: 0 = k_l_spec(j) .
function_k_l_7.
H1: 16 <= j .
H2: j <= 31 .
H3: interfaces__unsigned_32__size >= 0 .
H4: word__size >= 0 .
H5: round_index__size >= 0 .
H6: round_index__base__first <= round_index__base__last .
H7: round_index__base__first <= 0 .
H8: round_index__base__last >= 79 .
->
C1: 1518500249 = k_l_spec(j) .
function_k_l_8.
H1: 32 <= j .
H2: j <= 47 .
H3: interfaces__unsigned_32__size >= 0 .
H4: word__size >= 0 .
H5: round_index__size >= 0 .
H6: round_index__base__first <= round_index__base__last .
H7: round_index__base__first <= 0 .
H8: round_index__base__last >= 79 .
->
C1: 1859775393 = k_l_spec(j) .
function_k_l_9.
H1: 48 <= j .
H2: j <= 63 .
H3: interfaces__unsigned_32__size >= 0 .
H4: word__size >= 0 .
H5: round_index__size >= 0 .
H6: round_index__base__first <= round_index__base__last .
H7: round_index__base__first <= 0 .
H8: round_index__base__last >= 79 .
->
C1: 2400959708 = k_l_spec(j) .
function_k_l_10.
H1: j >= 0 .
H2: j <= 79 .
H3: 15 < j .
H4: 31 < j .
H5: 47 < j .
H6: 63 < j .
H7: interfaces__unsigned_32__size >= 0 .
H8: word__size >= 0 .
H9: round_index__size >= 0 .
H10: round_index__base__first <= round_index__base__last .
H11: round_index__base__first <= 0 .
H12: round_index__base__last >= 79 .
->
C1: 2840853838 = k_l_spec(j) .
[ Dauer der Verarbeitung: 2.35 Sekunden
]