-
Notifications
You must be signed in to change notification settings - Fork 25
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Print real condition in if labels #3222
Conversation
Codecov Report
@@ Coverage Diff @@
## main #3222 +/- ##
============================================
- Coverage 37.85% 37.84% -0.02%
- Complexity 16892 16895 +3
============================================
Files 2052 2054 +2
Lines 125443 125488 +45
Branches 21216 21227 +11
============================================
+ Hits 47487 47491 +4
- Misses 72104 72144 +40
- Partials 5852 5853 +1
... and 2 files with indirect coverage changes 📣 Codecov offers a browser extension for seamless coverage viewing on GitHub. Try it in Chrome or Firefox today! |
key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java
Outdated
Show resolved
Hide resolved
key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java
Outdated
Show resolved
Hide resolved
key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java
Outdated
Show resolved
Hide resolved
e1b479b
to
6260311
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks, nice feature! I have two minor complaints (mainly about the documentation), apart from that, the PR is fine.
For documentation: Since branch names are stored in proofs, unfortunately this PR does not take effect when loading proofs.
In the future, we could think of overwriting saved branch labels with the better ones from this PR. However, this would also overwrite manually named branches (I am not sure if anyone uses the feature of manual branch names ...).
This PR modifies the labels in the proof tree to show the actual condition of ifs instead of the boolean variable introduced by the unfold taclet. With this change, the branch labels in the proof tree are much more useful.