Skip to content

Commit

Permalink
fix creating of branches for overflow checking
Browse files Browse the repository at this point in the history
  • Loading branch information
@WolframPfeifer
WolframPfeifer committed Nov 15, 2023
1 parent ac66700 commit 5b68afc
Showing 1 changed file with 30 additions and 30 deletions.
60 changes: 30 additions & 30 deletions key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@
\find(\modality{#normalassign}{..
#loc = #seCharByteShortInt0 * #seCharByteShortInt1;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inInt(mul(#seCharByteShortInt0, #seCharByteShortInt1)))
};
Expand All @@ -56,7 +56,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt * #seLong;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inLong(mul(#seCharByteShortInt, #seLong)))
};
Expand All @@ -70,7 +70,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong * #seCharByteShortInt;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inLong(mul(#seLong, #seCharByteShortInt)))
};
Expand All @@ -84,7 +84,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong0 * #seLong1;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inLong(mul(#seLong0, #seLong1)))
};
Expand Down Expand Up @@ -280,7 +280,7 @@
\find(\modality{#normalassign}{..
#loc = #seCharByteShortInt0 - #seCharByteShortInt1;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inInt(sub(#seCharByteShortInt0, #seCharByteShortInt1)))
};
Expand All @@ -294,7 +294,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt - #seLong;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inLong(sub(#seCharByteShortInt, #seLong)))
};
Expand All @@ -308,7 +308,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong - #seCharByteShortInt;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inLong(sub(#seLong, #seCharByteShortInt)))
};
Expand All @@ -323,7 +323,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong0 - #seLong1;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inLong(sub(#seLong0, #seLong1)))
};
Expand All @@ -339,7 +339,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt0 + #seCharByteShortInt1;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inInt(add(#seCharByteShortInt0, #seCharByteShortInt1)))
};
Expand All @@ -354,7 +354,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt + #seLong;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inLong(add(#seCharByteShortInt, #seLong)))
};
Expand All @@ -369,7 +369,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong + #seCharByteShortInt;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inLong(add(#seLong, #seCharByteShortInt)))
};
Expand All @@ -384,7 +384,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong0 + #seLong1;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inLong(add(#seLong0, #seLong1)))
};
Expand Down Expand Up @@ -541,7 +541,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt0 >> #se;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inInt(shiftright(#seLong0, #se)))
};
Expand All @@ -556,7 +556,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong0 >> #se;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inInt(shiftright(#seLong0, #se)))
};
Expand All @@ -573,7 +573,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt0 << #se; ...}
\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inInt(shiftleft(#seCharByteShortInt0, #se)))
};
Expand All @@ -588,7 +588,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong0 << #se;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inLong(shiftleft(#seLong0, #se)))
};
Expand All @@ -605,7 +605,7 @@
\find(\modality{#normalassign}{..
#loc=#seCharByteShortInt0 >>> #se; ...}
\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inLong(unsignedshiftrightJint(#seCharByteShortInt0, #se)))
};
Expand All @@ -620,7 +620,7 @@
\find(\modality{#normalassign}{..
#loc=#seLong0 >>> #se;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inLong(unsignedshiftrightJlong(#seLong0, #se)))
};
Expand All @@ -638,7 +638,7 @@
\find(\modality{#normalassign}{..
#loc = - #seCharByteShortInt;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inInt(neg(#seCharByteShortInt)))
};
Expand All @@ -652,7 +652,7 @@
\find(\modality{#normalassign}{..
#loc = - #seLong;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inLong(neg(#seLong)))
};
Expand Down Expand Up @@ -686,7 +686,7 @@
\find(\modality{#normalassign}{..
#loc = (byte) #seShort;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inByte(#seShort))
};
Expand All @@ -700,7 +700,7 @@
\find(\modality{#normalassign}{..
#loc = (byte) #seInt;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inByte(#seInt))
};
Expand All @@ -714,7 +714,7 @@
\find(\modality{#normalassign}{..
#loc = (byte) #seLong;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inByte(#seLong))
};
Expand All @@ -728,7 +728,7 @@
\find(\modality{#normalassign}{..
#loc = (short) #seInt;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inShort(#seInt))
};
Expand All @@ -742,7 +742,7 @@
\find(\modality{#normalassign}{..
#loc = (short) #seLong;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inShort(#seLong))
};
Expand All @@ -754,7 +754,7 @@

narrowingIntCastLong {
\find(\modality{#normalassign}{.. #loc = (int) #seLong; ...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inInt(#seLong))
};
Expand All @@ -768,7 +768,7 @@
\find(\modality{#normalassign}{..
#loc = (char) #seByte;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inChar(#seByte))
};
Expand All @@ -783,7 +783,7 @@
\find(\modality{#normalassign}{..
#loc = (char) #seShort;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inChar(#seShort))
};
Expand All @@ -798,7 +798,7 @@
\find(\modality{#normalassign}{..
#loc = (char) #seInt;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inChar(#seInt))
};
Expand All @@ -812,7 +812,7 @@
\find(\modality{#normalassign}{..
#loc = (char) #seLong;
...}\endmodality (post))
(intRules:checkedOverflow) {
(intRules:arithmeticSemanticsCheckingOF) {
"Overflow check":
\replacewith(inChar(#seLong))
};
Expand Down

0 comments on commit 5b68afc

Please sign in to comment.