key
key copied to clipboard
Fix for the LoopInvariantConfigurationDialog
Related Issue
This PR fixes a bug that prevented the interactive provision of a loop invariant.
Intended Change
It should be possible to enter loop invariants manually.
Type of pull request
- [x] Bug fix (non-breaking change which fixes an issue)
- [ ] Refactoring (behaviour should not change or only minimally change)
- [ ] New feature (non-breaking change which adds functionality)
- [ ] Breaking change (fix or feature that would cause existing functionality to change)
- [x] There are changes to the (Java) code
- [ ] There are changes to the taclet rule base
- [ ] There are changes to the deployment/CI infrastructure (gradle, github, ...)
- [ ] Other:
Ensuring quality
- [ ] I made sure that introduced/changed code is well documented (javadoc and inline comments).
- [ ] I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
- [ ] I added new test case(s) for new functionality.
- [x] I have tested the feature as follows: Applied a manually entered loop invariant
- [ ] I have checked that runtime performance has not deteriorated.
Additional information and contact(s)
The problem was if no "free modifies"/"free assignable" was available then creating the whole modifies set "union(freeMod, mod)" led to a NullPointerException. The fix uses "strictly_nothing" as default for free assignables of loops, if non given.
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.