Test Summary

Failed tests

• TestRecoder2KeY. testJBlocks()
• TestTacletEquality. [1002] identityCastDouble, identityCastDouble { \find(#normalassign ( (modal operator))\[{ .. #loc=(double)#seDouble; ... }\] (post)) \replacewith(#normalassign ( (modal operator))\[{ .. #loc=#seDouble; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1003] identityCastFloat, identityCastFloat { \find(#normalassign ( (modal operator))\[{ .. #loc=(float)#seFloat; ... }\] (post)) \replacewith(#normalassign ( (modal operator))\[{ .. #loc=#seFloat; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1004] if, if { \find(#allmodal ( (modal operator))\[{ .. if (#se) #s0 ... }\] (post)) \replacewith(if-then-else(equals(#se,TRUE),#allmodal ( (modal operator))\[{ .. #s0 ... }\] (post),#allmodal(post))) Choices: programRules:Java}
• TestTacletEquality. [1005] ifElse, ifElse { \find(#allmodal ( (modal operator))\[{ .. if (#se) #s0 else #s1 ... }\] (post)) \replacewith(if-then-else(equals(#se,TRUE),#allmodal ( (modal operator))\[{ .. #s0 ... }\] (post),#allmodal ( (modal operator))\[{ .. #s1 ... }\] (post))) Choices: programRules:Java}
• TestTacletEquality. [1006] ifElseFalse, ifElseFalse { \assumes ([equals(#se,FALSE)]==>[]) \find(==>#allmodal ( (modal operator))\[{ .. if (#se) #s0 else #s1 ... }\] (post)) \replacewith([]==>[#allmodal ( (modal operator))\[{ .. #s1 ... }\] (post)]) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1007] ifElseSkipElse, ifElseSkipElse { \find(#allmodal ( (modal operator))\[{ .. #loc=true;if (#loc) #s0 else #s1 ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #loc=true;#s0 ... }\] (post)) \heuristics(simplify) Choices: programRules:Java}
• TestTacletEquality. [1008] ifElseSkipElseConditionInBlock, ifElseSkipElseConditionInBlock { \find(#allmodal ( (modal operator))\[{ .. {#loc=true;}if (#loc) #s0 else #s1 ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#loc=true;}#s0 ... }\] (post)) \heuristics(simplify) Choices: programRules:Java}
• TestTacletEquality. [1009] ifElseSkipThen, ifElseSkipThen { \find(#allmodal ( (modal operator))\[{ .. #loc=false;if (#loc) #s0 else #s1 ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #loc=false;#s1 ... }\] (post)) \heuristics(simplify) Choices: programRules:Java}
• TestTacletEquality. [1010] ifElseSkipThenConditionInBlock, ifElseSkipThenConditionInBlock { \find(#allmodal ( (modal operator))\[{ .. {#loc=false;}if (#loc) #s0 else #s1 ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#loc=false;}#s1 ... }\] (post)) \heuristics(simplify) Choices: programRules:Java}
• TestTacletEquality. [1011] ifElseSplit, ifElseSplit { \find(==>#allmodal ( (modal operator))\[{ .. if (#se) #s0 else #s1 ... }\] (post)) \add [equals(#se,FALSE)]==>[] \replacewith([]==>[#allmodal ( (modal operator))\[{ .. #s1 ... }\] (post)]) ; \add [equals(#se,TRUE)]==>[] \replacewith([]==>[#allmodal ( (modal operator))\[{ .. #s0 ... }\] (post)]) \heuristics(split_if) Choices: programRules:Java}
• TestTacletEquality. [1012] ifElseSplitLeft, ifElseSplitLeft { \find(#allmodal ( (modal operator))\[{ .. if (#se) #s0 else #s1 ... }\] (post)==>) \add [equals(#se,FALSE)]==>[] \replacewith([#allmodal ( (modal operator))\[{ .. #s1 ... }\] (post)]==>[]) ; \add [equals(#se,TRUE)]==>[] \replacewith([#allmodal ( (modal operator))\[{ .. #s0 ... }\] (post)]==>[]) \heuristics(split_if) Choices: programRules:Java}
• TestTacletEquality. [1013] ifElseTrue, ifElseTrue { \assumes ([equals(#se,TRUE)]==>[]) \find(==>#allmodal ( (modal operator))\[{ .. if (#se) #s0 else #s1 ... }\] (post)) \replacewith([]==>[#allmodal ( (modal operator))\[{ .. #s0 ... }\] (post)]) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1014] ifElseUnfold, ifElseUnfold { \find(#allmodal ( (modal operator))\[{ .. if (#nse) #s0 else #s1 ... }\] (post)) \varcond(\new(#boolv (program Variable), (type, sort): (boolean,boolean))) \replacewith(#allmodal ( (modal operator))\[{ .. boolean #boolv;#boolv=#nse;if (#boolv) #s0 else { #s1 } ... }\] (post)) \heuristics(simplify_autoname) Choices: programRules:Java}
• TestTacletEquality. [1015] ifEnterThen, ifEnterThen { \find(#allmodal ( (modal operator))\[{ .. #loc=true;if (#loc) #s0 ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #loc=true;#s0 ... }\] (post)) \heuristics(simplify) Choices: programRules:Java}
• TestTacletEquality. [1016] ifEnterThenConditionInBlock, ifEnterThenConditionInBlock { \find(#allmodal ( (modal operator))\[{ .. {#loc=true;}if (#loc) #s0 ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#loc=true;}#s0 ... }\] (post)) \heuristics(simplify) Choices: programRules:Java}
• TestTacletEquality. [1038] ifFalse, ifFalse { \assumes ([equals(#se,FALSE)]==>[]) \find(==>#allmodal ( (modal operator))\[{ .. if (#se) #s0 ... }\] (post)) \replacewith([]==>[#allmodal(post)]) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1039] ifSkipThen, ifSkipThen { \find(#allmodal ( (modal operator))\[{ .. #loc=false;if (#loc) #s0 ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #loc=false; ... }\] (post)) \heuristics(simplify) Choices: programRules:Java}
• TestTacletEquality. [1040] ifSkipThenConditionInBlock, ifSkipThenConditionInBlock { \find(#allmodal ( (modal operator))\[{ .. {#loc=false;}if (#loc) #s0 ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#loc=false;} ... }\] (post)) \heuristics(simplify) Choices: programRules:Java}
• TestTacletEquality. [1041] ifSplit, ifSplit { \find(==>#allmodal ( (modal operator))\[{ .. if (#se) #s0 ... }\] (post)) \add [equals(#se,FALSE)]==>[] \replacewith([]==>[#allmodal(post)]) ; \add [equals(#se,TRUE)]==>[] \replacewith([]==>[#allmodal ( (modal operator))\[{ .. #s0 ... }\] (post)]) \heuristics(split_if) Choices: programRules:Java}
• TestTacletEquality. [1042] ifSplitLeft, ifSplitLeft { \find(#allmodal ( (modal operator))\[{ .. if (#se) #s0 ... }\] (post)==>) \add [equals(#se,FALSE)]==>[] \replacewith([#allmodal(post)]==>[]) ; \add [equals(#se,TRUE)]==>[] \replacewith([#allmodal ( (modal operator))\[{ .. #s0 ... }\] (post)]==>[]) \heuristics(split_if) Choices: programRules:Java}
• TestTacletEquality. [1043] ifTrue, ifTrue { \assumes ([equals(#se,TRUE)]==>[]) \find(==>#allmodal ( (modal operator))\[{ .. if (#se) #s0 ... }\] (post)) \replacewith([]==>[#allmodal ( (modal operator))\[{ .. #s0 ... }\] (post)]) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1044] ifUnfold, ifUnfold { \find(#allmodal ( (modal operator))\[{ .. if (#nse) #s0 ... }\] (post)) \varcond(\new(#boolv (program Variable), (type, sort): (boolean,boolean))) \replacewith(#allmodal ( (modal operator))\[{ .. boolean #boolv;#boolv=#nse;if (#boolv) #s0 ... }\] (post)) \heuristics(simplify_autoname) Choices: programRules:Java}
• TestTacletEquality. [10] activeUseBitwiseOr, activeUseBitwiseOr { \find(#allmodal ( (modal operator))\[{ .. #sv=#left|#right; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = #left|#right;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [1165] inequality_comparison_new, inequality_comparison_new { \find(#allmodal ( (modal operator))\[{ .. #lhs=#senf0!=#senf1; ... }\] (post)) \replacewith(if-then-else(not(equals(#senf0,#senf1)),#allmodal ( (modal operator))\[{ .. #lhs=true; ... }\] (post),#allmodal ( (modal operator))\[{ .. #lhs=false; ... }\] (post))) \heuristics(split_if, simplify_prog, obsolete) Choices: programRules:Java}
• TestTacletEquality. [1166] inequality_comparison_simple, inequality_comparison_simple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#senf0!=#senf1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(equals(#senf0,#senf1),FALSE,TRUE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1167] inequality_comparison_simple_double, inequality_comparison_simple_double { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seDouble0!=#seDouble1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(eqDouble(#seDouble0,#seDouble1),FALSE,TRUE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1168] inequality_comparison_simple_float, inequality_comparison_simple_float { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seFloat0!=#seFloat1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(eqFloat(#seFloat0,#seFloat1),FALSE,TRUE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1179] instanceCreation, instanceCreation { \find(#allmodal ( (modal operator))\[{ .. #n ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#n (program SimpleInstanceCreation)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#v0) #v0 = create-object(#n);constructor-call(#n)post-work(#v0) ... }\] (post)) \heuristics(method_expand) Choices: programRules:Java}
• TestTacletEquality. [1180] instanceCreationAssignment, instanceCreationAssignment { \find(#normal ( (modal operator))\[{ .. #lhs=#n; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#lhs (program LeftHandSide)))) \replacewith(#normal ( (modal operator))\[{ .. #typeof(#v0) #v0 = create-object(#n);constructor-call(#n)post-work(#v0)#lhs=#v0; ... }\] (post)) \heuristics(method_expand) Choices: programRules:Java}
• TestTacletEquality. [1181] instanceCreationAssignmentUnfoldArguments, instanceCreationAssignmentUnfoldArguments { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nsn; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #evaluate-arguments(#lhs=#nsn;) ... }\] (post)) \heuristics(simplify_autoname) Choices: programRules:Java}
• TestTacletEquality. [1182] instanceCreationUnfoldArguments, instanceCreationUnfoldArguments { \find(#allmodal ( (modal operator))\[{ .. #nsn ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #evaluate-arguments(#nsn) ... }\] (post)) \heuristics(simplify_autoname) Choices: programRules:Java}
• TestTacletEquality. [1183] instanceof_eval, instanceof_eval { \find(#allmodal ( (modal operator))\[{ .. #v=#nse instanceof #t; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v0 = #nse;#v=#v0 instanceof #t; ... }\] (post)) \heuristics(simplify_autoname) Choices: programRules:Java}
• TestTacletEquality. [1194] intLongToFloatAddition1, intLongToFloatAddition1 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong+#seFloat; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(float::cast(#seLong),#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [1195] intToFloatAddition, intToFloatAddition { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt+#seFloat; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(float::cast(#seCharByteShortInt),#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [11] activeUseBitwiseXOr, activeUseBitwiseXOr { \find(#allmodal ( (modal operator))\[{ .. #sv=#left^#right; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = #left^#right;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [1215] iterated_assignments_0, iterated_assignments_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=#e;#lhs0=#lhs1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1216] iterated_assignments_1, iterated_assignments_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1*=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1*#e);#lhs0=#lhs1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1217] iterated_assignments_10, iterated_assignments_10 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1|=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1|#e);#lhs0=#lhs1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1218] iterated_assignments_11, iterated_assignments_11 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1^=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1^#e);#lhs0=#lhs1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1219] iterated_assignments_2, iterated_assignments_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1/=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1/#e);#lhs0=#lhs1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1220] iterated_assignments_3, iterated_assignments_3 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1%=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1%#e);#lhs0=#lhs1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1221] iterated_assignments_4, iterated_assignments_4 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1+=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1+#e);#lhs0=#lhs1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1222] iterated_assignments_5, iterated_assignments_5 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1-=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1-#e);#lhs0=#lhs1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1223] iterated_assignments_6, iterated_assignments_6 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1<<=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1<<#e);#lhs0=#lhs1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1224] iterated_assignments_7, iterated_assignments_7 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1>>=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1>>#e);#lhs0=#lhs1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1225] iterated_assignments_8, iterated_assignments_8 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1>>>=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1>>>#e);#lhs0=#lhs1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1226] iterated_assignments_9, iterated_assignments_9 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1&=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1&#e);#lhs0=#lhs1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [126] arrayCreation, arrayCreation { \find(#normal ( (modal operator))\[{ .. #lhs=#na; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#na (program ArrayCreation)))) \replacewith(#normal ( (modal operator))\[{ .. #typeof(#na) #v0;init-array-creation(#na)#lhs=#v0; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [127] arrayCreationWithInitializers, arrayCreationWithInitializers { \find(#allmodal ( (modal operator))\[{ .. #lhs=#arrayinitializer; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#lhs (program LeftHandSide)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#lhs) #v0;init-array-creation(#arrayinitializer)#lhs=#v0; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [128] arrayInitialisation, arrayInitialisation { \find(#allmodal ( (modal operator))\[{ .. for ( int #v = #se; #v<this.#length; #v++ ) this[#v]=#lit; ... }\] (post)) \replacewith(update-application(elem-update(heap)(memset(heap,arrayRange(#a,#se,sub(length(#a),Z(1(#)))),#lit)),#allmodal(post))) \heuristics(simplify) Choices: programRules:Java}
• TestTacletEquality. [1296] less_equal_than_comparison_new, less_equal_than_comparison_new { \find(#allmodal ( (modal operator))\[{ .. #lhs=#senf0<=#senf1; ... }\] (post)) \replacewith(if-then-else(leq(#senf0,#senf1),#allmodal ( (modal operator))\[{ .. #lhs=true; ... }\] (post),#allmodal ( (modal operator))\[{ .. #lhs=false; ... }\] (post))) \heuristics(split_if, simplify_prog, obsolete) Choices: programRules:Java}
• TestTacletEquality. [1297] less_equal_than_comparison_simple, less_equal_than_comparison_simple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#senf0<=#senf1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(leq(#senf0,#senf1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1298] less_equal_than_comparison_simple_double, less_equal_than_comparison_simple_double { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seDouble0<=#seDouble1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(leqDouble(#seDouble0,#seDouble1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1299] less_equal_than_comparison_simple_float, less_equal_than_comparison_simple_float { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seFloat0<=#seFloat1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(leqFloat(#seFloat0,#seFloat1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [12] activeUseByteCast, activeUseByteCast { \find(#allmodal ( (modal operator))\[{ .. #sv=(byte)#seShortIntLong; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = (byte)#seShortIntLong;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [1309] less_than_comparison_new, less_than_comparison_new { \find(#allmodal ( (modal operator))\[{ .. #lhs=#senf0<#senf1; ... }\] (post)) \replacewith(if-then-else(lt(#senf0,#senf1),#allmodal ( (modal operator))\[{ .. #lhs=true; ... }\] (post),#allmodal ( (modal operator))\[{ .. #lhs=false; ... }\] (post))) \heuristics(split_if, simplify_prog, obsolete) Choices: programRules:Java}
• TestTacletEquality. [1310] less_than_comparison_simple, less_than_comparison_simple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#senf0<#senf1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(lt(#senf0,#senf1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1311] less_than_comparison_simple_double, less_than_comparison_simple_double { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seDouble0<#seDouble1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(ltDouble(#seDouble0,#seDouble1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1312] less_than_comparison_simple_float, less_than_comparison_simple_float { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seFloat0<#seFloat1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(ltFloat(#seFloat0,#seFloat1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [131] array_post_declaration, array_post_declaration { \find(#allmodal ( (modal operator))\[{ .. #arraypost ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. array-post-declaration(#arraypost) ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1332] loopScopeInvBox, loopScopeInvBox { \find(#box ( (modal operator))\[{ .. while ( #nse ) #body ... }\] (post)) \varcond(\new(#permissionsBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#savedHeapBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#heapBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#x (program Variable), (type, sort): (boolean,boolean)), \varcond (\storeTermIn(loopFormula (formula), #box ( (modal operator))\[{while ( #nse ) #body }\] (post))), \varcond (\storeStmtI…
• TestTacletEquality. [1333] loopScopeInvDia, loopScopeInvDia { \find(#dia ( (modal operator))\[{ .. while ( #nse ) #body ... }\] (post)) \varcond(\new(#permissionsBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#savedHeapBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#heapBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#variant (program Variable), KeYJavaType:null,any), \new(#x (program Variable), (type, sort): (boolean,boolean)), \varcond (\storeTermIn(loopFormula (formula), #dia ( (modal operator))\[{whi…
• TestTacletEquality. [1334] loopUnwind, loopUnwind { \find(#allmodal ( (modal operator))\[{ .. while ( #e ) #s ... }\] (post)) \varcond(\newLabel (#innerLabel (program Label)), \newLabel (#outerLabel (program Label)), ) \replacewith(#allmodal ( (modal operator))\[{ .. #unwind-loop(while ( #e ) #s ) ... }\] (post)) \heuristics(loop_expand) Choices: programRules:Java}
• TestTacletEquality. [1335] lsBreak, lsBreak { \find(#allmodal ( (modal operator))\[{ .. loop-scope(#lhs) {break ; #slist } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=true; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1336] lsContinue, lsContinue { \find(#allmodal ( (modal operator))\[{ .. loop-scope(#lhs) {continue ; #slist } ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(FALSE),post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1337] lsLblBreak, lsLblBreak { \find(#allmodal ( (modal operator))\[{ .. loop-scope(#lhs) {break ; #slist } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#lhs=true;break ; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1338] lsLblContinueMatch, lsLblContinueMatch { \find(#allmodal ( (modal operator))\[{ .. #lb:loop-scope(#lhs) {continue ; #slist } ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(FALSE),post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1339] lsLblContinueNoMatch1, lsLblContinueNoMatch1 { \find(#allmodal ( (modal operator))\[{ .. loop-scope(#lhs) {continue ; #slist } ... }\] (post)) \varcond(\varcond (\storeStmtIn(#lsStmt (program Statement), #allmodal ( (modal operator))\[{loop-scope(#lhs) {continue ; #slist } }\] (post))), \varcond (\not\isLabeled(#lsStmt (program Statement)), ) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=true;continue ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1340] lsLblContinueNoMatch2, lsLblContinueNoMatch2 { \find(#allmodal ( (modal operator))\[{ .. #lb1:loop-scope(#lhs) {continue ; #slist } ... }\] (post)) \varcond(\different (#lb1 (program Label), #lb (program Label)), ) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=true;continue ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1341] lsReturnNonVoid, lsReturnNonVoid { \find(#allmodal ( (modal operator))\[{ .. loop-scope(#lhs) {return #se;#slist} ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=true;return #se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1342] lsReturnVoid, lsReturnVoid { \find(#allmodal ( (modal operator))\[{ .. loop-scope(#lhs) {return ;#slist} ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=true;return ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1343] lsThrow, lsThrow { \find(#allmodal ( (modal operator))\[{ .. loop-scope(#lhs) {throw #se;#slist} ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=true;throw #se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1360] methodBodyExpand, methodBodyExpand { \find(#allmodal ( (modal operator))\[{ .. #mb ... }\] (post)) \replacewith(#introAtPreDefs(#allmodal ( (modal operator))\[{ .. expand-method-body(#mb) ... }\] (post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1361] methodCall, methodCall { \find(==>#allmodal ( (modal operator))\[{ .. #se.#mn(#selist); ... }\] (post)) \varcond(\not \staticMethodReference(#se (program SimpleExpression), #mn (program MethodName), #selist (program SimpleExpression)), \mayExpandMethod(#se (program SimpleExpression), #mn (program MethodName), #selist (program SimpleExpression)), ) \add [equals(#se,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[#allmodal ( (modal operator))\[{ .. method-call(#se.#mn(#selist);) ... }\] (post)]) \heuristics…
• TestTacletEquality. [1362] methodCallEmpty, methodCallEmpty { \find(#allmodal ( (modal operator))\[{ .. method-frame(#ex) {} ... }\] (post)) \replacewith(#allmodal(post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1363] methodCallEmptyNoreturnBox, methodCallEmptyNoreturnBox { \find(\[{ .. method-frame(result->#v0, #ex) {} ... }\] (post)) \replacewith(box(post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1364] methodCallEmptyReturn, methodCallEmptyReturn { \find(#allmodal ( (modal operator))\[{ .. method-frame(#ex) { return ; #slist } ... }\] (post)) \replacewith(#allmodal(post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1365] methodCallParamThrow, methodCallParamThrow { \find(#allmodal ( (modal operator))\[{ .. method-frame(result->#v0, #ex) { throw #se; #slist } ... }\] (post)) \varcond(\isLocalVariable (#se (program SimpleExpression)), ) \replacewith(#allmodal ( (modal operator))\[{ .. throw #se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1366] methodCallReturn, methodCallReturn { \find(#allmodal ( (modal operator))\[{ .. method-frame(result->#v0, #ex) { return #se; #slist } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. method-frame(#ex) { #v0=#se; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1367] methodCallReturnIgnoreResult, methodCallReturnIgnoreResult { \find(#allmodal ( (modal operator))\[{ .. method-frame(#ex) { return #se; #slist } ... }\] (post)) \replacewith(#allmodal(post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1368] methodCallSuper, methodCallSuper { \find(#allmodal ( (modal operator))\[{ .. super.#mn(#elist); ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. method-call(super.#mn(#elist);) ... }\] (post)) \heuristics(method_expand, simplify_autoname) Choices: programRules:Java}
• TestTacletEquality. [1369] methodCallThrow, methodCallThrow { \find(#allmodal ( (modal operator))\[{ .. method-frame(#ex) { throw #se; #slist } ... }\] (post)) \varcond(\isLocalVariable (#se (program SimpleExpression)), ) \replacewith(#allmodal ( (modal operator))\[{ .. throw #se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1370] methodCallUnfoldArguments, methodCallUnfoldArguments { \find(#allmodal ( (modal operator))\[{ .. #nsmr ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #evaluate-arguments(#nsmr) ... }\] (post)) \heuristics(simplify_autoname) Choices: programRules:Java}
• TestTacletEquality. [1371] methodCallUnfoldTarget, methodCallUnfoldTarget { \find(#allmodal ( (modal operator))\[{ .. #nse.#mn(#elist); ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v0;#v0=#nse;#v0.#mn(#elist); ... }\] (post)) \heuristics(simplify_autoname) Choices: programRules:Java}
• TestTacletEquality. [1372] methodCallWithAssignment, methodCallWithAssignment { \find(==>#allmodal ( (modal operator))\[{ .. #lhs=#se.#mn(#selist); ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#lhs (program LeftHandSide))), \not \staticMethodReference(#se (program SimpleExpression), #mn (program MethodName), #selist (program SimpleExpression)), \mayExpandMethod(#se (program SimpleExpression), #mn (program MethodName), #selist (program SimpleExpression)), ) \add [equals(#se,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[#allmodal…
• TestTacletEquality. [1373] methodCallWithAssignmentSuper, methodCallWithAssignmentSuper { \find(#allmodal ( (modal operator))\[{ .. #lhs=super.#mn(#elist); ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#lhs (program LeftHandSide)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#lhs) #v0;method-call(super.#mn(#elist);)#lhs=#v0; ... }\] (post)) \heuristics(method_expand, simplify_autoname) Choices: programRules:Java}
• TestTacletEquality. [1374] methodCallWithAssignmentUnfoldArguments, methodCallWithAssignmentUnfoldArguments { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nsmr; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #evaluate-arguments(#lhs=#nsmr;) ... }\] (post)) \heuristics(simplify_autoname) Choices: programRules:Java}
• TestTacletEquality. [1375] methodCallWithAssignmentUnfoldTarget, methodCallWithAssignmentUnfoldTarget { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse.#mn(#elist); ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v0;#v0=#nse;#lhs=#v0.#mn(#elist); ... }\] (post)) \heuristics(simplify_autoname) Choices: programRules:Java}
• TestTacletEquality. [1376] methodCallWithAssignmentWithinClass, methodCallWithAssignmentWithinClass { \find(#allmodal ( (modal operator))\[{ .. #lhs=#mn(#elist); ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#lhs (program LeftHandSide))), \mayExpandMethod(null, #mn (program MethodName), #elist (program Expression)), ) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#lhs) #v0;method-call(#mn(#elist);)#lhs=#v0; ... }\] (post)) \heuristics(method_expand) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [1377] methodCallWithinClass, methodCallWithinClass { \find(#allmodal ( (modal operator))\[{ .. #mn(#elist); ... }\] (post)) \varcond(\mayExpandMethod(null, #mn (program MethodName), #elist (program Expression)), ) \replacewith(#allmodal ( (modal operator))\[{ .. method-call(#mn(#elist);) ... }\] (post)) \heuristics(method_expand) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [138] assertSafe, assertSafe { \find(==>#allmodal ( (modal operator))\[{ .. assert #e1; ... }\] (b)) \varcond(\new(#condition (program Variable), \typeof(#e1 (program Expression))), \not \containsAssignment( #e1 ), ) \add [equals(oldHeap,heap)]==>[] \replacewith([]==>[\[{method-frame(#ex) {#typeof (#e1) #condition = #e1; } }\] (all{f (variable)}(all{o (variable)}(or(and(not(equals(o,null)),equals(boolean::select(oldHeap,o,java.lang.Object::<created>),FALSE)),equals(any::select(oldHeap,o,f),any::select(heap,o,f))))))]) …
• TestTacletEquality. [139] assertSafeWithMessage, assertSafeWithMessage { \find(==>#allmodal ( (modal operator))\[{ .. assert #e1 : #e2; ... }\] (b)) \varcond(\new(#message (program Variable), \typeof(#e2 (program Expression))), \new(#condition (program Variable), \typeof(#e1 (program Expression))), \not \containsAssignment( #e1 ), \not \containsAssignment( #e2 ), ) \add [equals(oldHeap,heap)]==>[] \replacewith([]==>[\[{method-frame(#ex) {#typeof (#e1) #condition = #e1;#typeof (#e2) #message = #e2; } }\] (all{f (variable)}(all{o (variable)}(or(and…
• TestTacletEquality. [13] activeUseCharCast, activeUseCharCast { \find(#allmodal ( (modal operator))\[{ .. #sv=(char)#seByteShortIntLong; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = (char)#seByteShortIntLong;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [140] assignment, assignment { \find(#allmodal ( (modal operator))\[{ .. #loc=#se; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(#se),#allmodal(post))) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [141] assignmentAdditionBigint1, assignmentAdditionBigint1 { \find(#allmodal ( (modal operator))\[{ .. #loc=#seBigint+#seAny; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(add(#seBigint,#seAny)),#allmodal(post))) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & bigint:on)}
• TestTacletEquality. [1429] narrowingByteCastBigint, narrowingByteCastBigint { \find(#allmodal ( (modal operator))\[{ .. #loc=(byte)#seBigint; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seBigint)),#allmodal(post))) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & bigint:on)}
• TestTacletEquality. [142] assignmentAdditionBigint2, assignmentAdditionBigint2 { \find(#allmodal ( (modal operator))\[{ .. #loc=#seAny+#seBigint; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(add(#seAny,#seBigint)),#allmodal(post))) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & bigint:on)}
• TestTacletEquality. [1430] narrowingByteCastInt, narrowingByteCastInt { \find(#normalassign ( (modal operator))\[{ .. #loc=(byte)#seInt; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1431] narrowingByteCastLong, narrowingByteCastLong { \find(#normalassign ( (modal operator))\[{ .. #loc=(byte)#seLong; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1432] narrowingByteCastShort, narrowingByteCastShort { \find(#normalassign ( (modal operator))\[{ .. #loc=(byte)#seShort; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seShort)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1433] narrowingCastFloatToInt, narrowingCastFloatToInt { \find(#normalassign ( (modal operator))\[{ .. #loc=(int)#seFloat; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(int::cast(#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [1434] narrowingCastFloatToLong, narrowingCastFloatToLong { \find(#normalassign ( (modal operator))\[{ .. #loc=(long)#seFloat; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(int::cast(#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [1435] narrowingCharCastBigint, narrowingCharCastBigint { \find(#allmodal ( (modal operator))\[{ .. #loc=(char)#seBigint; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seBigint)),#allmodal(post))) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & bigint:on)}
• TestTacletEquality. [1436] narrowingCharCastByte, narrowingCharCastByte { \find(#normalassign ( (modal operator))\[{ .. #loc=(char)#seByte; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seByte)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1437] narrowingCharCastInt, narrowingCharCastInt { \find(#normalassign ( (modal operator))\[{ .. #loc=(char)#seInt; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1438] narrowingCharCastLong, narrowingCharCastLong { \find(#normalassign ( (modal operator))\[{ .. #loc=(char)#seLong; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1439] narrowingCharCastShort, narrowingCharCastShort { \find(#normalassign ( (modal operator))\[{ .. #loc=(char)#seShort; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seShort)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [143] assignmentAdditionDouble, assignmentAdditionDouble { \find(#normalassign ( (modal operator))\[{ .. #loc=#seDouble0+#seDouble1; ... }\] (post)) \varcond(\not\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [1440] narrowingIntCastBigint, narrowingIntCastBigint { \find(#allmodal ( (modal operator))\[{ .. #loc=(int)#seBigint; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastInt(#seBigint)),#allmodal(post))) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & bigint:on)}
• TestTacletEquality. [1441] narrowingIntCastLong, narrowingIntCastLong { \find(#normalassign ( (modal operator))\[{ .. #loc=(int)#seLong; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastInt(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1442] narrowingLongCastBigint, narrowingLongCastBigint { \find(#allmodal ( (modal operator))\[{ .. #loc=(long)#seBigint; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastLong(#seBigint)),#allmodal(post))) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & bigint:on)}
• TestTacletEquality. [1443] narrowingShortCastBigint, narrowingShortCastBigint { \find(#allmodal ( (modal operator))\[{ .. #loc=(short)#seBigint; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seBigint)),#allmodal(post))) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & bigint:on)}
• TestTacletEquality. [1444] narrowingShortCastInt, narrowingShortCastInt { \find(#normalassign ( (modal operator))\[{ .. #loc=(short)#seInt; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1445] narrowingShortCastLong, narrowingShortCastLong { \find(#normalassign ( (modal operator))\[{ .. #loc=(short)#seLong; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [144] assignmentAdditionDoubleStrictFP, assignmentAdditionDoubleStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc=#seDouble0+#seDouble1; ... }\] (post)) \varcond(\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(addDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java}
• TestTacletEquality. [145] assignmentAdditionFloat, assignmentAdditionFloat { \find(#normalassign ( (modal operator))\[{ .. #loc=#seFloat0+#seFloat1; ... }\] (post)) \varcond(\not\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [146] assignmentAdditionFloatStrictFP, assignmentAdditionFloatStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc=#seFloat0+#seFloat1; ... }\] (post)) \varcond(\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(addFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [147] assignmentAdditionInt, assignmentAdditionInt { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt0+#seCharByteShortInt1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [148] assignmentAdditionLong, assignmentAdditionLong { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt+#seLong; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [149] assignmentAdditionLong2, assignmentAdditionLong2 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong+#seCharByteShortInt; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [14] activeUseDivision, activeUseDivision { \find(#allmodal ( (modal operator))\[{ .. #sv=#left/#right; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = #left/#right;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [150] assignmentAdditionLong3, assignmentAdditionLong3 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong0+#seLong1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [151] assignmentBitwiseAndInt, assignmentBitwiseAndInt { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt0&#seCharByteShortInt1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [152] assignmentBitwiseAndLong, assignmentBitwiseAndLong { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt&#seLong; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1531] postdecrement, postdecrement { \find(#allmodal ( (modal operator))\[{ .. #lhs1--; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))#lhs1-1; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• 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) #v = #e;#typeof(#e0) #v0 = #e0;#v[#v0]=(#typeof(#e[#e0]))(#v[#v0]-1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1533] postdecrement_assignment, postdecrement_assignment { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1--; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#lhs0 (program LeftHandSide)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#lhs0) #v = #lhs1;#lhs1=(#typeof(#lhs1))(#lhs1-1);#lhs0=#v; ... }\] (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) #v = #e;#typeof(#e0) #v0 = #e0;#typeof(#lhs0) #v1 = #v[#v0];#v[#v0]=(#typeof(#e[#e0]))(#v[#v0]-1);#lhs0=#v1; ... }\] (post)) \heuristic…
• TestTacletEquality. [1535] postdecrement_assignment_attribute, postdecrement_assignment_attribute { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e.#attribute--; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#lhs0 (program LeftHandSide))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v = #e;#typeof(#lhs0) #v1 = #v.#attribute;#v.#attribute=(#typeof(#attribute))(#v.#attribute-1);#lhs0=#v1; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1536] postdecrement_attribute, postdecrement_attribute { \find(#allmodal ( (modal operator))\[{ .. #e.#attribute--; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v = #e;#v.#attribute=(#typeof(#attribute))(#v.#attribute-1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1537] postincrement, postincrement { \find(#allmodal ( (modal operator))\[{ .. #lhs1++; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1+1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• 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) #v = #e;#typeof(#e0) #v0 = #e0;#v[#v0]=(#typeof(#e[#e0]))(#v[#v0]+1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1539] postincrement_assignment, postincrement_assignment { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#lhs1++; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#lhs0 (program LeftHandSide)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#lhs0) #v = #lhs1;#lhs1=(#typeof(#lhs1))(#lhs1+1);#lhs0=#v; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [153] assignmentBitwiseAndLong2, assignmentBitwiseAndLong2 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong&#seCharByteShortInt; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) 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) #v = #e;#typeof(#e0) #v0 = #e0;#typeof(#lhs0) #v1 = #v[#v0];#v[#v0]=(#typeof(#e[#e0]))(#v[#v0]+1);#lhs0=#v1; ... }\] (post)) \heuristic…
• TestTacletEquality. [1541] postincrement_assignment_attribute, postincrement_assignment_attribute { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e.#attribute++; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#lhs0 (program LeftHandSide))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v = #e;#typeof(#lhs0) #v1 = #v.#attribute;#v.#attribute=(#typeof(#attribute))(#v.#attribute+1);#lhs0=#v1; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1542] postincrement_attribute, postincrement_attribute { \find(#allmodal ( (modal operator))\[{ .. #e.#attribute++; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v = #e;#v.#attribute=(#typeof(#attribute))(#v.#attribute+1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [154] assignmentBitwiseAndLong3, assignmentBitwiseAndLong3 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong0&#seLong1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseAndLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [155] assignmentBitwiseOrInt, assignmentBitwiseOrInt { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt0|#seCharByteShortInt1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [156] assignmentBitwiseOrLong, assignmentBitwiseOrLong { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt|#seLong; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1575] predecrement, predecrement { \find(#allmodal ( (modal operator))\[{ .. --#lhs1; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1-1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• 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) #v = #e;#typeof(#e0) #v0 = #e0;#v[#v0]=(#typeof(#e[#e0]))(#v[#v0]-1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1577] predecrement_assignment, predecrement_assignment { \find(#allmodal ( (modal operator))\[{ .. #lhs0=--#lhs1; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1-1);#lhs0=#lhs1; ... }\] (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) #v = #e;#typeof(#e0) #v0 = #e0;#v[#v0]=(#typeof(#e[#e0]))(#v[#v0]-1);#lhs0=#v[#v0]; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1579] predecrement_assignment_attribute, predecrement_assignment_attribute { \find(#allmodal ( (modal operator))\[{ .. #lhs=--#e.#attribute; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v = #e;#v.#attribute=(#typeof(#attribute))(#v.#attribute-1);#lhs=#v.#attribute; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [157] assignmentBitwiseOrLong2, assignmentBitwiseOrLong2 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong|#seCharByteShortInt; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1580] predecrement_attribute, predecrement_attribute { \find(#allmodal ( (modal operator))\[{ .. --#e.#attribute; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v = #e;#v.#attribute=(#typeof(#attribute))(#v.#attribute-1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1581] preincrement, preincrement { \find(#allmodal ( (modal operator))\[{ .. ++#lhs1; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1+1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• 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) #v = #e;#typeof(#e0) #v0 = #e0;#v[#v0]=(#typeof(#e[#e0]))(#v[#v0]+1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1583] preincrement_assignment, preincrement_assignment { \find(#allmodal ( (modal operator))\[{ .. #lhs0=++#lhs1; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs1=(#typeof(#lhs1))(#lhs1+1);#lhs0=#lhs1; ... }\] (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) #v = #e;#typeof(#e0) #v0 = #e0;#v[#v0]=(#typeof(#e[#e0]))(#v[#v0]+1);#lhs0=#v[#v0]; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1585] preincrement_assignment_attribute, preincrement_assignment_attribute { \find(#allmodal ( (modal operator))\[{ .. #lhs0=++#e.#attribute; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v = #e;#v.#attribute=(#typeof(#attribute))(#v.#attribute+1);#lhs0=#v.#attribute; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [1586] preincrement_attribute, preincrement_attribute { \find(#allmodal ( (modal operator))\[{ .. ++#e.#attribute; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v = #e;#v.#attribute=(#typeof(#attribute))(#v.#attribute+1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [158] assignmentBitwiseOrLong3, assignmentBitwiseOrLong3 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong0|#seLong1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseOrLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [159] assignmentBitwiseXOrInt, assignmentBitwiseXOrInt { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt0^#seCharByteShortInt1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [15] activeUseIntCast, activeUseIntCast { \find(#allmodal ( (modal operator))\[{ .. #sv=(int)#seLong; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = (int)#seLong;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [160] assignmentBitwiseXOrLong, assignmentBitwiseXOrLong { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt^#seLong; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1617] reference_type_cast, reference_type_cast { \find(==>#allmodal ( (modal operator))\[{ .. #lhs=(#npit)#se; ... }\] (post)) \varcond(\hasSort(#npit (program NonPrimitiveType), G), \not\sub(\typeof(#se (program SimpleExpression)), G), ) \add []==>[or(equals(#se,null),equals(G::instance(#se),TRUE))] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(#lhs (program LeftHandSide))(#addCast(#se,#lhs)),#allmodal(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & runtimeExceptions:ban)}
• TestTacletEquality. [161] assignmentBitwiseXOrLong2, assignmentBitwiseXOrLong2 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong^#seCharByteShortInt; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [162] assignmentBitwiseXOrLong3, assignmentBitwiseXOrLong3 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong0^#seLong1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseXOrLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1631] remove_parentheses_attribute_left, remove_parentheses_attribute_left { \find(#allmodal ( (modal operator))\[{ .. (#e.#attribute)=#e0; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #e.#attribute=#e0; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1632] remove_parentheses_lhs_left, remove_parentheses_lhs_left { \find(#allmodal ( (modal operator))\[{ .. (#lhs)=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#e; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1633] remove_parentheses_right, remove_parentheses_right { \find(#allmodal ( (modal operator))\[{ .. #lhs=(#e); ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#e; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [163] assignmentDivisionBigint1, assignmentDivisionBigint1 { \find(==>#allmodal ( (modal operator))\[{ .. #loc=#seBigint/#seAny; ... }\] (post)) \replacewith([]==>[not(equals(#seAny,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(div(#seBigint,#seAny)),#allmodal(post))]) \heuristics(executeIntegerAssignment) Choices: ((programRules:Java & bigint:on) & runtimeExceptions:ban)}
• TestTacletEquality. [164] assignmentDivisionBigint2, assignmentDivisionBigint2 { \find(==>#allmodal ( (modal operator))\[{ .. #loc=#seAny/#seBigint; ... }\] (post)) \replacewith([]==>[not(equals(#seBigint,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(div(#seAny,#seBigint)),#allmodal(post))]) \heuristics(executeIntegerAssignment) Choices: ((programRules:Java & bigint:on) & runtimeExceptions:ban)}
• TestTacletEquality. [165] assignmentDivisionDouble, assignmentDivisionDouble { \find(#normalassign ( (modal operator))\[{ .. #loc=#seDouble0/#seDouble1; ... }\] (post)) \varcond(\not\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(javaDivDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [1667] returnUnfold, returnUnfold { \find(#allmodal ( (modal operator))\[{ .. return #nse; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v0 = #nse;return #v0; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [166] assignmentDivisionDoubleStrictFP, assignmentDivisionDoubleStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc=#seDouble0/#seDouble1; ... }\] (post)) \varcond(\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(divDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java}
• TestTacletEquality. [1673] same_boxes_left, same_boxes_left { \assumes ([\[{ .. #s ... }\] (post)]==>[]) \find(\[{ .. #s ... }\] (post1)==>) \add [\[{ .. #s ... }\] (and(post,post1))]==>[] Choices: programRules:Java}
• TestTacletEquality. [1674] same_boxes_right, same_boxes_right { \assumes ([]==>[\[{ .. #s ... }\] (post)]) \find(==>\[{ .. #s ... }\] (post1)) \add []==>[\[{ .. #s ... }\] (or(post,post1))] Choices: programRules:Java}
• TestTacletEquality. [1675] same_diamonds_left, same_diamonds_left { \assumes ([\<{ .. #s ... }\> (post)]==>[]) \find(\<{ .. #s ... }\> (post1)==>) \add [\<{ .. #s ... }\> (and(post,post1))]==>[] Choices: programRules:Java}
• TestTacletEquality. [1676] same_diamonds_right, same_diamonds_right { \assumes ([]==>[\<{#s}\> (post)]) \find(==>\<{#s}\> (post1)) \add []==>[\<{#s}\> (or(post,post1))] Choices: programRules:Java}
• TestTacletEquality. [167] assignmentDivisionFloat, assignmentDivisionFloat { \find(#normalassign ( (modal operator))\[{ .. #loc=#seFloat0/#seFloat1; ... }\] (post)) \varcond(\not\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(javaDivFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [168] assignmentDivisionFloatStrictFP, assignmentDivisionFloatStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc=#seFloat0/#seFloat1; ... }\] (post)) \varcond(\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(divFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [1692] seqConcatUnfoldLeft, seqConcatUnfoldLeft { \find(#allmodal ( (modal operator))\[{ .. #v=\seq_concat(#nseLeft,#eRight); ... }\] (post)) \varcond(\new(#vLeftNew (program Variable), \typeof(#nseLeft (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseLeft) #vLeftNew = #nseLeft;#v=\seq_concat(#vLeftNew,#eRight); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1693] seqConcatUnfoldRight, seqConcatUnfoldRight { \find(#allmodal ( (modal operator))\[{ .. #v=\seq_concat(#seLeft,#nseRight); ... }\] (post)) \varcond(\new(#vRightNew (program Variable), \typeof(#nseRight (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseRight) #vRightNew = #nseRight;#v=\seq_concat(#seLeft,#vRightNew); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [169] assignmentDivisionInt, assignmentDivisionInt { \find(==>#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt0/#seCharByteShortInt1; ... }\] (post)) \replacewith([]==>[not(equals(#seCharByteShortInt1,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaDivInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))]) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & runtimeExceptions:ban)}
• TestTacletEquality. [16] activeUseModulo, activeUseModulo { \find(#allmodal ( (modal operator))\[{ .. #sv=#left%#right; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = #left%#right;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [1707] seqGetUnfoldLeft, seqGetUnfoldLeft { \find(#allmodal ( (modal operator))\[{ .. #v=#nseLeft[#eRight]; ... }\] (post)) \varcond(\new(#vLeftNew (program Variable), \typeof(#nseLeft (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseLeft) #vLeftNew = #nseLeft;#v=#vLeftNew[#eRight]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1708] seqGetUnfoldRight, seqGetUnfoldRight { \find(#allmodal ( (modal operator))\[{ .. #v=#seLeft[#nseRight]; ... }\] (post)) \varcond(\new(#vRightNew (program Variable), \typeof(#nseRight (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseRight) #vRightNew = #nseRight;#v=#seLeft[#vRightNew]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [170] assignmentDivisionLong, assignmentDivisionLong { \find(==>#normalassign ( (modal operator))\[{ .. #loc=#se/#seLong; ... }\] (post)) \replacewith([]==>[not(equals(#seLong,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaDivLong(#se,#seLong)),#normalassign(post))]) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & runtimeExceptions:ban)}
• TestTacletEquality. [1710] seqIndexOfUnfoldLeft, seqIndexOfUnfoldLeft { \find(#allmodal ( (modal operator))\[{ .. #v=\indexOf(#nseLeft,#eRight); ... }\] (post)) \varcond(\new(#vLeftNew (program Variable), \typeof(#nseLeft (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseLeft) #vLeftNew = #nseLeft;#v=\indexOf(#vLeftNew,#eRight); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1711] seqIndexOfUnfoldRight, seqIndexOfUnfoldRight { \find(#allmodal ( (modal operator))\[{ .. #v=\indexOf(#seLeft,#nseRight); ... }\] (post)) \varcond(\new(#vRightNew (program Variable), \typeof(#nseRight (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseRight) #vRightNew = #nseRight;#v=\indexOf(#seLeft,#vRightNew); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1712] seqLengthUnfold, seqLengthUnfold { \find(#allmodal ( (modal operator))\[{ .. #v=#nse.length; ... }\] (post)) \varcond(\new(#vNew (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #vNew = #nse;#v=#vNew.length; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1715] seqReverseUnfold, seqReverseUnfold { \find(#allmodal ( (modal operator))\[{ .. #v=\seq_reverse(#nse); ... }\] (post)) \varcond(\new(#vNew (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #vNew = #nse;#v=\seq_reverse(#vNew); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1718] seqSingletonUnfold, seqSingletonUnfold { \find(#allmodal ( (modal operator))\[{ .. #v=\seq_singleton(#nse); ... }\] (post)) \varcond(\new(#vNew (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #vNew = #nse;#v=\seq_singleton(#vNew); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1719] seqSubUnfoldLeft, seqSubUnfoldLeft { \find(#allmodal ( (modal operator))\[{ .. #v=\seq_sub(#nseLeft,#eMiddle,#eRight); ... }\] (post)) \varcond(\new(#vLeftNew (program Variable), \typeof(#nseLeft (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseLeft) #vLeftNew = #nseLeft;#v=\seq_sub(#vLeftNew,#eMiddle,#eRight); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [171] assignmentDivisionLong2, assignmentDivisionLong2 { \find(==>#normalassign ( (modal operator))\[{ .. #loc=#seLong/#seCharByteShortInt; ... }\] (post)) \replacewith([]==>[not(equals(#seCharByteShortInt,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaDivLong(#seLong,#seCharByteShortInt)),#normalassign(post))]) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & runtimeExceptions:ban)}
• TestTacletEquality. [1720] seqSubUnfoldMiddle, seqSubUnfoldMiddle { \find(#allmodal ( (modal operator))\[{ .. #v=\seq_sub(#seLeft,#nseMiddle,#eRight); ... }\] (post)) \varcond(\new(#vMiddleNew (program Variable), \typeof(#nseMiddle (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseMiddle) #vMiddleNew = #nseMiddle;#v=\seq_sub(#seLeft,#vMiddleNew,#eRight); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1721] seqSubUnfoldRight, seqSubUnfoldRight { \find(#allmodal ( (modal operator))\[{ .. #v=\seq_sub(#seLeft,#seMiddle,#nseRight); ... }\] (post)) \varcond(\new(#vRightNew (program Variable), \typeof(#nseRight (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseRight) #vRightNew = #nseRight;#v=\seq_sub(#seLeft,#seMiddle,#vRightNew); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1725] setIntersectUnfoldLeft, setIntersectUnfoldLeft { \find(#allmodal ( (modal operator))\[{ .. #v=\intersect(#nseLeft,#eRight); ... }\] (post)) \varcond(\new(#vLeftNew (program Variable), \typeof(#nseLeft (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseLeft) #vLeftNew = #nseLeft;#v=\intersect(#vLeftNew,#eRight); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1726] setIntersectUnfoldRight, setIntersectUnfoldRight { \find(#allmodal ( (modal operator))\[{ .. #v=\intersect(#seLeft,#nseRight); ... }\] (post)) \varcond(\new(#vRightNew (program Variable), \typeof(#nseRight (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseRight) #vRightNew = #nseRight;#v=\intersect(#seLeft,#vRightNew); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1727] setJavaCardTransient, setJavaCardTransient { \find(==>#allmodal ( (modal operator))\[{ .. #jcsystemType.#setTransient(#se,#se1)@#jcsystemType; ... }\] (post)) \replacewith([]==>[not(equals(#se,null))]) ; \replacewith([]==>[update-application(elem-update(heap)(store(heap,#se,java.lang.Object::<transient>,#se1)),#allmodal(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)}
• TestTacletEquality. [172] assignmentModDouble, assignmentModDouble { \find(#normalassign ( (modal operator))\[{ .. #loc=#seDouble0%#seDouble1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaModDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [1732] setMinusUnfoldLeft, setMinusUnfoldLeft { \find(#allmodal ( (modal operator))\[{ .. #v=\set_minus(#nseLeft,#eRight); ... }\] (post)) \varcond(\new(#vLeftNew (program Variable), \typeof(#nseLeft (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseLeft) #vLeftNew = #nseLeft;#v=\set_minus(#vLeftNew,#eRight); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1733] setMinusUnfoldRight, setMinusUnfoldRight { \find(#allmodal ( (modal operator))\[{ .. #v=\set_minus(#seLeft,#nseRight); ... }\] (post)) \varcond(\new(#vRightNew (program Variable), \typeof(#nseRight (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseRight) #vRightNew = #nseRight;#v=\set_minus(#seLeft,#vRightNew); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1737] setUnionUnfoldLeft, setUnionUnfoldLeft { \find(#allmodal ( (modal operator))\[{ .. #v=\set_union(#nseLeft,#eRight); ... }\] (post)) \varcond(\new(#vLeftNew (program Variable), \typeof(#nseLeft (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseLeft) #vLeftNew = #nseLeft;#v=\set_union(#vLeftNew,#eRight); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1738] setUnionUnfoldRight, setUnionUnfoldRight { \find(#allmodal ( (modal operator))\[{ .. #v=\set_union(#seLeft,#nseRight); ... }\] (post)) \varcond(\new(#vRightNew (program Variable), \typeof(#nseRight (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseRight) #vRightNew = #nseRight;#v=\set_union(#seLeft,#vRightNew); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [173] assignmentModFloat, assignmentModFloat { \find(#normalassign ( (modal operator))\[{ .. #loc=#seFloat0%#seFloat1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaModFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [174] assignmentModulo, assignmentModulo { \find(==>#normalassign ( (modal operator))\[{ .. #loc=#se0%#se1; ... }\] (post)) \replacewith([]==>[not(equals(#se1,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(javaMod(#se0,#se1)),#normalassign(post))]) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & runtimeExceptions:ban)}
• TestTacletEquality. [175] assignmentModuloBigint1, assignmentModuloBigint1 { \find(==>#allmodal ( (modal operator))\[{ .. #loc=#seBigint%#seAny; ... }\] (post)) \replacewith([]==>[not(equals(#seAny,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(mod(#seBigint,#seAny)),#allmodal(post))]) \heuristics(executeIntegerAssignment) Choices: ((programRules:Java & bigint:on) & runtimeExceptions:ban)}
• TestTacletEquality. [176] assignmentModuloBigint2, assignmentModuloBigint2 { \find(==>#allmodal ( (modal operator))\[{ .. #loc=#seAny%#seBigint; ... }\] (post)) \replacewith([]==>[not(equals(#seBigint,Z(0(#))))]) ; \replacewith([]==>[update-application(elem-update(#loc (program Variable))(mod(#seAny,#seBigint)),#allmodal(post))]) \heuristics(executeIntegerAssignment) Choices: ((programRules:Java & bigint:on) & runtimeExceptions:ban)}
• TestTacletEquality. [1771] singletonAssignment, singletonAssignment { \find(#allmodal ( (modal operator))\[{ .. #v=\singleton(#seObj.#a); ... }\] (post)) \replacewith(update-application(elem-update(#v (program Variable))(singleton(#seObj,#memberPVToField(#a))),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1773] singletonUnfold, singletonUnfold { \find(#allmodal ( (modal operator))\[{ .. #v=\singleton(#nseObj.#a); ... }\] (post)) \varcond(\new(#vObjNew (program Variable), \typeof(#nseObj (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseObj) #vObjNew = #nseObj;#v=\singleton(#vObjNew.#a); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [177] assignmentMultiplicationBigint1, assignmentMultiplicationBigint1 { \find(#allmodal ( (modal operator))\[{ .. #loc=#seBigint*#seAny; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(mul(#seBigint,#seAny)),#allmodal(post))) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & bigint:on)}
• TestTacletEquality. [1782] special_constructor_call, special_constructor_call { \find(#allmodal ( (modal operator))\[{ .. #scr ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. special-constructor-call(#scr) ... }\] (post)) \heuristics(method_expand) Choices: programRules:Java}
• TestTacletEquality. [178] assignmentMultiplicationBigint2, assignmentMultiplicationBigint2 { \find(#allmodal ( (modal operator))\[{ .. #loc=#seAny*#seBigint; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(mul(#seAny,#seBigint)),#allmodal(post))) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & bigint:on)}
• TestTacletEquality. [1793] staticMethodCall, staticMethodCall { \find(#allmodal ( (modal operator))\[{ .. #se.#mn(#elist); ... }\] (post)) \varcond(\staticMethodReference(#se (program SimpleExpression), #mn (program MethodName), #elist (program Expression)), ) \replacewith(#allmodal ( (modal operator))\[{ .. method-call(#se.#mn(#elist);) ... }\] (post)) \heuristics(method_expand) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [1794] staticMethodCallStaticViaTypereference, staticMethodCallStaticViaTypereference { \find(#allmodal ( (modal operator))\[{ .. #t.#mn(#elist); ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. method-call(#t.#mn(#elist);) ... }\] (post)) \heuristics(method_expand) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [1795] staticMethodCallStaticWithAssignmentViaTypereference, staticMethodCallStaticWithAssignmentViaTypereference { \find(#allmodal ( (modal operator))\[{ .. #lhs=#t.#mn(#elist); ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#lhs (program LeftHandSide)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#lhs) #v0;method-call(#t.#mn(#elist);)#lhs=#v0; ... }\] (post)) \heuristics(method_expand) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [1796] staticMethodCallWithAssignment, staticMethodCallWithAssignment { \find(#allmodal ( (modal operator))\[{ .. #lhs=#se.#mn(#elist); ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#lhs (program LeftHandSide))), \staticMethodReference(#se (program SimpleExpression), #mn (program MethodName), #elist (program Expression)), ) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#lhs) #v0;method-call(#se.#mn(#elist);)#lhs=#v0; ... }\] (post)) \heuristics(method_expand) Choices: (programRules:Java & initialisation:disableStatic…
• TestTacletEquality. [1797] stringAssignment, stringAssignment { \find(#normalassign ( (modal operator))\[{ .. #v=#slit; ... }\] (post)) \sameUpdateLevel\add [not(equals(strPool(#slit),null)),equals(boolean::select(heap,strPool(#slit),java.lang.Object::<created>),TRUE)]==>[] \replacewith(update-application(elem-update(#v (program Variable))(strPool(#slit)),#normalassign(post))) \heuristics(simplify_prog_subset, simplify_prog) Choices: true}
• TestTacletEquality. [1798] stringConcat, stringConcat { \find(#normalassign ( (modal operator))\[{ .. #v=#sstr1+#sstr2; ... }\] (post)) \sameUpdateLevel\add [equals(strContent(sk),seqConcat(strContent(#sstr1),strContent(#sstr2)))]==>[equals(sk,null)] \replacewith(update-application(elem-update(#v (program Variable))(sk),update-application(elem-update(heap)(create(heap,sk)),#normalassign(post)))) \heuristics(simplify_prog_subset, simplify_prog) Choices: true}
• TestTacletEquality. [1799] stringConcatBooleanLeft, stringConcatBooleanLeft { \find(#normalassign ( (modal operator))\[{ .. #v=#seLeft+#sstrRight; ... }\] (post)) \sameUpdateLevel\add [equals(strContent(sk),seqConcat(if-then-else(equals(#seLeft,TRUE),seqConcat(seqSingleton(C(6(1(1(#))))),seqConcat(seqSingleton(C(4(1(1(#))))),seqConcat(seqSingleton(C(7(1(1(#))))),seqSingleton(C(1(0(1(#)))))))),seqConcat(seqSingleton(C(2(0(1(#))))),seqConcat(seqSingleton(C(7(9(#)))),seqConcat(seqSingleton(C(8(0(1(#))))),seqConcat(seqSingleton(C(5(1(1(#))))),seqSingleton(C(1(0…
• TestTacletEquality. [179] assignmentMultiplicationDouble, assignmentMultiplicationDouble { \find(#normalassign ( (modal operator))\[{ .. #loc=#seDouble0*#seDouble1; ... }\] (post)) \varcond(\not\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [17] activeUseMultiplication, activeUseMultiplication { \find(#allmodal ( (modal operator))\[{ .. #sv=#left*#right; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = #left*#right;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [1800] stringConcatBooleanRight, stringConcatBooleanRight { \find(#normalassign ( (modal operator))\[{ .. #v=#sstrLeft+#seRight; ... }\] (post)) \sameUpdateLevel\add [equals(strContent(sk),seqConcat(strContent(#sstrLeft),if-then-else(equals(#seRight,TRUE),seqConcat(seqSingleton(C(6(1(1(#))))),seqConcat(seqSingleton(C(4(1(1(#))))),seqConcat(seqSingleton(C(7(1(1(#))))),seqSingleton(C(1(0(1(#)))))))),seqConcat(seqSingleton(C(2(0(1(#))))),seqConcat(seqSingleton(C(7(9(#)))),seqConcat(seqSingleton(C(8(0(1(#))))),seqConcat(seqSingleton(C(5(1(1(#…
• TestTacletEquality. [1801] stringConcatCharExpLeft, stringConcatCharExpLeft { \find(#normalassign ( (modal operator))\[{ .. #v=#seLeft+#sstrRight; ... }\] (post)) \sameUpdateLevel\add [equals(strContent(sk),seqConcat(seqSingleton(#seLeft),strContent(#sstrRight)))]==>[equals(sk,null)] \replacewith(update-application(elem-update(#v (program Variable))(sk),update-application(elem-update(heap)(create(heap,sk)),#normalassign(post)))) \heuristics(simplify_prog_subset, simplify_prog) Choices: true}
• TestTacletEquality. [1802] stringConcatCharExpRight, stringConcatCharExpRight { \find(#normalassign ( (modal operator))\[{ .. #v=#sstrLeft+#seRight; ... }\] (post)) \sameUpdateLevel\add [equals(strContent(sk),seqConcat(strContent(#sstrLeft),seqSingleton(#seRight)))]==>[equals(sk,null)] \replacewith(update-application(elem-update(#v (program Variable))(sk),update-application(elem-update(heap)(create(heap,sk)),#normalassign(post)))) \heuristics(simplify_prog_subset, simplify_prog) Choices: true}
• TestTacletEquality. [1803] stringConcatIntExpLeft, stringConcatIntExpLeft { \find(#normalassign ( (modal operator))\[{ .. #v=#seLeft+#sstrRight; ... }\] (post)) \sameUpdateLevel\add [equals(strContent(sk),seqConcat(clTranslateInt(#seLeft),strContent(#sstrRight)))]==>[equals(sk,null)] \replacewith(update-application(elem-update(#v (program Variable))(sk),update-application(elem-update(heap)(create(heap,sk)),#normalassign(post)))) \heuristics(simplify_prog_subset, simplify_prog) Choices: true}
• TestTacletEquality. [1804] stringConcatIntExpRight, stringConcatIntExpRight { \find(#normalassign ( (modal operator))\[{ .. #v=#sstrLeft+#seRight; ... }\] (post)) \sameUpdateLevel\add [equals(strContent(sk),seqConcat(strContent(#sstrLeft),clTranslateInt(#seRight)))]==>[equals(sk,null)] \replacewith(update-application(elem-update(#v (program Variable))(sk),update-application(elem-update(heap)(create(heap,sk)),#normalassign(post)))) \heuristics(simplify_prog_subset, simplify_prog) Choices: true}
• TestTacletEquality. [1805] stringConcatObjectLeft, stringConcatObjectLeft { \find(#normalassign ( (modal operator))\[{ .. #v=#seLeft+#sstrRight; ... }\] (post)) \sameUpdateLevel\add [equals(#seLeft,null),equals(strContent(sk),seqConcat(strContent(null),strContent(#sstrRight)))]==>[equals(sk,null)] \replacewith(update-application(elem-update(#v (program Variable))(sk),update-application(elem-update(heap)(create(heap,sk)),#normalassign(post)))) ; \add []==>[equals(#seLeft,null)] \replacewith(#normalassign ( (modal operator))\[{ .. #v=#seLeft.toString()+#sstr…
• TestTacletEquality. [1806] stringConcatObjectRight, stringConcatObjectRight { \find(#normalassign ( (modal operator))\[{ .. #v=#sstrLeft+#seRight; ... }\] (post)) \sameUpdateLevel\add [equals(#seRight,null),equals(strContent(sk),seqConcat(strContent(#sstrLeft),strContent(null)))]==>[equals(sk,null)] \replacewith(update-application(elem-update(#v (program Variable))(sk),update-application(elem-update(heap)(create(heap,sk)),#normalassign(post)))) ; \add []==>[equals(#seRight,null)] \replacewith(#normalassign ( (modal operator))\[{ .. #v=#sstrLeft+#seRight.toS…
• TestTacletEquality. [180] assignmentMultiplicationDoubleStrictFP, assignmentMultiplicationDoubleStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc=#seDouble0*#seDouble1; ... }\] (post)) \varcond(\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(mulDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java}
• TestTacletEquality. [181] assignmentMultiplicationFloat, assignmentMultiplicationFloat { \find(#normalassign ( (modal operator))\[{ .. #loc=#seFloat0*#seFloat1; ... }\] (post)) \varcond(\not\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [182] assignmentMultiplicationFloatStrictFP, assignmentMultiplicationFloatStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc=#seFloat0*#seFloat1; ... }\] (post)) \varcond(\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(mulFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [183] assignmentMultiplicationInt, assignmentMultiplicationInt { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt0*#seCharByteShortInt1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [184] assignmentMultiplicationLong, assignmentMultiplicationLong { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt*#seLong; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [185] assignmentMultiplicationLong2, assignmentMultiplicationLong2 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong*#seCharByteShortInt; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1861] switch, switch { \find(#allmodal ( (modal operator))\[{ .. #sw ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. switch-to-if(#sw) ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1864] synchronizedBlockEmpty, synchronizedBlockEmpty { \find(==>#allmodal ( (modal operator))\[{ .. synchronized(#se) {} ... }\] (post)) \varcond(\isLocalVariable (#se (program SimpleExpression)), ) \replacewith([]==>[not(equals(#se,null))]) ; \replacewith([]==>[#allmodal(post)]) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & runtimeExceptions:ban)}
• TestTacletEquality. [1865] synchronizedBlockEmpty2, synchronizedBlockEmpty2 { \find(#allmodal ( (modal operator))\[{ .. synchronized(#cr) {} ... }\] (post)) \replacewith(#allmodal(post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1866] synchronizedBlockEvalSync, synchronizedBlockEvalSync { \find(#allmodal ( (modal operator))\[{ .. synchronized(#nsencr) {#slist} ... }\] (post)) \varcond(\new(#loc (program Variable), \typeof(#nsencr (program NonSimpleExpressionNoClassReference))), \isLocalVariable (#nsencr (program NonSimpleExpressionNoClassReference)), ) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nsencr) #loc = #nsencr;synchronized(#loc) {#slist} ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [186] assignmentMultiplicationLong3, assignmentMultiplicationLong3 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong0*#seLong1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1870] throwBox, throwBox { \find(#box ( (modal operator))\[{throw #se;#slist}\] (post)) \replacewith(true) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1871] throwDiamond, throwDiamond { \find(#diamond ( (modal operator))\[{throw #se;#slist}\] (post)) \replacewith(false) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1872] throwLabel, throwLabel { \find(#allmodal ( (modal operator))\[{ .. #lb:throw #se; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. throw #se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1873] throwLabelBlock, throwLabelBlock { \find(#allmodal ( (modal operator))\[{ .. #lb: {throw #se;#slist} ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. throw #se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1874] throwNull, throwNull { \find(#allmodal ( (modal operator))\[{ .. throw null; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. throw new java.lang.NullPointerException (); ... }\] (post)) Choices: programRules:Java}
• TestTacletEquality. [1875] throwUnfold, throwUnfold { \find(#allmodal ( (modal operator))\[{ .. throw #nse; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v0 = #nse;throw #v0; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1876] throwUnfoldMore, throwUnfoldMore { \find(#allmodal ( (modal operator))\[{ .. throw #se; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#se (program SimpleExpression))), \isLocalVariable (#se (program SimpleExpression)), ) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#se) #v0 = #se;throw #v0; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [187] assignmentShiftLeftInt, assignmentShiftLeftInt { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt0<<#se; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftInt(#seCharByteShortInt0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [188] assignmentShiftLeftLong, assignmentShiftLeftLong { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong0<<#se; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftLong(#seLong0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [189] assignmentShiftRightInt, assignmentShiftRightInt { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt0>>#se; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [18] activeUseShiftLeft, activeUseShiftLeft { \find(#allmodal ( (modal operator))\[{ .. #sv=#left<<#right; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = #left<<#right;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [190] assignmentShiftRightLong, assignmentShiftRightLong { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong0>>#se; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightLong(#seLong0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [191] assignmentSubtractionBigint1, assignmentSubtractionBigint1 { \find(#allmodal ( (modal operator))\[{ .. #loc=#seBigint-#seAny; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(sub(#seBigint,#seAny)),#allmodal(post))) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & bigint:on)}
• TestTacletEquality. [192] assignmentSubtractionBigint2, assignmentSubtractionBigint2 { \find(#allmodal ( (modal operator))\[{ .. #loc=#seAny-#seBigint; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(sub(#seAny,#seBigint)),#allmodal(post))) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & bigint:on)}
• TestTacletEquality. [1934] tryBreak, tryBreak { \find(#allmodal ( (modal operator))\[{ .. try {break ; #slist } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. break ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1935] tryBreakLabel, tryBreakLabel { \find(#allmodal ( (modal operator))\[{ .. try {break ; #slist } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. break ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1936] tryCatchFinallyThrow, tryCatchFinallyThrow { \find(#allmodal ( (modal operator))\[{ .. try {throw #se;#slist} catch (#t #v0) { #slist1 } #cs finally { #slist2 } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. if (#se==null) { try { throw new java.lang.NullPointerException (); } catch (#t #v0) { #slist1 } #cs finally { #slist2 } } else if (#se instanceof #t) { …
• TestTacletEquality. [1937] tryCatchThrow, tryCatchThrow { \find(#allmodal ( (modal operator))\[{ .. try {throw #se;#slist} catch (#t #v0) { #slist1 } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. if (#se==null) { try { throw new java.lang.NullPointerException (); } catch (#t #v0) { #slist1 } } else if (#se instanceof #t) { #t #v0; #v0=(#t)#se; #slist1 } else { throw #se; } ... }\] (post)) \heu…
• TestTacletEquality. [1938] tryEmpty, tryEmpty { \find(#allmodal ( (modal operator))\[{ .. try {}#cs ... }\] (post)) \replacewith(#allmodal(post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1939] tryFinallyBreak, tryFinallyBreak { \find(#allmodal ( (modal operator))\[{ .. try {break ; #slist } #cs finally { #slist2 } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist2}break ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [193] assignmentSubtractionDouble, assignmentSubtractionDouble { \find(#normalassign ( (modal operator))\[{ .. #loc=#seDouble0-#seDouble1; ... }\] (post)) \varcond(\not\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [1940] tryFinallyBreakLabel, tryFinallyBreakLabel { \find(#allmodal ( (modal operator))\[{ .. try {break ; #slist } #cs finally { #slist2 } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist2}break ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1941] tryFinallyEmpty, tryFinallyEmpty { \find(#allmodal ( (modal operator))\[{ .. try {}#csfinally { #slist2 } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist2} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1942] tryFinallyReturn, tryFinallyReturn { \find(#allmodal ( (modal operator))\[{ .. try {return #se;#slist}#csfinally { #slist2 } ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#se (program SimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#se) #v0 = #se; {#slist2}return #v0; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1943] tryFinallyReturnNoValue, tryFinallyReturnNoValue { \find(#allmodal ( (modal operator))\[{ .. try {return ;#slist}#csfinally { #slist2 } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist2}return ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1944] tryFinallyThrow, tryFinallyThrow { \find(#allmodal ( (modal operator))\[{ .. try {throw #se;#slist}finally { #slist2 } ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#se (program SimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. if (#se==null) { { #slist2 } throw new java.lang.NullPointerException (); } else {#typeof (#se) #v0 = #se; { #slist2 } throw #v0; } ... }\] (post)) \heuristics(simplify_prog) Choice…
• TestTacletEquality. [1945] tryMultipleCatchThrow, tryMultipleCatchThrow { \find(#allmodal ( (modal operator))\[{ .. try {throw #se;#slist} catch (#t #v0) { #slist1 } catch (#t2 #v1) { #slist3 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. if (#se==null) { try { throw new java.lang.NullPointerException (); } catch (#t #v0) { #slist1 } catch (#t2 #v1) { #slist3 } #cs } else if (#se instanceof #t) …
• TestTacletEquality. [1946] tryReturn, tryReturn { \find(#allmodal ( (modal operator))\[{ .. try {return #se;#slist}#cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. return #se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1947] tryReturnNoValue, tryReturnNoValue { \find(#allmodal ( (modal operator))\[{ .. try {return ;#slist}#cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. return ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1948] try_continue_1, try_continue_1 { \find(#allmodal ( (modal operator))\[{ .. try {continue ; #slist } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. continue ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1949] try_continue_2, try_continue_2 { \find(#allmodal ( (modal operator))\[{ .. try {continue ; #slist } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. continue ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [194] assignmentSubtractionDoubleStrictFP, assignmentSubtractionDoubleStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc=#seDouble0-#seDouble1; ... }\] (post)) \varcond(\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(subDouble(#seDouble0,#seDouble1)),#normalassign(post))) \heuristics(executeDoubleAssignment) Choices: programRules:Java}
• TestTacletEquality. [1950] try_finally_continue_1, try_finally_continue_1 { \find(#allmodal ( (modal operator))\[{ .. try {continue ; #slist } #cs finally { #slist2 } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist2}continue ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1951] try_finally_continue_2, try_finally_continue_2 { \find(#allmodal ( (modal operator))\[{ .. try {continue ; #slist } #cs finally { #slist2 } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist2}continue ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1956] unaryMinusBigint, unaryMinusBigint { \find(#allmodal ( (modal operator))\[{ .. #loc=-#seBigint; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(neg(#seBigint)),#allmodal(post))) \heuristics(executeIntegerAssignment) Choices: (programRules:Java & bigint:on)}
• TestTacletEquality. [1957] unaryMinusDouble, unaryMinusDouble { \find(#normalassign ( (modal operator))\[{ .. #loc=-#seDouble; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusDouble(#seDouble)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [1958] unaryMinusFloat, unaryMinusFloat { \find(#normalassign ( (modal operator))\[{ .. #loc=-#seFloat; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusFloat(#seFloat)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [1959] unaryMinusInt, unaryMinusInt { \find(#normalassign ( (modal operator))\[{ .. #loc=-#seCharByteShortInt; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusInt(#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [195] assignmentSubtractionFloat, assignmentSubtractionFloat { \find(#normalassign ( (modal operator))\[{ .. #loc=#seFloat0-#seFloat1; ... }\] (post)) \varcond(\not\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [1960] unaryMinusLong, unaryMinusLong { \find(#normalassign ( (modal operator))\[{ .. #loc=-#seLong; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusLong(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [196] assignmentSubtractionFloatStrictFP, assignmentSubtractionFloatStrictFP { \find(#normalassign ( (modal operator))\[{ .. #loc=#seFloat0-#seFloat1; ... }\] (post)) \varcond(\isStrictFp, ) \replacewith(update-application(elem-update(#loc (program Variable))(subFloat(#seFloat0,#seFloat1)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [1977] unusedLabel, unusedLabel { \find(#allmodal ( (modal operator))\[{ .. #lb:#s ... }\] (post)) \varcond(\not\freeLabelIn (#lb,#s), ) \replacewith(#allmodal ( (modal operator))\[{ .. #s ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1978] unwindLoopScope, unwindLoopScope { \find(#allmodal ( (modal operator))\[{ .. while ( #nse ) #body ... }\] (post)) \varcond(\new(#x (program Variable), (type, sort): (boolean,boolean))) \replacewith(#allmodal ( (modal operator))\[{ .. boolean #x;loop-scope(#x) {if (#nse) { #body continue ; } else { break ; } } ... }\] (and(imp(equals(#x<<loopScopeIndex>>,TRUE),post),imp(equals(#x<<loopScopeIndex>>,FALSE),#allmodal ( (modal operator))\[{ .. #reattachLoopInvariant(wh…
• TestTacletEquality. [1979] variableDeclaration, variableDeclaration { \find(#allmodal ( (modal operator))\[{ .. #t #v0; ... }\] (post)) \addprogvars {#v0 (program Variable)} \replacewith(#allmodal(post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [197] assignmentSubtractionInt, assignmentSubtractionInt { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt0-#seCharByteShortInt1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1980] variableDeclarationAssign, variableDeclarationAssign { \find(#allmodal ( (modal operator))\[{ .. #t #v0 = #vi; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #t #v0;#v0=#vi; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1981] variableDeclarationFinal, variableDeclarationFinal { \find(#allmodal ( (modal operator))\[{ .. final#t #v0; ... }\] (post)) \addprogvars {#v0 (program Variable)} \replacewith(#allmodal(post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1982] variableDeclarationFinalAssign, variableDeclarationFinalAssign { \find(#allmodal ( (modal operator))\[{ .. final#t #v0 = #vi; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. final#t #v0;#v0=#vi; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1983] variableDeclarationGhost, variableDeclarationGhost { \find(#allmodal ( (modal operator))\[{ .. ghost#t #v0; ... }\] (post)) \addprogvars {#v0 (program Variable)} \replacewith(#allmodal(post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1984] variableDeclarationGhostAssign, variableDeclarationGhostAssign { \find(#allmodal ( (modal operator))\[{ .. ghost#t #v0 = #vi; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. ghost#t #v0;#v0=#vi; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [1985] variableDeclarationMult, variableDeclarationMult { \find(#allmodal ( (modal operator))\[{ .. #multvardecl ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. multiple-var-decl(#multvardecl) ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [198] assignmentSubtractionLong, assignmentSubtractionLong { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt-#seLong; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seCharByteShortInt,#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [1999] wideningCastIntToFloat, wideningCastIntToFloat { \find(#normalassign ( (modal operator))\[{ .. #loc=(float)#seCharByteShortInt; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(float::cast(#seCharByteShortInt)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [199] assignmentSubtractionLong2, assignmentSubtractionLong2 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong-#seCharByteShortInt; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong,#seCharByteShortInt)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [19] activeUseShiftRight, activeUseShiftRight { \find(#allmodal ( (modal operator))\[{ .. #sv=#left>>#right; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = #left>>#right;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [1] abortJavaCardTransactionAPI, abortJavaCardTransactionAPI { \find(==>#allmodal ( (modal operator))\[{ .. #jcsystemType.#abortTransaction()@#jcsystemType; ... }\] (post)) \replacewith([]==>[#allmodal ( (modal operator))\[{ .. #abortJavaCardTransaction; ... }\] (post)]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)}
• TestTacletEquality. [2000] wideningCastLongToFloat, wideningCastLongToFloat { \find(#normalassign ( (modal operator))\[{ .. #loc=(float)#seLong; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(float::cast(#seLong)),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [2001] widening_identity_cast_1, widening_identity_cast_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=(byte)#seByte; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#seByte; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [2002] widening_identity_cast_10, widening_identity_cast_10 { \find(#allmodal ( (modal operator))\[{ .. #lhs=(long)#seByteShortInt; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#seByteShortInt; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [2003] widening_identity_cast_11, widening_identity_cast_11 { \find(#allmodal ( (modal operator))\[{ .. #lhs=(long)#seLong; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#seLong; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [2004] widening_identity_cast_12, widening_identity_cast_12 { \find(#allmodal ( (modal operator))\[{ .. #lhs=(int)#seChar; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#seChar; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [2005] widening_identity_cast_13, widening_identity_cast_13 { \find(#allmodal ( (modal operator))\[{ .. #lhs=(long)#seChar; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#seChar; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [2006] widening_identity_cast_2, widening_identity_cast_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=(short)#seByte; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#seByte; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [2007] widening_identity_cast_3, widening_identity_cast_3 { \find(#allmodal ( (modal operator))\[{ .. #lhs=(char)#seChar; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#seChar; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [2008] widening_identity_cast_4, widening_identity_cast_4 { \find(#allmodal ( (modal operator))\[{ .. #lhs=(short)#seShort; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#seShort; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [2009] widening_identity_cast_5, widening_identity_cast_5 { \find(#allmodal ( (modal operator))\[{ .. #lhs=(int)#seByteShortInt; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#seByteShortInt; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [200] assignmentSubtractionLong3, assignmentSubtractionLong3 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong0-#seLong1; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong0,#seLong1)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [2010] widening_identity_cast_bigint, widening_identity_cast_bigint { \find(#allmodal ( (modal operator))\[{ .. #lhs=(\bigint)#seAny; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#seAny; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & bigint:on)}
• TestTacletEquality. [201] assignmentUnsignedShiftRightInt, assignmentUnsignedShiftRightInt { \find(#normalassign ( (modal operator))\[{ .. #loc=#seCharByteShortInt0>>>#se; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [202] assignmentUnsignedShiftRightLong, assignmentUnsignedShiftRightLong { \find(#normalassign ( (modal operator))\[{ .. #loc=#seLong0>>>#se; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightLong(#seLong0,#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [203] assignment_array2, assignment_array2 { \find(==>#allmodal ( (modal operator))\[{ .. #v=#v0[#se]; ... }\] (post)) \varcond(\hasSort(\elemSort(#v0 (program Variable)), G), ) \add [and(not(equals(#v0,null)),or(leq(length(#v0),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v0,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(#v (program Variable))(G::select(heap,#v0,arr(#se))),#allmodal(post))]) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRu…
• TestTacletEquality. [204] assignment_read_attribute, assignment_read_attribute { \find(==>#allmodal ( (modal operator))\[{ .. #v0=#v.#a; ... }\] (post)) \varcond( \not \static(#a (program Variable)), \not \isArrayLength(#a (program Variable)), \hasSort(#a (program Variable), G), \not\isThisReference (#v (program Variable)), ) \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(#v0 (program Variable))(G::select(heap,#v,#memberPVToField(#a))),#allmodal(post))]) \heuristics(simplify_prog_subset, simplify_…
• TestTacletEquality. [205] assignment_read_attribute_this, assignment_read_attribute_this { \find(==>#allmodal ( (modal operator))\[{ .. #v0=#v.#a; ... }\] (post)) \varcond( \not \static(#a (program Variable)), \not \isArrayLength(#a (program Variable)), \hasSort(#a (program Variable), G), \isThisReference (#v (program Variable)), ) \replacewith([]==>[update-application(elem-update(#v0 (program Variable))(G::select(heap,#v,#memberPVToField(#a))),#allmodal(post))]) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & runtimeExceptions:ba…
• TestTacletEquality. [206] assignment_read_length, assignment_read_length { \find(==>#allmodal ( (modal operator))\[{ .. #v0=#v.#length; ... }\] (post)) \varcond(\not\isThisReference (#v (program Variable)), ) \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(#v0 (program Variable))(length(#v)),#allmodal(post))]) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & runtimeExceptions:ban)}
• TestTacletEquality. [207] assignment_read_length_this, assignment_read_length_this { \find(#allmodal ( (modal operator))\[{ .. #v0=#v.#length; ... }\] (post)) \sameUpdateLevel\varcond(\isThisReference (#v (program Variable)), ) \replacewith(update-application(elem-update(#v0 (program Variable))(length(#v)),#allmodal(post))) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [208] assignment_read_static_attribute, assignment_read_static_attribute { \find(#allmodal ( (modal operator))\[{ .. #v0=@(#sv); ... }\] (post)) \sameUpdateLevel\varcond(\hasSort(#sv (program StaticVariable), G), ) \replacewith(update-application(elem-update(#v0 (program Variable))(G::select(heap,null,#memberPVToField(#sv))),#allmodal(post))) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [209] assignment_read_static_attribute_with_variable_prefix, assignment_read_static_attribute_with_variable_prefix { \find(#allmodal ( (modal operator))\[{ .. #loc=@(#v.#sv); ... }\] (post)) \varcond(\hasSort(#sv (program StaticVariable), G), ) \replacewith(update-application(elem-update(#loc (program Variable))(G::select(heap,#v,#memberPVToField(#sv))),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [20] activeUseShortCast, activeUseShortCast { \find(#allmodal ( (modal operator))\[{ .. #sv=(short)#seIntLong; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = (short)#seIntLong;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [210] assignment_to_primitive_array_component, assignment_to_primitive_array_component { \find(==>#normal ( (modal operator))\[{ .. #v[#se]=#se0; ... }\] (post)) \varcond( \not \isReferenceArray(#v (program Variable)), ) \add [and(not(equals(#v,null)),or(leq(length(#v),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,arr(#se),#se0)),#normal(post))]) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRul…
• TestTacletEquality. [211] assignment_to_primitive_array_component_transaction, assignment_to_primitive_array_component_transaction { \find(==>#transaction ( (modal operator))\[{ .. #v[#se]=#se0; ... }\] (post)) \varcond( \not \isReferenceArray(#v (program Variable)), ) \add [and(not(equals(#v,null)),or(leq(length(#v),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,arr(#se),#se0)),update-application(elem-update(savedHeap)(if-then-else(equals(int::sel…
• TestTacletEquality. [212] assignment_to_reference_array_component, assignment_to_reference_array_component { \find(==>#normal ( (modal operator))\[{ .. #v[#se]=#se0; ... }\] (post)) \varcond(\isReferenceArray(#v (program Variable)), ) \add [and(and(and(not(equals(#v,null)),lt(#se,length(#v))),geq(#se,Z(0(#)))),not(arrayStoreValid(#v,#se0)))]==>[] \replacewith([]==>[false]) ; \add [and(not(equals(#v,null)),or(leq(length(#v),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[update-applicatio…
• TestTacletEquality. [213] assignment_to_reference_array_component_transaction, assignment_to_reference_array_component_transaction { \find(==>#transaction ( (modal operator))\[{ .. #v[#se]=#se0; ... }\] (post)) \varcond(\isReferenceArray(#v (program Variable)), ) \add [and(and(and(not(equals(#v,null)),lt(#se,length(#v))),geq(#se,Z(0(#)))),not(arrayStoreValid(#v,#se0)))]==>[] \replacewith([]==>[false]) ; \add [and(not(equals(#v,null)),or(leq(length(#v),#se),lt(#se,Z(0(#)))))]==>[] \replacewith([]==>[false]) ; \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[…
• TestTacletEquality. [214] assignment_write_array_this_access_normalassign, assignment_write_array_this_access_normalassign { \find(#allmodal ( (modal operator))\[{ .. this[#se]=#se0; ... }\] (post)) \replacewith(imp(and(lt(#se,length(#v)),lt(Z(neglit(1(#))),#se)),update-application(elem-update(heap)(store(heap,#v,arr(#se),#se0)),#allmodal(post)))) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & permissions:off)}
• TestTacletEquality. [215] assignment_write_attribute, assignment_write_attribute { \find(==>#allmodal ( (modal operator))\[{ .. #v.#a=#se; ... }\] (post)) \varcond( \not \static(#a (program Variable)), \not\isThisReference (#v (program Variable)), ) \add [equals(#v,null)]==>[] \replacewith([]==>[false]) ; \replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,#memberPVToField(#a),#se)),#allmodal(post))]) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & runtimeExceptions:ban)}
• TestTacletEquality. [216] assignment_write_attribute_this, assignment_write_attribute_this { \find(==>#allmodal ( (modal operator))\[{ .. #v.#a=#se; ... }\] (post)) \varcond( \not \static(#a (program Variable)), \isThisReference (#v (program Variable)), ) \replacewith([]==>[update-application(elem-update(heap)(store(heap,#v,#memberPVToField(#a),#se)),#allmodal(post))]) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & runtimeExceptions:ban)}
• TestTacletEquality. [217] assignment_write_static_attribute, assignment_write_static_attribute { \find(#allmodal ( (modal operator))\[{ .. @(#sv)=#se; ... }\] (post)) \replacewith(update-application(elem-update(heap)(store(heap,null,#memberPVToField(#sv),#se)),#allmodal(post))) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [218] assignment_write_static_attribute_with_variable_prefix, assignment_write_static_attribute_with_variable_prefix { \find(#allmodal ( (modal operator))\[{ .. @(#v.#sv)=#se; ... }\] (post)) \replacewith(update-application(elem-update(heap)(store(heap,#v,#memberPVToField(#sv),#se)),#allmodal(post))) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [21] activeUseStaticFieldReadAccess, activeUseStaticFieldReadAccess { \find(#allmodal ( (modal operator))\[{ .. #lhs=#sv; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=@(#sv); ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [22] activeUseStaticFieldReadAccess2, activeUseStaticFieldReadAccess2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#v.#sv; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=@(#sv); ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [23] activeUseStaticFieldWriteAccess, activeUseStaticFieldWriteAccess { \find(#allmodal ( (modal operator))\[{ .. #sv=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [24] activeUseStaticFieldWriteAccess2, activeUseStaticFieldWriteAccess2 { \find(#allmodal ( (modal operator))\[{ .. #v.#sv=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [253] beginJavaCardTransactionAPI, beginJavaCardTransactionAPI { \find(==>#allmodal ( (modal operator))\[{ .. #jcsystemType.#beginTransaction()@#jcsystemType; ... }\] (post)) \replacewith([]==>[#allmodal ( (modal operator))\[{ .. #beginJavaCardTransaction; ... }\] (post)]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)}
• TestTacletEquality. [254] beginJavaCardTransactionBox, beginJavaCardTransactionBox { \find(==>\[{ .. #beginJavaCardTransaction; ... }\] (post)) \replacewith([]==>[update-application(elem-update(savedHeap)(heap),box_transaction(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)}
• TestTacletEquality. [255] beginJavaCardTransactionDiamond, beginJavaCardTransactionDiamond { \find(==>\<{ .. #beginJavaCardTransaction; ... }\> (post)) \replacewith([]==>[update-application(elem-update(savedHeap)(heap),diamond_transaction(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)}
• TestTacletEquality. [25] activeUseStaticFieldWriteAccess3, activeUseStaticFieldWriteAccess3 { \find(#allmodal ( (modal operator))\[{ .. #sv=#arr[#idx]; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = #arr[#idx];@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [268] bitwiseNegation, bitwiseNegation { \find(#normalassign ( (modal operator))\[{ .. #loc=~#se; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseNegation(#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [269] blockBreak, blockBreak { \find(#allmodal ( (modal operator))\[{ .. {break ; #slist } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. break ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [26] activeUseStaticFieldWriteAccess4, activeUseStaticFieldWriteAccess4 { \find(#allmodal ( (modal operator))\[{ .. #v.#sv=#arr[#idx]; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = #arr[#idx];@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [270] blockBreakLabel, blockBreakLabel { \find(#allmodal ( (modal operator))\[{ .. #lb0: {break ; #slist } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. do-break(#lb0:break ; ) ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [271] blockBreakLabeled, blockBreakLabeled { \find(#allmodal ( (modal operator))\[{ .. {break ; #slist } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. break ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [272] blockBreakNoLabel, blockBreakNoLabel { \find(#allmodal ( (modal operator))\[{ .. {break ; #slist } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. break ; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [273] blockContinue, blockContinue { \find(#allmodal ( (modal operator))\[{ .. {continue ; #slist } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. continue ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [274] blockContinueLabeled, blockContinueLabeled { \find(#allmodal ( (modal operator))\[{ .. {continue ; #slist } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. continue ; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [275] blockEmpty, blockEmpty { \find(#allmodal ( (modal operator))\[{ .. {} ... }\] (post)) \replacewith(#allmodal(post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [276] blockEmptyLabel, blockEmptyLabel { \find(#allmodal ( (modal operator))\[{ .. #lb: {} ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {} ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [277] blockReturn, blockReturn { \find(#allmodal ( (modal operator))\[{ .. {return #se;#slist} ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. return #se; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [278] blockReturnLabel1, blockReturnLabel1 { \find(#allmodal ( (modal operator))\[{ .. #lb:return #se; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. return #se; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [279] blockReturnLabel2, blockReturnLabel2 { \find(#allmodal ( (modal operator))\[{ .. #lb: {return #se;#slist} ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. return #se; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [27] activeUseStaticFieldWriteAccess5, activeUseStaticFieldWriteAccess5 { \find(#allmodal ( (modal operator))\[{ .. #sv=#v1.#a; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#a (program Variable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#a) #v0 = #v1.#a;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [280] blockReturnNoValue, blockReturnNoValue { \find(#allmodal ( (modal operator))\[{ .. {return ;#slist} ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. return ; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [281] blockThrow, blockThrow { \find(#allmodal ( (modal operator))\[{ .. {throw #e;#slist} ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. throw #e; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [288] boxToDiamond, boxToDiamond { \find(\[{ .. #s ... }\] (post)) \replacewith(not(\<{ .. #s ... }\> (not(post)))) \heuristics(boxDiamondConv) Choices: programRules:Java}
• TestTacletEquality. [289] boxToDiamondTransaction, boxToDiamondTransaction { \find(box_transaction\[{ .. #s ... }\] (post)) \replacewith(not(diamond_transaction\[{ .. #s ... }\] (not(post)))) \heuristics(boxDiamondConv) Choices: programRules:Java}
• TestTacletEquality. [28] activeUseStaticFieldWriteAccess6, activeUseStaticFieldWriteAccess6 { \find(#allmodal ( (modal operator))\[{ .. #v.#sv=#v1.#a; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#a (program Variable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#a) #v0 = #v1.#a;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [290] box_and_left, box_and_left { \find(#box ( (modal operator))\[{ .. #s ... }\] (and(post,post1))==>) \replacewith([and(#box ( (modal operator))\[{ .. #s ... }\] (post),#box ( (modal operator))\[{ .. #s ... }\] (post1))]==>[]) Choices: programRules:Java}
• TestTacletEquality. [291] box_and_right, box_and_right { \find(==>#box ( (modal operator))\[{ .. #s ... }\] (and(post,post1))) \replacewith([]==>[#box ( (modal operator))\[{ .. #s ... }\] (post1)]) ; \replacewith([]==>[#box ( (modal operator))\[{ .. #s ... }\] (post)]) Choices: programRules:Java}
• TestTacletEquality. [292] box_or_left, box_or_left { \find(#box ( (modal operator))\[{ .. #s ... }\] (or(post,post1))==>) \replacewith([or(#box ( (modal operator))\[{ .. #s ... }\] (post),#box ( (modal operator))\[{ .. #s ... }\] (post1))]==>[]) Choices: programRules:Java}
• TestTacletEquality. [293] box_or_right, box_or_right { \find(==>#box ( (modal operator))\[{ .. #s ... }\] (or(post,post1))) \replacewith([]==>[or(#box ( (modal operator))\[{ .. #s ... }\] (post),#box ( (modal operator))\[{ .. #s ... }\] (post1))]) Choices: programRules:Java}
• TestTacletEquality. [294] box_true, box_true { \find(#box ( (modal operator))\[{ .. #s ... }\] (true)) \replacewith(true) \heuristics(modal_tautology) Choices: programRules:Java}
• TestTacletEquality. [29] activeUseSubtraction, activeUseSubtraction { \find(#allmodal ( (modal operator))\[{ .. #sv=#left-#right; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = #left-#right;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [2] abortJavaCardTransactionBox, abortJavaCardTransactionBox { \find(==>box_transaction\[{ .. #abortJavaCardTransaction; ... }\] (post)) \replacewith([]==>[update-application(elem-update(heap)(anon(savedHeap,allObjects(java.lang.Object::<transactionConditionallyUpdated>),heap)),box(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)}
• TestTacletEquality. [30] activeUseUnaryMinus, activeUseUnaryMinus { \find(#allmodal ( (modal operator))\[{ .. #sv=-#left; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = -#left;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [315] break, break { \find(#allmodal ( (modal operator))\[{ .. #lb0:break ; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. do-break(#lb0:break ; ) ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [31] activeUseUnsignedShiftRight, activeUseUnsignedShiftRight { \find(#allmodal ( (modal operator))\[{ .. #sv=#left>>>#right; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = #left>>>#right; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [377] castLongToFloatAddition2, castLongToFloatAddition2 { \find(#normalassign ( (modal operator))\[{ .. #loc=#seFloat+#seLong; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaAddFloat(#seFloat,float::cast(#seLong))),#normalassign(post))) \heuristics(executeFloatAssignment) Choices: programRules:Java}
• TestTacletEquality. [378] castToBoolean, castToBoolean { \find(#allmodal ( (modal operator))\[{ .. #lhs=(boolean)#exBool; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#exBool; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [396] commitJavaCardTransactionAPI, commitJavaCardTransactionAPI { \find(==>#allmodal ( (modal operator))\[{ .. #jcsystemType.#commitTransaction()@#jcsystemType; ... }\] (post)) \replacewith([]==>[#allmodal ( (modal operator))\[{ .. #commitJavaCardTransaction; ... }\] (post)]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)}
• TestTacletEquality. [397] commitJavaCardTransactionBox, commitJavaCardTransactionBox { \find(==>box_transaction\[{ .. #commitJavaCardTransaction; ... }\] (post)) \replacewith([]==>[box(post)]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)}
• TestTacletEquality. [398] commitJavaCardTransactionDiamond, commitJavaCardTransactionDiamond { \find(==>diamond_transaction\[{ .. #commitJavaCardTransaction; ... }\] (post)) \replacewith([]==>[diamond(post)]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)}
• TestTacletEquality. [3] abortJavaCardTransactionDiamond, abortJavaCardTransactionDiamond { \find(==>diamond_transaction\[{ .. #abortJavaCardTransaction; ... }\] (post)) \replacewith([]==>[update-application(elem-update(heap)(anon(savedHeap,allObjects(java.lang.Object::<transactionConditionallyUpdated>),heap)),diamond(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)}
• TestTacletEquality. [408] compound_addition_1, compound_addition_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse+#se; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=#v+#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [409] compound_addition_2, compound_addition_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e+#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse) #v1 = #nse;#lhs=#v0+#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [410] compound_assignment_1_new, compound_assignment_1_new { \find(#allmodal ( (modal operator))\[{ .. #lhs=!#seBool; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(equals(#seBool,TRUE),FALSE,TRUE)),#allmodal(post))) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [411] compound_assignment_2, compound_assignment_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=!#nseBool; ... }\] (post)) \varcond(\new(#v (program Variable), (type, sort): (boolean,boolean))) \replacewith(#allmodal ( (modal operator))\[{ .. boolean #v = #nseBool;#lhs=!#v; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [412] compound_assignment_3_mixed, compound_assignment_3_mixed { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nseBool0&&#seBool1; ... }\] (post)) \varcond(\new(#v0 (program Variable), (type, sort): (boolean,boolean))) \replacewith(#allmodal ( (modal operator))\[{ .. boolean #v0 = #nseBool0;#lhs=#v0&&#seBool1; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [413] compound_assignment_3_nonsimple, compound_assignment_3_nonsimple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#exBool0&&#nseBool1; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. if (!#exBool0) #lhs=false; else #lhs=#nseBool1; ... }\] (post)) \heuristics(split_if, simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [414] compound_assignment_3_simple, compound_assignment_3_simple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seBool0&&#seBool1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(equals(#seBool0,TRUE),if-then-else(equals(#seBool1,TRUE),TRUE,FALSE),FALSE)),#allmodal(post))) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [415] compound_assignment_4_nonsimple, compound_assignment_4_nonsimple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nseBool0&#exBool1; ... }\] (post)) \varcond(\new(#v1 (program Variable), (type, sort): (boolean,boolean)), \new(#v0 (program Variable), (type, sort): (boolean,boolean))) \replacewith(#allmodal ( (modal operator))\[{ .. boolean #v0 = #nseBool0;boolean #v1 = #exBool1;#lhs=#v0&#v1; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [416] compound_assignment_4_simple, compound_assignment_4_simple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seBool0&#seBool1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(equals(#seBool0,TRUE),if-then-else(equals(#seBool1,TRUE),TRUE,FALSE),FALSE)),#allmodal(post))) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [417] compound_assignment_5_mixed, compound_assignment_5_mixed { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nseBool0||#seBool1; ... }\] (post)) \varcond(\new(#v0 (program Variable), (type, sort): (boolean,boolean))) \replacewith(#allmodal ( (modal operator))\[{ .. boolean #v0 = #nseBool0;#lhs=#v0||#seBool1; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [418] compound_assignment_5_nonsimple, compound_assignment_5_nonsimple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#exBool0||#nseBool1; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. if (#exBool0) #lhs=true; else #lhs=#nseBool1; ... }\] (post)) \heuristics(split_if, simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [419] compound_assignment_5_simple, compound_assignment_5_simple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seBool0||#seBool1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(equals(#seBool0,TRUE),TRUE,if-then-else(equals(#seBool1,TRUE),TRUE,FALSE))),#allmodal(post))) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [420] compound_assignment_6_nonsimple, compound_assignment_6_nonsimple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nseBool0|#exBool1; ... }\] (post)) \varcond(\new(#v1 (program Variable), (type, sort): (boolean,boolean)), \new(#v0 (program Variable), (type, sort): (boolean,boolean))) \replacewith(#allmodal ( (modal operator))\[{ .. boolean #v0 = #nseBool0;boolean #v1 = #exBool1;#lhs=#v0|#v1; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [421] compound_assignment_6_simple, compound_assignment_6_simple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seBool0|#seBool1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(equals(#seBool0,TRUE),TRUE,if-then-else(equals(#seBool1,TRUE),TRUE,FALSE))),#allmodal(post))) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [422] compound_assignment_op_and, compound_assignment_op_and { \find(#allmodal ( (modal operator))\[{ .. #lhs&=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=(#typeof(#lhs))(#lhs&(#e)); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]&#e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [424] compound_assignment_op_and_attr, compound_assignment_op_and_attr { \find(#allmodal ( (modal operator))\[{ .. #e0.#attribute&=#e; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v = #e0;#v.#attribute=(#typeof(#attribute))(#v.#attribute&#e); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [425] compound_assignment_op_div, compound_assignment_op_div { \find(#allmodal ( (modal operator))\[{ .. #lhs/=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=(#typeof(#lhs))(#lhs/(#e)); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]/#e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [427] compound_assignment_op_div_attr, compound_assignment_op_div_attr { \find(#allmodal ( (modal operator))\[{ .. #e0.#attribute/=#e; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v = #e0;#v.#attribute=(#typeof(#attribute))(#v.#attribute/#e); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [428] compound_assignment_op_minus, compound_assignment_op_minus { \find(#allmodal ( (modal operator))\[{ .. #lhs-=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=(#typeof(#lhs))(#lhs-(#e)); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]-#e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [430] compound_assignment_op_minus_attr, compound_assignment_op_minus_attr { \find(#allmodal ( (modal operator))\[{ .. #e0.#attribute-=#e; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v = #e0;#v.#attribute=(#typeof(#attribute))(#v.#attribute-#e); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [431] compound_assignment_op_mod, compound_assignment_op_mod { \find(#allmodal ( (modal operator))\[{ .. #lhs%=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=(#typeof(#lhs))(#lhs%(#e)); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]%#e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [433] compound_assignment_op_mod_attr, compound_assignment_op_mod_attr { \find(#allmodal ( (modal operator))\[{ .. #e0.#attribute%=#e; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v = #e0;#v.#attribute=(#typeof(#attribute))(#v.#attribute%#e); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [434] compound_assignment_op_mul, compound_assignment_op_mul { \find(#allmodal ( (modal operator))\[{ .. #lhs*=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=(#typeof(#lhs))(#lhs*(#e)); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]*#e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [436] compound_assignment_op_mul_attr, compound_assignment_op_mul_attr { \find(#allmodal ( (modal operator))\[{ .. #e0.#attribute*=#e; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v = #e0;#v.#attribute=(#typeof(#attribute))(#v.#attribute*#e); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [437] compound_assignment_op_or, compound_assignment_op_or { \find(#allmodal ( (modal operator))\[{ .. #lhs|=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=(#typeof(#lhs))(#lhs|(#e)); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]|#e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [439] compound_assignment_op_or_attr, compound_assignment_op_or_attr { \find(#allmodal ( (modal operator))\[{ .. #e0.#attribute|=#e; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v = #e0;#v.#attribute=(#typeof(#attribute))(#v.#attribute|#e); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [440] compound_assignment_op_plus, compound_assignment_op_plus { \find(#allmodal ( (modal operator))\[{ .. #lhs+=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=(#typeof(#lhs))(#lhs+(#e)); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]+#e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [442] compound_assignment_op_plus_attr, compound_assignment_op_plus_attr { \find(#allmodal ( (modal operator))\[{ .. #e0.#attribute+=#e; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v = #e0;#v.#attribute=(#typeof(#attribute))(#v.#attribute+#e); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [443] compound_assignment_op_shiftleft, compound_assignment_op_shiftleft { \find(#allmodal ( (modal operator))\[{ .. #lhs<<=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=(#typeof(#lhs))(#lhs<<(#e)); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]<<#e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [445] compound_assignment_op_shiftleft_attr, compound_assignment_op_shiftleft_attr { \find(#allmodal ( (modal operator))\[{ .. #e0.#attribute<<=#e; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v = #e0;#v.#attribute=(#typeof(#attribute))(#v.#attribute<<#e); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [446] compound_assignment_op_shiftright, compound_assignment_op_shiftright { \find(#allmodal ( (modal operator))\[{ .. #lhs>>=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=(#typeof(#lhs))(#lhs>>(#e)); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]>>#e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [448] compound_assignment_op_shiftright_attr, compound_assignment_op_shiftright_attr { \find(#allmodal ( (modal operator))\[{ .. #e0.#attribute>>=#e; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v = #e0;#v.#attribute=(#typeof(#attribute))(#v.#attribute>>#e); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [449] compound_assignment_op_unsigned_shiftright, compound_assignment_op_unsigned_shiftright { \find(#allmodal ( (modal operator))\[{ .. #lhs>>>=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=(#typeof(#lhs))(#lhs>>>(#e)); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]>>>#e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [451] compound_assignment_op_unsigned_shiftright_attr, compound_assignment_op_unsigned_shiftright_attr { \find(#allmodal ( (modal operator))\[{ .. #e0.#attribute>>>=#e; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v = #e0;#v.#attribute=(#typeof(#attribute))(#v.#attribute>>>#e); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [452] compound_assignment_op_xor, compound_assignment_op_xor { \find(#allmodal ( (modal operator))\[{ .. #lhs^=#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=(#typeof(#lhs))(#lhs^(#e)); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]^#e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [454] compound_assignment_op_xor_attr, compound_assignment_op_xor_attr { \find(#allmodal ( (modal operator))\[{ .. #e0.#attribute^=#e; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v = #e0;#v.#attribute=(#typeof(#attribute))(#v.#attribute^#e); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [455] compound_assignment_xor_nonsimple, compound_assignment_xor_nonsimple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nseBool0^#exBool1; ... }\] (post)) \varcond(\new(#v1 (program Variable), (type, sort): (boolean,boolean)), \new(#v0 (program Variable), (type, sort): (boolean,boolean))) \replacewith(#allmodal ( (modal operator))\[{ .. boolean #v0 = #nseBool0;boolean #v1 = #exBool1;#lhs=#v0^#v1; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [456] compound_assignment_xor_simple, compound_assignment_xor_simple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seBool0^#seBool1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(equals(#seBool0,#seBool1),FALSE,TRUE)),#allmodal(post))) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [457] compound_binary_AND_1, compound_binary_AND_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse&#se; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=#v&#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [458] compound_binary_AND_2, compound_binary_AND_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e&#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse) #v1 = #nse;#lhs=#v0&#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [459] compound_binary_OR_1, compound_binary_OR_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse|#se; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=#v|#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [460] compound_binary_OR_2, compound_binary_OR_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e|#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse) #v1 = #nse;#lhs=#v0|#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [461] compound_binary_XOR_1, compound_binary_XOR_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse^#se; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=#v^#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [462] compound_binary_XOR_2, compound_binary_XOR_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e^#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse) #v1 = #nse;#lhs=#v0^#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [463] compound_binary_neg, compound_binary_neg { \find(#allmodal ( (modal operator))\[{ .. #lhs=~#nse; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v0 = #nse;#lhs=~#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [464] compound_byte_cast_expression, compound_byte_cast_expression { \find(#allmodal ( (modal operator))\[{ .. #lhs=(byte)#nse; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=(byte)#v; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [465] compound_division_1, compound_division_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse/#se; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=#v/#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [466] compound_division_2, compound_division_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e/#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse) #v1 = #nse;#lhs=#v0/#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [467] compound_double_cast_expression, compound_double_cast_expression { \find(#normalassign ( (modal operator))\[{ .. #loc=(double)#nse; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#normalassign ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#loc=(double)#v; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [468] compound_equality_comparison_1, compound_equality_comparison_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse0==#se; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse0 (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse0) #v0 = #nse0;#lhs=#v0==#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [469] compound_equality_comparison_2, compound_equality_comparison_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e==#nse0; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse0 (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse0) #v1 = #nse0;#lhs=#v0==#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [470] compound_float_cast_expression, compound_float_cast_expression { \find(#normalassign ( (modal operator))\[{ .. #loc=(float)#nse; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#normalassign ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#loc=(float)#v; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [471] compound_greater_equal_than_comparison_1, compound_greater_equal_than_comparison_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse0>=#se; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse0 (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse0) #v0 = #nse0;#lhs=#v0>=#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [472] compound_greater_equal_than_comparison_2, compound_greater_equal_than_comparison_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e>=#nse0; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse0 (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse0) #v1 = #nse0;#lhs=#v0>=#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [473] compound_greater_than_comparison_1, compound_greater_than_comparison_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse0>#se; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse0 (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse0) #v0 = #nse0;#lhs=#v0>#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [474] compound_greater_than_comparison_2, compound_greater_than_comparison_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e>#nse0; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse0 (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse0) #v1 = #nse0;#lhs=#v0>#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [475] compound_inequality_comparison_1, compound_inequality_comparison_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse0!=#se; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse0 (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse0) #v0 = #nse0;#lhs=#v0!=#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [476] compound_inequality_comparison_2, compound_inequality_comparison_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e!=#nse0; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse0 (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse0) #v1 = #nse0;#lhs=#v0!=#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [477] compound_int_cast_expression, compound_int_cast_expression { \find(#allmodal ( (modal operator))\[{ .. #lhs=(int)#nse; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=(int)#v; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [478] compound_invert_bits, compound_invert_bits { \find(#allmodal ( (modal operator))\[{ .. #lhs=~#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v1 = #nse;#lhs=~#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [479] compound_less_equal_than_comparison_1, compound_less_equal_than_comparison_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse0<=#se; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse0 (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse0) #v0 = #nse0;#lhs=#v0<=#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [480] compound_less_equal_than_comparison_2, compound_less_equal_than_comparison_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e<=#nse0; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse0 (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse0) #v1 = #nse0;#lhs=#v0<=#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [481] compound_less_than_comparison_1, compound_less_than_comparison_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse0<#se; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse0 (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse0) #v0 = #nse0;#lhs=#v0<#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [482] compound_less_than_comparison_2, compound_less_than_comparison_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e<#nse0; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse0 (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse0) #v1 = #nse0;#lhs=#v0<#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [483] compound_long_cast_expression, compound_long_cast_expression { \find(#allmodal ( (modal operator))\[{ .. #lhs=(long)#nse; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=(long)#v; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [484] compound_modulo_1, compound_modulo_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse%#se; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=#v%#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [485] compound_modulo_2, compound_modulo_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e%#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse) #v1 = #nse;#lhs=#v0%#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [486] compound_multiplication_1, compound_multiplication_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse*#se; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=#v*#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [487] compound_multiplication_2, compound_multiplication_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e*#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse) #v1 = #nse;#lhs=#v0*#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [488] compound_reference_cast_expression, compound_reference_cast_expression { \find(#allmodal ( (modal operator))\[{ .. #lhs=(#npit)#nse; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=(#npit)#v; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [489] compound_shiftleft_1, compound_shiftleft_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse<<#se; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=#v<<#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [490] compound_shiftleft_2, compound_shiftleft_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e<<#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse) #v1 = #nse;#lhs=#v0<<#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [491] compound_shiftright_1, compound_shiftright_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse>>#se; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=#v>>#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [492] compound_shiftright_2, compound_shiftright_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e>>#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse) #v1 = #nse;#lhs=#v0>>#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [493] compound_short_cast_expression, compound_short_cast_expression { \find(#allmodal ( (modal operator))\[{ .. #lhs=(short)#nse; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=(short)#v; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [494] compound_subtraction_1, compound_subtraction_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse-#se; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=#v-#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [495] compound_subtraction_2, compound_subtraction_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e-#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse) #v1 = #nse;#lhs=#v0-#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [496] compound_unary_minus_eval, compound_unary_minus_eval { \find(#allmodal ( (modal operator))\[{ .. #lhs=-#nse; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v0 = #nse;#lhs=-#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
• TestTacletEquality. [497] compound_unary_plus_assignment, compound_unary_plus_assignment { \find(#allmodal ( (modal operator))\[{ .. #lhs=+#e; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. #lhs=#e; ... }\] (post)) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
• TestTacletEquality. [498] compound_unsigned_shiftright_1, compound_unsigned_shiftright_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse>>>#se; ... }\] (post)) \varcond(\new(#v (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v = #nse;#lhs=#v>>>#se; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [499] compound_unsigned_shiftright_2, compound_unsigned_shiftright_2 { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e>>>#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e) #v0 = #e;#typeof(#nse) #v1 = #nse;#lhs=#v0>>>#v1; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [521] condition, condition { \find(#allmodal ( (modal operator))\[{ .. #lhs=#e0 ?#e1 :#e2; ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. if (#e0) { #lhs=#e1; } else { #lhs=#e2; } ... }\] (post)) \heuristics(split_if, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [522] condition_not_simple, condition_not_simple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#nse ?#se1 :#se2; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v0 = #nse;#lhs=#v0 ?#se1 :#se2; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [523] condition_simple, condition_simple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#se0 ?#se1 :#se2; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(equals(#se0,TRUE),#se1,#se2)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [580] deleteMergePoint, deleteMergePoint { \find(#allmodal ( (modal operator))\[{ .. //@ merge_point (#lhs (program LeftHandSide)); ... }\] (post)) \replacewith(#allmodal(post)) \heuristics(merge_point, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [581] delete_unnecessary_cast, delete_unnecessary_cast { \find(#allmodal ( (modal operator))\[{ .. #lhs=(#npit)#se; ... }\] (post)) \sameUpdateLevel\varcond(\hasSort(#npit (program NonPrimitiveType), G), \sub(\typeof(#se (program SimpleExpression)), G), ) \add [or(equals(#se,null),equals(G::instance(#se),TRUE))]==>[] \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(#addCast(#se,#lhs)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [582] diamondToBox, diamondToBox { \find(\<{ .. #s ... }\> (post)) \replacewith(not(\[{ .. #s ... }\] (not(post)))) \heuristics(boxDiamondConv) Choices: programRules:Java}
• TestTacletEquality. [583] diamondToBoxTransaction, diamondToBoxTransaction { \find(diamond_transaction\[{ .. #s ... }\] (post)) \replacewith(not(box_transaction\[{ .. #s ... }\] (not(post)))) \heuristics(boxDiamondConv) Choices: programRules:Java}
• TestTacletEquality. [584] diamond_and_left, diamond_and_left { \find(#diamond ( (modal operator))\[{ .. #s ... }\] (and(post,post1))==>) \replacewith([and(#diamond ( (modal operator))\[{ .. #s ... }\] (post),#diamond ( (modal operator))\[{ .. #s ... }\] (post1))]==>[]) Choices: programRules:Java}
• TestTacletEquality. [585] diamond_and_right, diamond_and_right { \find(==>#diamond ( (modal operator))\[{ .. #s ... }\] (and(post,post1))) \replacewith([]==>[#diamond ( (modal operator))\[{ .. #s ... }\] (post1)]) ; \replacewith([]==>[#diamond ( (modal operator))\[{ .. #s ... }\] (post)]) Choices: programRules:Java}
• TestTacletEquality. [586] diamond_false, diamond_false { \find(#diamond ( (modal operator))\[{ .. #s ... }\] (false)) \replacewith(false) \heuristics(modal_tautology) Choices: programRules:Java}
• TestTacletEquality. [587] diamond_or_left, diamond_or_left { \find(#diamond ( (modal operator))\[{ .. #s ... }\] (or(post,post1))==>) \replacewith([or(#diamond ( (modal operator))\[{ .. #s ... }\] (post),#diamond ( (modal operator))\[{ .. #s ... }\] (post1))]==>[]) Choices: programRules:Java}
• TestTacletEquality. [588] diamond_or_right, diamond_or_right { \find(==>#diamond ( (modal operator))\[{ .. #s ... }\] (or(post,post1))) \replacewith([]==>[or(#diamond ( (modal operator))\[{ .. #s ... }\] (post),#diamond ( (modal operator))\[{ .. #s ... }\] (post1))]) Choices: programRules:Java}
• TestTacletEquality. [589] diamond_split_termination, diamond_split_termination { \find(\<{ .. #s ... }\> (post)) \replacewith(and(\[{ .. #s ... }\] (post),\<{ .. #s ... }\> (true))) Choices: programRules:Java}
• TestTacletEquality. [60] allFieldsUnfold, allFieldsUnfold { \find(#allmodal ( (modal operator))\[{ .. #v=\all_fields(#nseObj); ... }\] (post)) \varcond(\new(#vObjNew (program Variable), \typeof(#nseObj (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nseObj) #vObjNew = #nseObj;#v=\all_fields(#vObjNew); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [63] allObjectsAssignment, allObjectsAssignment { \find(#allmodal ( (modal operator))\[{ .. #v=\all_objects(#eObj.#a); ... }\] (post)) \replacewith(update-application(elem-update(#v (program Variable))(allObjects(#memberPVToField(#a))),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [662] doWhileUnwind, doWhileUnwind { \find(#allmodal ( (modal operator))\[{ .. do#swhile ( #e ); ... }\] (post)) \varcond(\newLabel (#innerLabel (program Label)), \newLabel (#outerLabel (program Label)), ) \replacewith(#allmodal ( (modal operator))\[{ .. #unwind-loop(do#swhile ( #e ); ) ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [695] elim_double_block, elim_double_block { \find(#allmodal ( (modal operator))\[{ {#slist}}\] (post)) \replacewith(#allmodal ( (modal operator))\[{#slist}\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [696] elim_double_block_2, elim_double_block_2 { \find(#allmodal ( (modal operator))\[{ .. { {#slist}} ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [697] elim_double_block_3, elim_double_block_3 { \find(#allmodal ( (modal operator))\[{ .. {while ( #e ) #s } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. while ( #e ) #s ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [698] elim_double_block_4, elim_double_block_4 { \find(#allmodal ( (modal operator))\[{ .. {for ( #loopInit; #guard; #forupdates ) #s } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. for ( #loopInit; #guard; #forupdates ) #s ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [699] elim_double_block_5, elim_double_block_5 { \find(#allmodal ( (modal operator))\[{ .. {for ( ; #guard; #forupdates ) #s } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. for ( ; #guard; #forupdates ) #s ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [700] elim_double_block_6, elim_double_block_6 { \find(#allmodal ( (modal operator))\[{ .. {for ( #loopInit; #guard; ) #s } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. for ( #loopInit; #guard; ) #s ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [701] elim_double_block_7, elim_double_block_7 { \find(#allmodal ( (modal operator))\[{ .. {for ( ; #guard; ) #s } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. for ( ; #guard; ) #s ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [702] elim_double_block_8, elim_double_block_8 { \find(#allmodal ( (modal operator))\[{ .. {do#swhile ( #e ); } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. do#swhile ( #e ); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [703] elim_double_block_9, elim_double_block_9 { \find(#allmodal ( (modal operator))\[{ .. { {#slist} {#slist1}} ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist} {#slist1} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [72] allocateInstance, allocateInstance { \find(==>#allmodal ( (modal operator))\[{ .. #lhs=#t.#allocate()@#t; ... }\] (post)) \varcond(\hasSort(#t2 (program Type), alphaObj), ) \add [and(and(not(equals(#lhs,null)),imp(wellFormed(heap),equals(boolean::select(heap,#lhs,java.lang.Object::<created>),FALSE))),equals(alphaObj::exactInstance(#lhs),TRUE))]==>[] \replacewith([]==>[update-application(elem-update(heap)(create(heap,#lhs)),#allmodal(post))]) \heuristics(method_expand) Choices: (programRules:Java & permissions:off)}
• TestTacletEquality. [73] allocateInstanceWithLength, allocateInstanceWithLength { \find(==>#allmodal ( (modal operator))\[{ .. #lhs=#t.#allocate(#len)@#t; ... }\] (post)) \varcond(\hasSort(#t2 (program Type), alphaObj), ) \add [and(and(not(equals(#lhs,null)),imp(wellFormed(heap),and(equals(boolean::select(heap,#lhs,java.lang.Object::<created>),FALSE),equals(length(#lhs),#len)))),equals(alphaObj::exactInstance(#lhs),TRUE))]==>[] \replacewith([]==>[update-application(elem-update(heap)(store(store(create(heap,#lhs),#lhs,java.lang.Object::<transient>,Z(0(#)))…
• TestTacletEquality. [758] emptyStatement, emptyStatement { \find(#allmodal ( (modal operator))\[{ .. ; ... }\] (post)) \replacewith(#allmodal(post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [760] enhancedfor_iterable, enhancedfor_iterable { \find(#allmodal ( (modal operator))\[{ .. for (#ty #id : #e) #stm ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. enhancedfor-elim(for (#ty #id : #e) #stm ) ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [798] equality_comparison_double, equality_comparison_double { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seDouble0==#seDouble1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(eqDouble(#seDouble0,#seDouble1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [799] equality_comparison_new, equality_comparison_new { \find(#allmodal ( (modal operator))\[{ .. #lhs=#senf0==#senf1; ... }\] (post)) \replacewith(if-then-else(not(equals(#senf0,#senf1)),#allmodal ( (modal operator))\[{ .. #lhs=false; ... }\] (post),#allmodal ( (modal operator))\[{ .. #lhs=true; ... }\] (post))) \heuristics(split_if, simplify_prog, obsolete) Choices: programRules:Java}
• TestTacletEquality. [7] activeUseAddition, activeUseAddition { \find(#allmodal ( (modal operator))\[{ .. #sv=#left+#right; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = #left+#right;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [800] equality_comparison_simple, equality_comparison_simple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#senf0==#senf1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(equals(#senf0,#senf1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [801] equality_comparison_simple_float, equality_comparison_simple_float { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seFloat0==#seFloat1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(eqFloat(#seFloat0,#seFloat1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [805] eval_array_this_access, eval_array_this_access { \find(#allmodal ( (modal operator))\[{ .. this[#nse]=#se0; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v0 = #nse;this[#v0]=#se0; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [806] eval_order_access1, eval_order_access1 { \find(#allmodal ( (modal operator))\[{ .. #nv.#attribute=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nv (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nv) #v0 = #nv;#v0.#attribute=#e; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [807] eval_order_access2, eval_order_access2 { \find(#allmodal ( (modal operator))\[{ .. #v=#nv.#attribute; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nv (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nv) #v0 = #nv;#v=#v0.#attribute; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [808] eval_order_access4, eval_order_access4 { \find(#allmodal ( (modal operator))\[{ .. #v.#a=#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#v (program Variable))), \not \static(#a (program Variable)), ) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#v) #v0 = #v;#typeof(#nse) #v1 = #nse;#v0.#a=#v1; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [809] eval_order_access4_this, eval_order_access4_this { \find(#allmodal ( (modal operator))\[{ .. #v.#a=#nse; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \not \static(#a (program Variable)), \isThisReference (#v (program Variable)), ) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nse) #v1 = #nse;#v.#a=#v1; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [810] eval_order_array_access1, eval_order_array_access1 { \find(#allmodal ( (modal operator))\[{ .. #nv[#e]=#e0; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nv (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nv) #v0 = #nv;#v0[#e]=#e0; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [811] eval_order_array_access2, eval_order_array_access2 { \find(#allmodal ( (modal operator))\[{ .. #v[#nse]=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#ar1 (program Variable), \typeof(#v (program Variable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#v) #ar1 = #v;#typeof(#nse) #v0 = #nse;#ar1[#v0]=#e; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [812] eval_order_array_access3, eval_order_array_access3 { \find(#allmodal ( (modal operator))\[{ .. #v[#se]=#nse; ... }\] (post)) \varcond(\new(#v2 (program Variable), \typeof(#se (program SimpleExpression))), \new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#v0 (program Variable), \typeof(#v (program Variable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#v) #v0 = #v;#typeof(#se) #v2 = #se;#typeof(#nse) #v1 = #nse;#v0[#v2]=#v1; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_pro…
• TestTacletEquality. [813] eval_order_array_access4, eval_order_array_access4 { \find(#allmodal ( (modal operator))\[{ .. #v=#nv[#e]; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nv (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nv) #v0 = #nv;#v=#v0[#e]; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [814] eval_order_array_access5, eval_order_array_access5 { \find(#allmodal ( (modal operator))\[{ .. #v=#v0[#nse]; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#nse (program NonSimpleExpression))), \new(#ar1 (program Variable), \typeof(#v0 (program Variable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#v0) #ar1 = #v0;#typeof(#nse) #v1 = #nse;#v=#ar1[#v1]; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [815] eval_order_array_access6, eval_order_array_access6 { \find(#allmodal ( (modal operator))\[{ .. #v=#nv.#length; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#nv (program NonSimpleExpression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#nv) #v0 = #nv;#v=#v0.#length; ... }\] (post)) \heuristics(simplify_prog_subset, simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [816] eval_order_iterated_assignments_0_0, eval_order_iterated_assignments_0_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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=#e1;#lhs0=#v0[#v1]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [817] eval_order_iterated_assignments_0_1, eval_order_iterated_assignments_0_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e0.#attribute=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v0 = #e0;#v0.#attribute=#e;#lhs0=#v0.#attribute; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]|#e1);#lhs0=#v0[#v1]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [819] eval_order_iterated_assignments_10_1, eval_order_iterated_assignments_10_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e0.#attribute|=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v0 = #e0;#v0.#attribute=(#typeof(#attribute))(#v0.#attribute|#e);#lhs0=#v0.#attribute; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]^#e1);#lhs0=#v0[#v1]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [821] eval_order_iterated_assignments_11_1, eval_order_iterated_assignments_11_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e0.#attribute^=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v0 = #e0;#v0.#attribute=(#typeof(#attribute))(#v0.#attribute^#e);#lhs0=#v0.#attribute; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]*#e1);#lhs0=#v0[#v1]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [823] eval_order_iterated_assignments_1_1, eval_order_iterated_assignments_1_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e0.#attribute*=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v0 = #e0;#v0.#attribute=(#typeof(#attribute))(#v0.#attribute*#e);#lhs0=#v0.#attribute; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]/#e1);#lhs0=#v0[#v1]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [825] eval_order_iterated_assignments_2_1, eval_order_iterated_assignments_2_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e0.#attribute/=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v0 = #e0;#v0.#attribute=(#typeof(#attribute))(#v0.#attribute/#e);#lhs0=#v0.#attribute; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]%#e1);#lhs0=#v0[#v1]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [827] eval_order_iterated_assignments_3_1, eval_order_iterated_assignments_3_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e0.#attribute%=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v0 = #e0;#v0.#attribute=(#typeof(#attribute))(#v0.#attribute%#e);#lhs0=#v0.#attribute; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]+#e1);#lhs0=#v0[#v1]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [829] eval_order_iterated_assignments_4_1, eval_order_iterated_assignments_4_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e0.#attribute+=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v0 = #e0;#v0.#attribute=(#typeof(#attribute))(#v0.#attribute+#e);#lhs0=#v0.#attribute; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]-#e1);#lhs0=#v0[#v1]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [831] eval_order_iterated_assignments_5_1, eval_order_iterated_assignments_5_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e0.#attribute-=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v0 = #e0;#v0.#attribute=(#typeof(#attribute))(#v0.#attribute-#e);#lhs0=#v0.#attribute; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]<<#e1);#lhs0=#v0[#v1]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [833] eval_order_iterated_assignments_6_1, eval_order_iterated_assignments_6_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e0.#attribute<<=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v0 = #e0;#v0.#attribute=(#typeof(#attribute))(#v0.#attribute<<#e);#lhs0=#v0.#attribute; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]>>#e1);#lhs0=#v0[#v1]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [835] eval_order_iterated_assignments_7_1, eval_order_iterated_assignments_7_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e0.#attribute>>=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v0 = #e0;#v0.#attribute=(#typeof(#attribute))(#v0.#attribute>>#e);#lhs0=#v0.#attribute; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]>>>#e1);#lhs0=#v0[#v1]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [837] eval_order_iterated_assignments_8_1, eval_order_iterated_assignments_8_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e0.#attribute>>>=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v0 = #e0;#v0.#attribute=(#typeof(#attribute))(#v0.#attribute>>>#e);#lhs0=#v0.#attribute; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• 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) #v0 = #e0;#typeof(#e) #v1 = #e;#v0[#v1]=(#typeof(#e0[#e]))(#v0[#v1]&#e1);#lhs0=#v0[#v1]; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [839] eval_order_iterated_assignments_9_1, eval_order_iterated_assignments_9_1 { \find(#allmodal ( (modal operator))\[{ .. #lhs0=#e0.#attribute&=#e; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#e0) #v0 = #e0;#v0.#attribute=(#typeof(#attribute))(#v0.#attribute&#e);#lhs0=#v0.#attribute; ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [855] execBreak, execBreak { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Break) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist1} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [856] execBreakEliminateBreakLabel, execBreakEliminateBreakLabel { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Break #lb) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {break ; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [857] execBreakEliminateBreakLabelWildcard, execBreakEliminateBreakLabelWildcard { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Break *) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {break ; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [858] execBreakEliminateContinue, execBreakEliminateContinue { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Continue) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {break ; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [859] execBreakEliminateContinueLabel, execBreakEliminateContinueLabel { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Continue #lb) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {break ; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [860] execBreakEliminateContinueLabelWildcard, execBreakEliminateContinueLabelWildcard { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Continue *) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {break ; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [861] execBreakEliminateExcCcatch, execBreakEliminateExcCcatch { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (#t #v0) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {break ; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [862] execBreakEliminateReturn, execBreakEliminateReturn { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Return) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {break ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [863] execBreakEliminateReturnVal, execBreakEliminateReturnVal { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Return #t #v) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {break ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [864] execBreakLabelEliminateBreak, execBreakLabelEliminateBreak { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Break) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {break ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [865] execBreakLabelEliminateBreakLabelNoMatch, execBreakLabelEliminateBreakLabelNoMatch { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Break #lb1) { #slist1 } #cs ... }\] (post)) \varcond(\different (#lb (program Label), #lb1 (program Label)), ) \replacewith(#allmodal ( (modal operator))\[{ .. exec {break ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [866] execBreakLabelEliminateContinue, execBreakLabelEliminateContinue { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Continue) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {break ; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [867] execBreakLabelEliminateContinueLabel, execBreakLabelEliminateContinueLabel { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Continue #lb1) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {break ; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [868] execBreakLabelEliminateContinueLabelWildcard, execBreakLabelEliminateContinueLabelWildcard { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Continue *) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {break ; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [869] execBreakLabelEliminateExcCcatch, execBreakLabelEliminateExcCcatch { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (#t #v) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {break ; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [870] execBreakLabelEliminateReturn, execBreakLabelEliminateReturn { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Return) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {break ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [871] execBreakLabelEliminateReturnVal, execBreakLabelEliminateReturnVal { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Return #t #v) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {break ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [872] execBreakLabelMatch, execBreakLabelMatch { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Break #lb) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist1} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [873] execBreakLabelWildcard, execBreakLabelWildcard { \find(#allmodal ( (modal operator))\[{ .. exec {break ; #slist } ccatch (\Break *) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist1} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [874] execCatchThrow, execCatchThrow { \find(#allmodal ( (modal operator))\[{ .. exec {throw #se;#slist} ccatch (#t #v0) { #slist1 } ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. if (#se==null) { exec { throw new java.lang.NullPointerException (); } ccatch (#t #v0) { #slist1 } } else if (#se instanceof #t) { #t #v0; #v0=(#t)#se; #slist1 } else { throw #se; } ... }\] (post)) \heuristics(simplif…
• TestTacletEquality. [875] execContinue, execContinue { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Continue) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist1} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [876] execContinueEliminateBreak, execContinueEliminateBreak { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Break) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {continue ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [877] execContinueEliminateBreakLabel, execContinueEliminateBreakLabel { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Break #lb) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {continue ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [878] execContinueEliminateBreakLabelWildcard, execContinueEliminateBreakLabelWildcard { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Break *) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {continue ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [879] execContinueEliminateExcCcatch, execContinueEliminateExcCcatch { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (#t #v0) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {continue ; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [880] execContinueEliminateReturn, execContinueEliminateReturn { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Return) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {continue ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [881] execContinueEliminateReturnVal, execContinueEliminateReturnVal { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Return #t #v) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {continue ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [882] execContinueLabelEliminateBreak, execContinueLabelEliminateBreak { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Break) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {continue ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [883] execContinueLabelEliminateBreakLabel, execContinueLabelEliminateBreakLabel { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Break #lb1) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {continue ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [884] execContinueLabelEliminateBreakLabelWildcard, execContinueLabelEliminateBreakLabelWildcard { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Break *) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {continue ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [885] execContinueLabelEliminateContinue, execContinueLabelEliminateContinue { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Continue) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {continue ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [886] execContinueLabelEliminateContinueLabelNoMatch, execContinueLabelEliminateContinueLabelNoMatch { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Continue #lb1) { #slist1 } #cs ... }\] (post)) \varcond(\different (#lb (program Label), #lb1 (program Label)), ) \replacewith(#allmodal ( (modal operator))\[{ .. exec {continue ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [887] execContinueLabelEliminateExcCcatch, execContinueLabelEliminateExcCcatch { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (#t #v) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {continue ; } ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [888] execContinueLabelEliminateReturn, execContinueLabelEliminateReturn { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Return) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {continue ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [889] execContinueLabelEliminateReturnVal, execContinueLabelEliminateReturnVal { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Return #t #v) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {continue ; } #cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [890] execContinueLabelMatch, execContinueLabelMatch { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Continue #lb) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist1} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [891] execContinueLabelWildcard, execContinueLabelWildcard { \find(#allmodal ( (modal operator))\[{ .. exec {continue ; #slist } ccatch (\Continue *) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist1} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [892] execEmpty, execEmpty { \find(#allmodal ( (modal operator))\[{ .. exec {}#cs ... }\] (post)) \replacewith(#allmodal(post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [893] execMultipleCatchThrow, execMultipleCatchThrow { \find(#allmodal ( (modal operator))\[{ .. exec {throw #se;#slist} ccatch (#t #v0) { #slist1 } ccatch (#t2 #v1) { #slist3 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. if (#se==null) { exec { throw new java.lang.NullPointerException (); } ccatch (#t #v0) { #slist1 } ccatch (#t2 #v1) { #slist3 } #cs } else if (#se instanceof #t) { #t #v0; #v0=(#t)#se; #slist…
• TestTacletEquality. [894] execNoCcatch, execNoCcatch { \find(#allmodal ( (modal operator))\[{ .. exec {#slist} ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [895] execReturn, execReturn { \find(#allmodal ( (modal operator))\[{ .. exec {return ;#slist} ccatch (\Return) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {#slist1} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [896] execReturnEliminateBreak, execReturnEliminateBreak { \find(#allmodal ( (modal operator))\[{ .. exec {return ;#slist} ccatch (\Break) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return ;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [897] execReturnEliminateBreakLabel, execReturnEliminateBreakLabel { \find(#allmodal ( (modal operator))\[{ .. exec {return ;#slist} ccatch (\Break #lb) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return ;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [898] execReturnEliminateBreakLabelWildcard, execReturnEliminateBreakLabelWildcard { \find(#allmodal ( (modal operator))\[{ .. exec {return ;#slist} ccatch (\Break *) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return ;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [899] execReturnEliminateContinue, execReturnEliminateContinue { \find(#allmodal ( (modal operator))\[{ .. exec {return ;#slist} ccatch (\Continue) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return ;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [8] activeUseBitwiseAnd, activeUseBitwiseAnd { \find(#allmodal ( (modal operator))\[{ .. #sv=#left&#right; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = #left&#right;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestTacletEquality. [900] execReturnEliminateContinueLabel, execReturnEliminateContinueLabel { \find(#allmodal ( (modal operator))\[{ .. exec {return ;#slist} ccatch (\Continue #lb) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return ;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [901] execReturnEliminateContinueLabelWildcard, execReturnEliminateContinueLabelWildcard { \find(#allmodal ( (modal operator))\[{ .. exec {return ;#slist} ccatch (\Continue *) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return ;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [902] execReturnEliminateExcCcatch, execReturnEliminateExcCcatch { \find(#allmodal ( (modal operator))\[{ .. exec {return ;#slist} ccatch (#t #v0) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return ;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [903] execReturnEliminateReturnVal, execReturnEliminateReturnVal { \find(#allmodal ( (modal operator))\[{ .. exec {return ;#slist} ccatch (\Return #t #v) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return ;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [904] execReturnVal, execReturnVal { \find(#allmodal ( (modal operator))\[{ .. exec {return #se;#slist} ccatch (\Return #t #v) { #slist1 } #cs ... }\] (post)) \varcond(\sub(\typeof(#se (program SimpleExpression)), \typeof(#v (program Variable))), ) \replacewith(#allmodal ( (modal operator))\[{ .. {#t #v;#v=(#t)#se;#slist1} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [905] execReturnValEliminateBreak, execReturnValEliminateBreak { \find(#allmodal ( (modal operator))\[{ .. exec {return #se;#slist} ccatch (\Break) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return #se;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [906] execReturnValEliminateBreakLabel, execReturnValEliminateBreakLabel { \find(#allmodal ( (modal operator))\[{ .. exec {return #se;#slist} ccatch (\Break #lb) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return #se;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [907] execReturnValEliminateBreakLabelWildcard, execReturnValEliminateBreakLabelWildcard { \find(#allmodal ( (modal operator))\[{ .. exec {return #se;#slist} ccatch (\Break *) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return #se;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [908] execReturnValEliminateContinue, execReturnValEliminateContinue { \find(#allmodal ( (modal operator))\[{ .. exec {return #se;#slist} ccatch (\Continue) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return #se;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [909] execReturnValEliminateContinueLabel, execReturnValEliminateContinueLabel { \find(#allmodal ( (modal operator))\[{ .. exec {return #se;#slist} ccatch (\Continue #lb) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return #se;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [910] execReturnValEliminateContinueLabelWildcard, execReturnValEliminateContinueLabelWildcard { \find(#allmodal ( (modal operator))\[{ .. exec {return #se;#slist} ccatch (\Continue *) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return #se;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [911] execReturnValEliminateExcCcatch, execReturnValEliminateExcCcatch { \find(#allmodal ( (modal operator))\[{ .. exec {return #se;#slist} ccatch (#t #v0) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {return #se;} ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [912] execReturnValEliminateReturn, execReturnValEliminateReturn { \find(#allmodal ( (modal operator))\[{ .. exec {return #se;#slist} ccatch (\Return) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {return #se;}#cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [913] execReturnValNonMatchingType, execReturnValNonMatchingType { \find(#allmodal ( (modal operator))\[{ .. exec {return #se;#slist} ccatch (\Return #t #v) { #slist1 } #cs ... }\] (post)) \varcond(\not\sub(\typeof(#se (program SimpleExpression)), \typeof(#v (program Variable))), ) \replacewith(#allmodal ( (modal operator))\[{ .. exec {return #se;#slist}#cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [914] execThrowEliminateBreak, execThrowEliminateBreak { \find(#allmodal ( (modal operator))\[{ .. exec {throw #se;#slist} ccatch (\Break) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {throw #se;}#cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [915] execThrowEliminateBreakLabel, execThrowEliminateBreakLabel { \find(#allmodal ( (modal operator))\[{ .. exec {throw #se;#slist} ccatch (\Break #lb) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {throw #se;}#cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [916] execThrowEliminateBreakLabelWildcard, execThrowEliminateBreakLabelWildcard { \find(#allmodal ( (modal operator))\[{ .. exec {throw #se;#slist} ccatch (\Break *) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {throw #se;}#cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [917] execThrowEliminateContinue, execThrowEliminateContinue { \find(#allmodal ( (modal operator))\[{ .. exec {throw #se;#slist} ccatch (\Continue) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {throw #se;}#cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [918] execThrowEliminateContinueLabel, execThrowEliminateContinueLabel { \find(#allmodal ( (modal operator))\[{ .. exec {throw #se;#slist} ccatch (\Continue #lb) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {throw #se;}#cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [919] execThrowEliminateContinueLabelWildcard, execThrowEliminateContinueLabelWildcard { \find(#allmodal ( (modal operator))\[{ .. exec {throw #se;#slist} ccatch (\Continue *) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {throw #se;}#cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [920] execThrowEliminateReturn, execThrowEliminateReturn { \find(#allmodal ( (modal operator))\[{ .. exec {throw #se;#slist} ccatch (\Return) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {throw #se;}#cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [921] execThrowEliminateReturnVal, execThrowEliminateReturnVal { \find(#allmodal ( (modal operator))\[{ .. exec {throw #se;#slist} ccatch (\Return #t #v) { #slist1 } #cs ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. exec {throw #se;}#cs ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [949] finishJavaCardTransactionBox, finishJavaCardTransactionBox { \find(==>box_transaction\[{ .. #finishJavaCardTransaction; ... }\] (post)) \replacewith([]==>[box(post)]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)}
• TestTacletEquality. [950] finishJavaCardTransactionDiamond, finishJavaCardTransactionDiamond { \find(==>diamond_transaction\[{ .. #finishJavaCardTransaction; ... }\] (post)) \replacewith([]==>[diamond(post)]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)}
• TestTacletEquality. [952] forInitUnfold, forInitUnfold { \find(#allmodal ( (modal operator))\[{ .. for ( #loopInit; #guard; #forupdates ) #s ... }\] (post)) \replacewith(#allmodal ( (modal operator))\[{ .. {forInitUnfoldTransformer(#loopInit)for ( ; #guard; #forupdates ) #s } ... }\] (post)) \heuristics(loop_expand) Choices: programRules:Java}
• TestTacletEquality. [953] for_to_while, for_to_while { \find(#allmodal ( (modal operator))\[{ .. #forloop ... }\] (post)) \varcond(\newLabel (#innerLabel (program Label)), \newLabel (#outerLabel (program Label)), ) \replacewith(#allmodal ( (modal operator))\[{ .. #for-to-while(#forloop) ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [961] getJavaCardTransient, getJavaCardTransient { \find(==>#allmodal ( (modal operator))\[{ .. #lhs=#jcsystemType.#getTransient(#se)@#jcsystemType; ... }\] (post)) \replacewith([]==>[not(equals(#se,null))]) ; \replacewith([]==>[update-application(elem-update(#lhs (program LeftHandSide))(int::select(heap,#se,java.lang.Object::<transient>)),#allmodal(post))]) \heuristics(simplify_prog) Choices: (programRules:Java & JavaCard:on)}
• TestTacletEquality. [984] greater_equal_than_comparison_new, greater_equal_than_comparison_new { \find(#allmodal ( (modal operator))\[{ .. #lhs=#senf0>=#senf1; ... }\] (post)) \replacewith(if-then-else(geq(#senf0,#senf1),#allmodal ( (modal operator))\[{ .. #lhs=true; ... }\] (post),#allmodal ( (modal operator))\[{ .. #lhs=false; ... }\] (post))) \heuristics(split_if, simplify_prog, obsolete) Choices: programRules:Java}
• TestTacletEquality. [985] greater_equal_than_comparison_simple, greater_equal_than_comparison_simple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#senf0>=#senf1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(geq(#senf0,#senf1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [986] greater_equal_than_comparison_simple_double, greater_equal_than_comparison_simple_double { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seDouble0>=#seDouble1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(geqDouble(#seDouble0,#seDouble1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [987] greater_equal_than_comparison_simple_float, greater_equal_than_comparison_simple_float { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seFloat0>=#seFloat1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(geqFloat(#seFloat0,#seFloat1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [989] greater_than_comparison_new, greater_than_comparison_new { \find(#allmodal ( (modal operator))\[{ .. #lhs=#senf0>#senf1; ... }\] (post)) \replacewith(if-then-else(gt(#senf0,#senf1),#allmodal ( (modal operator))\[{ .. #lhs=true; ... }\] (post),#allmodal ( (modal operator))\[{ .. #lhs=false; ... }\] (post))) \heuristics(split_if, simplify_prog, obsolete) Choices: programRules:Java}
• TestTacletEquality. [990] greater_than_comparison_simple, greater_than_comparison_simple { \find(#allmodal ( (modal operator))\[{ .. #lhs=#senf0>#senf1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(gt(#senf0,#senf1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [991] greater_than_comparison_simple_double, greater_than_comparison_simple_double { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seDouble0>#seDouble1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(gtDouble(#seDouble0,#seDouble1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [992] greater_than_comparison_simple_float, greater_than_comparison_simple_float { \find(#allmodal ( (modal operator))\[{ .. #lhs=#seFloat0>#seFloat1; ... }\] (post)) \replacewith(update-application(elem-update(#lhs (program LeftHandSide))(if-then-else(gtFloat(#seFloat0,#seFloat1),TRUE,FALSE)),#allmodal(post))) \heuristics(simplify_prog) Choices: programRules:Java}
• TestTacletEquality. [9] activeUseBitwiseNegation, activeUseBitwiseNegation { \find(#allmodal ( (modal operator))\[{ .. #sv=~#left; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#sv (program StaticVariable)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof(#sv) #v0 = ~#left;@(#sv)=#v0; ... }\] (post)) \heuristics(simplify_expression) Choices: (programRules:Java & initialisation:disableStaticInitialisation)}
• TestProgramMetaConstructs. testForInitUnfoldTransformer1()
• TestProgramMetaConstructs. testForInitUnfoldTransformer2()
• TestProgramMetaConstructs. testForInitUnfoldTransformer3()

Ignored tests

• TestRecoder2KeY. xtestFileInput()
• TestClashFreeSubst. xtestMultiClash()
• TestClashFreeSubst. xtestMultiClash1()
• TestDeclParser. testAmbiguousDecls()
• TestDeclParser. testGenericSortDecl5()
• TestParser. testRelativeInclude()
• TestTermParser. test12()
• TestTermParser. testJavaQueryAndAttribute_all()
• TestTermParser. xtestBindingUpdateTermOldBindingAlternative()
• TestTermParser. xtestParsingArrayWithSpaces()
• ParserMessageTest. verifyColumnNumber()
• ParserMessageTest. verifyLineNumber()
• ParserMessageTest. verifyMessage()
• TestGoal. testSetBack0()
• TestGoal. testSetBack1()
• TestTacletIndex. disabled_testNonInteractiveIsShownOnlyIfHeuristicIsMissed()
• TestProgramMetaConstructs. testASTWalker()
• MasterHandlerTest. [10] quant1.props
• MasterHandlerTest. [11] bool1.props
• MasterHandlerTest. [12] quant2.props
• MasterHandlerTest. [13] types1.props
• MasterHandlerTest. [14] bool3.props
• MasterHandlerTest. [15] types2.props
• MasterHandlerTest. [16] heap1.props
• MasterHandlerTest. [17] ex1.props
• MasterHandlerTest. [18] float1.props
• MasterHandlerTest. [19] ex2.props
• MasterHandlerTest. [1] cast3.props
• MasterHandlerTest. [20] float.sqrt1.props
• MasterHandlerTest. [21] cast2.props
• MasterHandlerTest. [22] ite1.props
• MasterHandlerTest. [23] int1.props
• MasterHandlerTest. [24] upd1.props
• MasterHandlerTest. [2] float.sqrt2.props
• MasterHandlerTest. [3] upd2.props
• MasterHandlerTest. [4] cast1.props
• MasterHandlerTest. [5] float.sinDouble.props
• MasterHandlerTest. [6] float2.props
• MasterHandlerTest. [7] uninterpreted1.props
• MasterHandlerTest. [8] float.eq.props
• MasterHandlerTest. [9] bool2.props
• TestCvc4. testAdd1()
• TestCvc4. testAllex1()
• TestCvc4. testAllex2()
• TestCvc4. testAllex3()
• TestCvc4. testAndnot()
• TestCvc4. testAndornot()
• TestCvc4. testAndornot2()
• TestCvc4. testBProd1()
• TestCvc4. testBProd2()
• TestCvc4. testBProd3()
• TestCvc4. testBSum1()
• TestCvc4. testBSum2()
• TestCvc4. testBSum3()
• TestCvc4. testBinderPred2()
• TestCvc4. testBinderPred3()
• TestCvc4. testEqual1()
• TestCvc4. testEqual2()
• TestCvc4. testEqui1()
• TestCvc4. testEqui2()
• TestCvc4. testImply()
• TestCvc4. testImply2()
• TestCvc4. testImply3()
• TestCvc4. testLogicalIte1()
• TestCvc4. testLogicalIte2()
• TestCvc4. testOrnot()
• TestCvc4. testSubsort1()
• TestCvc4. testSubsort2()
• TestZ3. testAdd1()
• TestZ3. testAllex1()
• TestZ3. testAllex2()
• TestZ3. testAllex3()
• TestZ3. testAndnot()
• TestZ3. testAndornot()
• TestZ3. testAndornot2()
• TestZ3. testBProd1()
• TestZ3. testBProd2()
• TestZ3. testBProd3()
• TestZ3. testBSum1()
• TestZ3. testBSum2()
• TestZ3. testBSum3()
• TestZ3. testBinderPred2()
• TestZ3. testBinderPred3()
• TestZ3. testDiv1()
• TestZ3. testDiv3()
• TestZ3. testDiv5()
• TestZ3. testDiv6()
• TestZ3. testEqual1()
• TestZ3. testEqual2()
• TestZ3. testEqui1()
• TestZ3. testEqui2()
• TestZ3. testImply()
• TestZ3. testImply2()
• TestZ3. testImply3()
• TestZ3. testLogicalIte1()
• TestZ3. testLogicalIte2()
• TestZ3. testOrnot()
• TestZ3. testSubsort1()
• TestZ3. testSubsort2()
• TestJMLPreTranslator. disabled_testMLCommentEndInSLComment1()
• TestJMLPreTranslator. disabled_testMLCommentEndInSLComment2()
• TestTriggersSet. testTrigger2()
• DesignTests. xtestTermSubclassVisibility()
• TestProofUserManager. testUserManagement_NoEnvironment()

Packages

Classes