Logical Infrastructure for final values independent from the heap #3189
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
although not really elegantly engineered. The dependency would have to be handed in too deep. I remember the value of a flag in a thread local variable instead.
* master: (213 commits) fix dependencies for gradle 7+ Add setting to disable load examples dialog window Fix KeYProject#1566 fixed NPE with regroup search filter improved and corrected wrapLine specification and implementation Fixes issues with displaying syntax errors [Fix] Intersection construction of location sets in TemrBuilder adding a KeY-proven line wrapping method. change jetbrains annotation against jsr305 one. fix test cases fix loading problems Revert "restore old order" restore old order fix NPE in KeyIO.Loader rename lex() to createLexer() add comments switch back to ImmutableList remove if statement clean up comments added comment to KeYParser.g4 as requested ... # Conflicts: # key/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key
# Conflicts: # key/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java # key/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java # key/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLTranslator.java
|
Does this also affect the proof management tool of @WolframPfeifer? Checking whether taclet option was active, while a constructor appeared in a method-frame? |
13 tasks
|
This PR has been superseded by #3495 based on the same (but rebased) code changes |
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 is a copy of Merge Request !318 at gitlab. See also there for an extensive discussion on the subject.
Constructors
This mechanism must not be used when verifying a constructor or if constructors are planned to be inlined. In these cases, final field are writable. We suggest to implement this mechanism with a taclet option such that it can be switched off -- or even switched off automatically if need be.
Example
This file that can be closed automatically with this encoding. It cannot be closed in KeY itself since the
finalmodifier is not considered in KeY.A.java
Remaining issues
This is work in progress. There may be parts of KeY where this change has unexpected consequences.
FinalArray<T>which allows this for arrays too (well ...)Side note: The variable condition
\finalhas already been implemented by Daniel, but was not used till now. Thanks.