Print real condition in if labels #3222
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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! |
unp1
reviewed
Jul 26, 2023
key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java
Outdated
Show resolved
Hide resolved
wadoon
reviewed
Aug 20, 2023
key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java
Outdated
Show resolved
Hide resolved
wadoon
reviewed
Aug 20, 2023
key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java
Outdated
Show resolved
Hide resolved
wadoon
added
Pending
Under Review
FliegendeWurst
force-pushed
the
ifLabel
branch
from
e1b479b
to
6260311
Compare
FliegendeWurst
added
Review Request
WolframPfeifer
approved these changes
Nov 3, 2023
There was a problem hiding this comment.
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 ...).
key.core/src/main/java/org/key_project/proof/LocationVariableTracker.java
Show resolved
Hide resolved
WolframPfeifer
added
Reviewer Feedback
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.