The recently merged PR #3353 only partially fixes the overflow checking: All the taclets in integerAssignment2UpdateRules.key, which add another formula to the sequent for the overflow check, are missing the \sameUpdateLevel constraint. This can lead to unprovable overflow check branches (see the inInt line in the screenshot below, which talks about the variables _a and _b instead of a and b).
Btw.: I think that the bug is "only" a completeness issue and not soundness critical, since the variables can only appear in the inInt(...) predicate and the original modality and nowhere else on the sequent.
In addition to the fix in the rules, this PR adds test cases (one provable and one unprovable) for each of the test cases, which hopefully will help in the future to detect such problems earlier.
Related Issue
This pull request fixes the only partially corrected #3353.
This PR addresses #3487.
Type of pull request
Bug fix (non-breaking change which fixes an issue)
There are changes to the (Java) code (new test cases)
There are changes to the taclet rule base (added \sameUpdateLevel constraints)
Ensuring quality
I made sure that introduced/changed code is well documented (javadoc and inline comments).
I added new test case(s).
Additional information and contact(s)
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.
The recently merged PR #3353 only partially fixes the overflow checking: All the taclets in
integerAssignment2UpdateRules.key, which add another formula to the sequent for the overflow check, are missing the\sameUpdateLevelconstraint. This can lead to unprovable overflow check branches (see theinIntline in the screenshot below, which talks about the variables_aand_binstead ofaandb).Btw.: I think that the bug is "only" a completeness issue and not soundness critical, since the variables can only appear in the inInt(...) predicate and the original modality and nowhere else on the sequent.
In addition to the fix in the rules, this PR adds test cases (one provable and one unprovable) for each of the test cases, which hopefully will help in the future to detect such problems earlier.
Related Issue
This pull request fixes the only partially corrected #3353. This PR addresses #3487.
Type of pull request
\sameUpdateLevelconstraints)Ensuring quality
Additional information and contact(s)
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.