integerAssignment2UpdateRules.key
Taclets
Enabled under choices:
programRules:Java
assignmentMultiplicationInt
assignmentMultiplicationInt {
\find ( \modality{#normalassign}{..
#loc = #seCharByteShortInt0 * #seCharByteShortInt1;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inInt ( mul ( #seCharByteShortInt0, #seCharByteShortInt1)))}
;
\replacewith ( { #loc:= javaMulInt ( #seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "multiplication"
};defined in: integerAssignment2UpdateRules.key Line: 41 Offset :4
assignmentMultiplicationLong
assignmentMultiplicationLong {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt * #seLong;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inLong ( mul ( #seCharByteShortInt, #seLong)))}
;
\replacewith ( { #loc:= javaMulLong ( #seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "multiplication"
};defined in: integerAssignment2UpdateRules.key Line: 56 Offset :4
assignmentMultiplicationLong2
assignmentMultiplicationLong2 {
\find ( \modality{#normalassign}{..
#loc=#seLong * #seCharByteShortInt;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inLong ( mul ( #seLong, #seCharByteShortInt)))}
;
\replacewith ( { #loc:= javaMulLong ( #seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "multiplication"
};defined in: integerAssignment2UpdateRules.key Line: 71 Offset :4
assignmentMultiplicationLong3
assignmentMultiplicationLong3 {
\find ( \modality{#normalassign}{..
#loc=#seLong0 * #seLong1;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inLong ( mul ( #seLong0, #seLong1)))}
;
\replacewith ( { #loc:= javaMulLong ( #seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "multiplication"
};defined in: integerAssignment2UpdateRules.key Line: 86 Offset :4
Taclets
Enabled under choices:
programRules:JavaruntimeExceptions:ban
assignmentDivisionInt
assignmentDivisionInt {
\find ( ==> \modality{#normalassign}{..
#loc=#seCharByteShortInt0 / #seCharByteShortInt1;
...}\endmodality ( post ))
\replacewith ( ==> { #loc:= javaDivInt ( #seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality ( post ));
\replacewith ( ==> #seCharByteShortInt1!= 0 )
\heuristics (executeIntegerAssignment )
\displayname "division"
};defined in: integerAssignment2UpdateRules.key Line: 107 Offset :4
assignmentDivisionLong2
assignmentDivisionLong2 {
\find ( ==> \modality{#normalassign}{..
#loc=#seLong / #seCharByteShortInt;
...}\endmodality ( post ))
\replacewith ( ==> { #loc:= javaDivLong ( #seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality ( post ));
\replacewith ( ==> #seCharByteShortInt!= 0 )
\heuristics (executeIntegerAssignment )
\displayname "division"
};defined in: integerAssignment2UpdateRules.key Line: 131 Offset :4
Taclets
Enabled under choices:
programRules:JavaruntimeExceptions:ignore
assignmentDivisionInt
assignmentDivisionInt {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt0 / #seCharByteShortInt1;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaDivInt ( #seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "division"
};defined in: integerAssignment2UpdateRules.key Line: 164 Offset :4
assignmentDivisionLong
assignmentDivisionLong {
\find ( \modality{#normalassign}{..
#loc=#se / #seLong;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaDivLong ( #se, #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "division"
};defined in: integerAssignment2UpdateRules.key Line: 175 Offset :4
assignmentDivisionLong2
assignmentDivisionLong2 {
\find ( \modality{#normalassign}{..
#loc=#seLong / #seCharByteShortInt;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaDivLong ( #seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "division"
};defined in: integerAssignment2UpdateRules.key Line: 186 Offset :4
Taclets
Enabled under choices:
programRules:JavaruntimeExceptions:allow
assignmentDivisionInt
assignmentDivisionInt {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt0 / #seCharByteShortInt1;
...}\endmodality ( post ))
\replacewith ( \if ( #seCharByteShortInt1!= 0 )\then ( { #loc:= javaDivInt ( #seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality ( post ))\else ( \modality{#normalassign}{..
throw new java.lang.ArithmeticException();
...}\endmodality ( post )))
\heuristics (executeIntegerAssignment )
\displayname "division"
};defined in: integerAssignment2UpdateRules.key Line: 217 Offset :4
assignmentDivisionLong
assignmentDivisionLong {
\find ( \modality{#normalassign}{..
#loc=#se / #seLong;
...}\endmodality ( post ))
\replacewith ( \if ( #seLong!= 0 )\then ( { #loc:= javaDivLong ( #se, #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))\else ( \modality{#normalassign}{..
throw new java.lang.ArithmeticException();
...}\endmodality ( post )))
\heuristics (executeIntegerAssignment )
\displayname "division"
};defined in: integerAssignment2UpdateRules.key Line: 231 Offset :4
assignmentDivisionLong2
assignmentDivisionLong2 {
\find ( \modality{#normalassign}{..
#loc=#seLong / #seCharByteShortInt;
...}\endmodality ( post ))
\replacewith ( \if ( #seCharByteShortInt!= 0 )\then ( { #loc:= javaDivLong ( #seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality ( post ))\else ( \modality{#normalassign}{..
throw new java.lang.ArithmeticException();
...}\endmodality ( post )))
\heuristics (executeIntegerAssignment )
\displayname "division"
};defined in: integerAssignment2UpdateRules.key Line: 245 Offset :4
assignmentModulo
assignmentModulo {
\find ( \modality{#normalassign}{..
#loc=#se0 % #se1;
...}\endmodality ( post ))
\replacewith ( \if ( #se1!= 0 )\then ( { #loc:= javaMod ( #se0, #se1)} \modality{#normalassign}{.. ...}\endmodality ( post ))\else ( \modality{#normalassign}{..
throw new java.lang.ArithmeticException();
...}\endmodality ( post )))
\heuristics (executeIntegerAssignment )
\displayname "modulo"
};defined in: integerAssignment2UpdateRules.key Line: 263 Offset :4
Taclets
Enabled under choices:
programRules:Java
assignmentSubtractionInt
assignmentSubtractionInt {
\find ( \modality{#normalassign}{..
#loc = #seCharByteShortInt0 - #seCharByteShortInt1;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inInt ( sub ( #seCharByteShortInt0, #seCharByteShortInt1)))}
;
\replacewith ( { #loc:= javaSubInt ( #seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "subtraction"
};defined in: integerAssignment2UpdateRules.key Line: 283 Offset :4
assignmentSubtractionLong
assignmentSubtractionLong {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt - #seLong;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inLong ( sub ( #seCharByteShortInt, #seLong)))}
;
\replacewith ( { #loc:= javaSubLong ( #seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "subtraction"
};defined in: integerAssignment2UpdateRules.key Line: 298 Offset :4
assignmentSubtractionLong2
assignmentSubtractionLong2 {
\find ( \modality{#normalassign}{..
#loc=#seLong - #seCharByteShortInt;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inLong ( sub ( #seLong, #seCharByteShortInt)))}
;
\replacewith ( { #loc:= javaSubLong ( #seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "subtraction"
};defined in: integerAssignment2UpdateRules.key Line: 313 Offset :4
assignmentSubtractionLong3
assignmentSubtractionLong3 {
\find ( \modality{#normalassign}{..
#loc=#seLong0 - #seLong1;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inLong ( sub ( #seLong0, #seLong1)))}
;
\replacewith ( { #loc:= javaSubLong ( #seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "subtraction"
};defined in: integerAssignment2UpdateRules.key Line: 329 Offset :4
assignmentAdditionInt
assignmentAdditionInt {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt0 + #seCharByteShortInt1;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inInt ( add ( #seCharByteShortInt0, #seCharByteShortInt1)))}
;
\replacewith ( { #loc:= javaAddInt ( #seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "addition"
};defined in: integerAssignment2UpdateRules.key Line: 346 Offset :4
assignmentAdditionLong
assignmentAdditionLong {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt + #seLong;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inLong ( add ( #seCharByteShortInt, #seLong)))}
;
\replacewith ( { #loc:= javaAddLong ( #seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "addition"
};defined in: integerAssignment2UpdateRules.key Line: 362 Offset :4
assignmentAdditionLong2
assignmentAdditionLong2 {
\find ( \modality{#normalassign}{..
#loc=#seLong + #seCharByteShortInt;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inLong ( add ( #seLong, #seCharByteShortInt)))}
;
\replacewith ( { #loc:= javaAddLong ( #seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "addition"
};defined in: integerAssignment2UpdateRules.key Line: 378 Offset :4
assignmentAdditionLong3
assignmentAdditionLong3 {
\find ( \modality{#normalassign}{..
#loc=#seLong0 + #seLong1;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inLong ( add ( #seLong0, #seLong1)))}
;
\replacewith ( { #loc:= javaAddLong ( #seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "addition"
};defined in: integerAssignment2UpdateRules.key Line: 394 Offset :4
assignmentBitwiseAndInt
assignmentBitwiseAndInt {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt0 & #seCharByteShortInt1;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseAndInt ( #seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "bitwiseAnd"
};defined in: integerAssignment2UpdateRules.key Line: 412 Offset :4
assignmentBitwiseAndLong
assignmentBitwiseAndLong {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt & #seLong;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseAndLong ( #seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "bitwiseAnd"
};defined in: integerAssignment2UpdateRules.key Line: 423 Offset :4
assignmentBitwiseAndLong2
assignmentBitwiseAndLong2 {
\find ( \modality{#normalassign}{..
#loc=#seLong & #seCharByteShortInt;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseAndLong ( #seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "bitwiseAnd"
};defined in: integerAssignment2UpdateRules.key Line: 434 Offset :4
assignmentBitwiseAndLong3
assignmentBitwiseAndLong3 {
\find ( \modality{#normalassign}{..
#loc=#seLong0 & #seLong1;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseAndLong ( #seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "bitwiseAnd"
};defined in: integerAssignment2UpdateRules.key Line: 445 Offset :4
assignmentBitwiseOrInt
assignmentBitwiseOrInt {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt0 | #seCharByteShortInt1;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseOrInt ( #seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "bitwiseOr"
};defined in: integerAssignment2UpdateRules.key Line: 458 Offset :4
assignmentBitwiseOrLong
assignmentBitwiseOrLong {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt | #seLong;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseOrLong ( #seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "bitwiseOr"
};defined in: integerAssignment2UpdateRules.key Line: 469 Offset :4
assignmentBitwiseOrLong2
assignmentBitwiseOrLong2 {
\find ( \modality{#normalassign}{..
#loc=#seLong | #seCharByteShortInt;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseOrLong ( #seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "bitwiseOr"
};defined in: integerAssignment2UpdateRules.key Line: 481 Offset :4
assignmentBitwiseOrLong3
assignmentBitwiseOrLong3 {
\find ( \modality{#normalassign}{..
#loc=#seLong0 | #seLong1;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseOrLong ( #seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "bitwiseOr"
};defined in: integerAssignment2UpdateRules.key Line: 493 Offset :4
assignmentBitwiseXOrInt
assignmentBitwiseXOrInt {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt0 ^ #seCharByteShortInt1;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseXOrInt ( #seCharByteShortInt0, #seCharByteShortInt1)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "bitwiseXOr"
};defined in: integerAssignment2UpdateRules.key Line: 506 Offset :4
assignmentBitwiseXOrLong
assignmentBitwiseXOrLong {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt ^ #seLong;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseXOrLong ( #seCharByteShortInt, #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "bitwiseXOr"
};defined in: integerAssignment2UpdateRules.key Line: 517 Offset :4
assignmentBitwiseXOrLong2
assignmentBitwiseXOrLong2 {
\find ( \modality{#normalassign}{..
#loc=#seLong ^ #seCharByteShortInt;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseXOrLong ( #seLong, #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "bitwiseXOr"
};defined in: integerAssignment2UpdateRules.key Line: 528 Offset :4
assignmentBitwiseXOrLong3
assignmentBitwiseXOrLong3 {
\find ( \modality{#normalassign}{..
#loc=#seLong0 ^ #seLong1;
...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseXOrLong ( #seLong0, #seLong1)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "bitwiseXOr"
};defined in: integerAssignment2UpdateRules.key Line: 539 Offset :4
assignmentShiftRightInt
assignmentShiftRightInt {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt0 >> #se;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inInt ( shiftright ( #seLong0, #se)))}
;
\replacewith ( { #loc:= javaShiftRightInt ( #seCharByteShortInt0, #se)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "shift"
};defined in: integerAssignment2UpdateRules.key Line: 552 Offset :4
assignmentShiftRightLong
assignmentShiftRightLong {
\find ( \modality{#normalassign}{..
#loc=#seLong0 >> #se;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inInt ( shiftright ( #seLong0, #se)))}
;
\replacewith ( { #loc:= javaShiftRightLong ( #seLong0, #se)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "shift"
};defined in: integerAssignment2UpdateRules.key Line: 568 Offset :4
assignmentShiftLeftInt
assignmentShiftLeftInt {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt0 << #se; ...}
\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inInt ( shiftleft ( #seCharByteShortInt0, #se)))}
;
\replacewith ( { #loc:= javaShiftLeftInt ( #seCharByteShortInt0, #se)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "shift"
};defined in: integerAssignment2UpdateRules.key Line: 586 Offset :4
assignmentShiftLeftLong
assignmentShiftLeftLong {
\find ( \modality{#normalassign}{..
#loc=#seLong0 << #se;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inLong ( shiftleft ( #seLong0, #se)))}
;
\replacewith ( { #loc:= javaShiftLeftLong ( #seLong0, #se)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "shift"
};defined in: integerAssignment2UpdateRules.key Line: 602 Offset :4
assignmentUnsignedShiftRightInt
assignmentUnsignedShiftRightInt {
\find ( \modality{#normalassign}{..
#loc=#seCharByteShortInt0 >>> #se; ...}
\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inLong ( unsignedshiftrightJint ( #seCharByteShortInt0, #se)))}
;
\replacewith ( { #loc:= javaUnsignedShiftRightInt ( #seCharByteShortInt0, #se)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "shift"
};defined in: integerAssignment2UpdateRules.key Line: 620 Offset :4
assignmentUnsignedShiftRightLong
assignmentUnsignedShiftRightLong {
\find ( \modality{#normalassign}{..
#loc=#seLong0 >>> #se;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inLong ( unsignedshiftrightJlong ( #seLong0, #se)))}
;
\replacewith ( { #loc:= javaUnsignedShiftRightLong ( #seLong0, #se)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "shift"
};defined in: integerAssignment2UpdateRules.key Line: 636 Offset :4
unaryMinusInt
unaryMinusInt {
\find ( \modality{#normalassign}{..
#loc = - #seCharByteShortInt;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inInt ( neg ( #seCharByteShortInt)))}
;
\replacewith ( { #loc:= javaUnaryMinusInt ( #seCharByteShortInt)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "unaryMinus"
};defined in: integerAssignment2UpdateRules.key Line: 655 Offset :4
unaryMinusLong
unaryMinusLong {
\find ( \modality{#normalassign}{..
#loc = - #seLong;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inLong ( neg ( #seLong)))}
;
\replacewith ( { #loc:= javaUnaryMinusLong ( #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "unary_minus"
};defined in: integerAssignment2UpdateRules.key Line: 670 Offset :4
bitwiseNegationInt
bitwiseNegationInt {
\find ( \modality{#normalassign}{.. #loc = ~ #seCharByteShortInt; ...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseNegateInt ( #se)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "invertBits"
};defined in: integerAssignment2UpdateRules.key Line: 685 Offset :4
bitwiseNegationLong
bitwiseNegationLong {
\find ( \modality{#normalassign}{.. #loc = ~ #se; ...}\endmodality ( post ))
\replacewith ( { #loc:= javaBitwiseNegateLong ( #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "invertBits"
};defined in: integerAssignment2UpdateRules.key Line: 693 Offset :4
narrowingByteCastShort
narrowingByteCastShort {
\find ( \modality{#normalassign}{..
#loc = (byte) #seShort;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inByte ( #seShort))}
;
\replacewith ( { #loc:= javaCastByte ( #seShort)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "cast"
};defined in: integerAssignment2UpdateRules.key Line: 705 Offset :4
narrowingByteCastInt
narrowingByteCastInt {
\find ( \modality{#normalassign}{..
#loc = (byte) #seInt;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inByte ( #seInt))}
;
\replacewith ( { #loc:= javaCastByte ( #seInt)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "cast"
};defined in: integerAssignment2UpdateRules.key Line: 720 Offset :4
narrowingByteCastLong
narrowingByteCastLong {
\find ( \modality{#normalassign}{..
#loc = (byte) #seLong;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inByte ( #seLong))}
;
\replacewith ( { #loc:= javaCastByte ( #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "cast"
};defined in: integerAssignment2UpdateRules.key Line: 735 Offset :4
narrowingShortCastInt
narrowingShortCastInt {
\find ( \modality{#normalassign}{..
#loc = (short) #seInt;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inShort ( #seInt))}
;
\replacewith ( { #loc:= javaCastShort ( #seInt)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "cast"
};defined in: integerAssignment2UpdateRules.key Line: 750 Offset :4
narrowingShortCastLong
narrowingShortCastLong {
\find ( \modality{#normalassign}{..
#loc = (short) #seLong;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inShort ( #seLong))}
;
\replacewith ( { #loc:= javaCastShort ( #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "cast"
};defined in: integerAssignment2UpdateRules.key Line: 765 Offset :4
narrowingIntCastLong
narrowingIntCastLong {
\find ( \modality{#normalassign}{.. #loc = (int) #seLong; ...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inInt ( #seLong))}
;
\replacewith ( { #loc:= javaCastInt ( #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "cast"
};defined in: integerAssignment2UpdateRules.key Line: 780 Offset :4
narrowingCharCastByte
narrowingCharCastByte {
\find ( \modality{#normalassign}{..
#loc = (char) #seByte;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inChar ( #seByte))}
;
\replacewith ( { #loc:= javaCastChar ( #seByte)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "cast"
};defined in: integerAssignment2UpdateRules.key Line: 793 Offset :4
narrowingCharCastShort
narrowingCharCastShort {
\find ( \modality{#normalassign}{..
#loc = (char) #seShort;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inChar ( #seShort))}
;
\replacewith ( { #loc:= javaCastChar ( #seShort)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "cast"
};defined in: integerAssignment2UpdateRules.key Line: 809 Offset :4
narrowingCharCastInt
narrowingCharCastInt {
\find ( \modality{#normalassign}{..
#loc = (char) #seInt;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inChar ( #seInt))}
;
\replacewith ( { #loc:= javaCastChar ( #seInt)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "cast"
};defined in: integerAssignment2UpdateRules.key Line: 825 Offset :4
narrowingCharCastLong
narrowingCharCastLong {
\find ( \modality{#normalassign}{..
#loc = (char) #seLong;
...}\endmodality ( post ))
\sameUpdateLevel
( intRules : arithmeticSemanticsCheckingOF ) {
"Overflow check" : \add ( ==> inChar ( #seLong))}
;
\replacewith ( { #loc:= javaCastChar ( #seLong)} \modality{#normalassign}{.. ...}\endmodality ( post ))
\heuristics (executeIntegerAssignment )
\displayname "cast"
};defined in: integerAssignment2UpdateRules.key Line: 840 Offset :4