Package de.uka.ilkd.key.nparser

Failed tests

• TestTacletEquality. [1532] postdecrement_array, postdecrement_array { \find(#allmodal ( (modal operator))\[{ .. #e[#e0]--; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #v[#v0] = (#typeof( #e[#e0]);) (#v[#v0] - 1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1534] postdecrement_assignment_array, postdecrement_assignment_array { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e[#e0]--; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#lhs0 (program LeftHandSide))), \new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #lhs0 (program LeftHandSide)); #v1 = #…
• TestTacletEquality. [1538] postincrement_array, postincrement_array { \find(#allmodal ( (modal operator))\[{ .. #e[#e0]++; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #v[#v0] = (#typeof( #e[#e0]);) (#v[#v0] + 1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1540] postincrement_assignment_array, postincrement_assignment_array { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e[#e0]++; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#lhs0 (program LeftHandSide))), \new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #lhs0 (program LeftHandSide)); #v1 = #…
• TestTacletEquality. [1576] predecrement_array, predecrement_array { \find(#allmodal ( (modal operator))\[{ .. --#e[#e0]; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #v[#v0] = (#typeof( #e[#e0]);) (#v[#v0] - 1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1578] predecrement_assignment_array, predecrement_assignment_array { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = --#e[#e0]; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #v[#v0] = (#typeof( #e[#e0]);) (#v[#v0] - 1); #lhs0 = #v[#v0]; ... }\] (post)) \heuristics(simplify_expression) Ch…
• TestTacletEquality. [1582] preincrement_array, preincrement_array { \find(#allmodal ( (modal operator))\[{ .. ++#e[#e0]; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #v[#v0] = (#typeof( #e[#e0]);) (#v[#v0] + 1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1584] preincrement_assignment_array, preincrement_assignment_array { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = ++#e[#e0]; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #v[#v0] = (#typeof( #e[#e0]);) (#v[#v0] + 1); #lhs0 = #v[#v0]; ... }\] (post)) \heuristics(simplify_expression) Ch…
• TestTacletEquality. [423] compound_assignment_op_and_array, compound_assignment_op_and_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] &= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] & #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules…
• TestTacletEquality. [426] compound_assignment_op_div_array, compound_assignment_op_div_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] /= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] / #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules…
• TestTacletEquality. [429] compound_assignment_op_minus_array, compound_assignment_op_minus_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] -= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] - #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRul…
• TestTacletEquality. [432] compound_assignment_op_mod_array, compound_assignment_op_mod_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] %= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] % #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules…
• TestTacletEquality. [435] compound_assignment_op_mul_array, compound_assignment_op_mul_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] *= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] * #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules…
• TestTacletEquality. [438] compound_assignment_op_or_array, compound_assignment_op_or_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] |= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] | #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:…
• TestTacletEquality. [441] compound_assignment_op_plus_array, compound_assignment_op_plus_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] += #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] + #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRule…
• TestTacletEquality. [444] compound_assignment_op_shiftleft_array, compound_assignment_op_shiftleft_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] <<= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] << #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: prog…
• TestTacletEquality. [447] compound_assignment_op_shiftright_array, compound_assignment_op_shiftright_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] >>= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] >> #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: pro…
• TestTacletEquality. [450] compound_assignment_op_unsigned_shiftright_array, compound_assignment_op_unsigned_shiftright_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] >>>= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] >>> #e1); ... }\] (post)) \heuristics(simplify_prog) C…
• TestTacletEquality. [453] compound_assignment_op_xor_array, compound_assignment_op_xor_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] ^= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] ^ #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules…
• TestTacletEquality. [818] eval_order_iterated_assignments_10_0, eval_order_iterated_assignments_10_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] |= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] | #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simp…
• TestTacletEquality. [820] eval_order_iterated_assignments_11_0, eval_order_iterated_assignments_11_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] ^= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] ^ #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simp…
• TestTacletEquality. [822] eval_order_iterated_assignments_1_0, eval_order_iterated_assignments_1_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] *= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] * #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simpl…
• TestTacletEquality. [824] eval_order_iterated_assignments_2_0, eval_order_iterated_assignments_2_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] /= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] / #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simpl…
• TestTacletEquality. [826] eval_order_iterated_assignments_3_0, eval_order_iterated_assignments_3_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] %= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] % #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simpl…
• TestTacletEquality. [828] eval_order_iterated_assignments_4_0, eval_order_iterated_assignments_4_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] += #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] + #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simpl…
• TestTacletEquality. [830] eval_order_iterated_assignments_5_0, eval_order_iterated_assignments_5_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] -= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] - #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simpl…
• TestTacletEquality. [832] eval_order_iterated_assignments_6_0, eval_order_iterated_assignments_6_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] <<= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] << #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(sim…
• TestTacletEquality. [834] eval_order_iterated_assignments_7_0, eval_order_iterated_assignments_7_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] >>= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] >> #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(sim…
• TestTacletEquality. [836] eval_order_iterated_assignments_8_0, eval_order_iterated_assignments_8_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] >>>= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] >>> #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(s…
• TestTacletEquality. [838] eval_order_iterated_assignments_9_0, eval_order_iterated_assignments_9_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] &= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] & #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simpl…

Classes