Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
s_l.siv
Sprache: Unknown
Spracherkennung für: .siv vermutete Sprache: Hlasm {Hlasm[736] BAT[806] Abap[926]} [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:29
SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
function RMD.S_L
For path(s) from start to run-time check associated with statement of line 87:
function_s_l_1.
*** true . /* all conclusions proved */
For path(s) from start to finish:
function_s_l_2.
H1: j >= 0 .
H2: j <= 79 .
H3: integer__size >= 0 .
H4: round_index__size >= 0 .
H5: round_index__base__first <= round_index__base__last .
H6: rotate_amount__size >= 0 .
H7: round_index__base__first <= 0 .
H8: round_index__base__last >= 79 .
->
C1: element(mk__rotate_definition([0] := 11, [1] := 14, [2] := 15, [3] :=
12, [4] := 5, [5] := 8, [6] := 7, [7] := 9, [8] := 11, [9] := 13, [10]
:= 14, [11] := 15, [12] := 6, [13] := 7, [14] := 9, [15] := 8, [16]
:= 7, [17] := 6, [18] := 8, [19] := 13, [20] := 11, [21] := 9, [22]
:= 7, [23] := 15, [24] := 7, [25] := 12, [26] := 15, [27] := 9, [28]
:= 11, [29] := 7, [30] := 13, [31] := 12, [32] := 11, [33] := 13, [34]
:= 6, [35] := 7, [36] := 14, [37] := 9, [38] := 13, [39] := 15, [40]
:= 14, [41] := 8, [42] := 13, [43] := 6, [44] := 5, [45] := 12, [46]
:= 7, [47] := 5, [48] := 11, [49] := 12, [50] := 14, [51] := 15, [52]
:= 14, [53] := 15, [54] := 9, [55] := 8, [56] := 9, [57] := 14, [58]
:= 5, [59] := 6, [60] := 8, [61] := 6, [62] := 5, [63] := 12, [64] :=
9, [65] := 15, [66] := 5, [67] := 11, [68] := 6, [69] := 8, [70] :=
13, [71] := 12, [72] := 5, [73] := 12, [74] := 13, [75] := 14, [76]
:= 11, [77] := 8, [78] := 5, [79] := 6), [j]) = s_l_spec(j) .
C2: element(mk__rotate_definition([0] := 11, [1] := 14, [2] := 15, [3] :=
12, [4] := 5, [5] := 8, [6] := 7, [7] := 9, [8] := 11, [9] := 13, [10]
:= 14, [11] := 15, [12] := 6, [13] := 7, [14] := 9, [15] := 8, [16]
:= 7, [17] := 6, [18] := 8, [19] := 13, [20] := 11, [21] := 9, [22]
:= 7, [23] := 15, [24] := 7, [25] := 12, [26] := 15, [27] := 9, [28]
:= 11, [29] := 7, [30] := 13, [31] := 12, [32] := 11, [33] := 13, [34]
:= 6, [35] := 7, [36] := 14, [37] := 9, [38] := 13, [39] := 15, [40]
:= 14, [41] := 8, [42] := 13, [43] := 6, [44] := 5, [45] := 12, [46]
:= 7, [47] := 5, [48] := 11, [49] := 12, [50] := 14, [51] := 15, [52]
:= 14, [53] := 15, [54] := 9, [55] := 8, [56] := 9, [57] := 14, [58]
:= 5, [59] := 6, [60] := 8, [61] := 6, [62] := 5, [63] := 12, [64] :=
9, [65] := 15, [66] := 5, [67] := 11, [68] := 6, [69] := 8, [70] :=
13, [71] := 12, [72] := 5, [73] := 12, [74] := 13, [75] := 14, [76]
:= 11, [77] := 8, [78] := 5, [79] := 6), [j]) >= 0 .
C3: element(mk__rotate_definition([0] := 11, [1] := 14, [2] := 15, [3] :=
12, [4] := 5, [5] := 8, [6] := 7, [7] := 9, [8] := 11, [9] := 13, [10]
:= 14, [11] := 15, [12] := 6, [13] := 7, [14] := 9, [15] := 8, [16]
:= 7, [17] := 6, [18] := 8, [19] := 13, [20] := 11, [21] := 9, [22]
:= 7, [23] := 15, [24] := 7, [25] := 12, [26] := 15, [27] := 9, [28]
:= 11, [29] := 7, [30] := 13, [31] := 12, [32] := 11, [33] := 13, [34]
:= 6, [35] := 7, [36] := 14, [37] := 9, [38] := 13, [39] := 15, [40]
:= 14, [41] := 8, [42] := 13, [43] := 6, [44] := 5, [45] := 12, [46]
:= 7, [47] := 5, [48] := 11, [49] := 12, [50] := 14, [51] := 15, [52]
:= 14, [53] := 15, [54] := 9, [55] := 8, [56] := 9, [57] := 14, [58]
:= 5, [59] := 6, [60] := 8, [61] := 6, [62] := 5, [63] := 12, [64] :=
9, [65] := 15, [66] := 5, [67] := 11, [68] := 6, [69] := 8, [70] :=
13, [71] := 12, [72] := 5, [73] := 12, [74] := 13, [75] := 14, [76]
:= 11, [77] := 8, [78] := 5, [79] := 6), [j]) <= 15 .
[ Dauer der Verarbeitung: 0.107 Sekunden
]
|
|
