Set statement: Check assignee for validity #3195
Closed
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
mattulbrich
requested changes
Jul 15, 2023
key.core/src/main/java/de/uka/ilkd/key/rule/SetStatementRule.java
Outdated
Show resolved
Hide resolved
key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java
Outdated
Show resolved
Hide resolved
key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java
Outdated
Show resolved
Hide resolved
key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java
Outdated
Show resolved
Hide resolved
key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
Outdated
Show resolved
Hide resolved
key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
Outdated
Show resolved
Hide resolved
key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
Outdated
Show resolved
Hide resolved
key.core/src/test/java/de/uka/ilkd/key/speclang/SetStatementTest.java
Outdated
Show resolved
Hide resolved
key.core/src/test/java/de/uka/ilkd/key/speclang/SetStatementTest.java
Outdated
Show resolved
Hide resolved
|
This PR seems to replace set statements as copy assignments with proper set statements that do not have an Java-AST for the assigned value. If that is so, that would be great and expressions can be supported in set statements like quantifiers etc. |
The Recoder removal branch does this except for set statements. |
* origin/main: (331 commits) increase spotless version (and thus also eclipse formatter) to fix missing space in instanceof formatting Spotless and fix rebase Some additional minor fixes and spotlessApply Update `collect(Collectors.toList())` to `toList()` Introduction of record classes where it seems useful. Refactor: Introduce a pattern variable were possible. Translate large string concatenations into raw string literal (text blocks) update beanshell version in recoder's dependencies Switch to Java 17 for KeY-2.14.0 repair POM generation using afterEvaluate Adding license to KeY files Adding license to Java files add metadata for POM generation and update templates for license headers Bump ch.qos.logback:logback-classic from 1.4.8 to 1.4.11 Fix bug in icon selection update samplesIndex.txt Repair example index better default keyboard shortcuts, corrected docs URL, cleanup removing the SmansEtAl example from first touch change docking frames dependencies to maven central versions ...
|
I have removed the @mattulbrich You can re-review. |
* origin/main: (180 commits) Use Amazon's Corretto add caching for gradle dependencies Update to Java 21 Runtime for testing Add HelpInfo to more extensions Add help buttons to extension settings Use pattern matching to avoid cast Change default notification setting to unfocused Renaming from reviewer suggestion (got lost when splitting the PR) Minor cleanup Prevent possible NullPointerException. Cleanup. Remove last usage of the legacy matcher. Check only new terms for well-typedness Move static metavariable cache to service caches Minor cleanup incl. spotless changes Use array of assumes instantiations Preparation for parallel prover engine - make Strategies stateless by introducing a specific explicit state object for TermBuffers and the Backtracking Manager This will allow strategies to execute in parallel Update keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java Update keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java Some cleanup and proper switching to automode Avoid access of non-private field in synchronized context ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/speclang/njml/PreParser.java
wadoon
added
Review Request
This reverts commit c539948. Reason for reverting: The implemented changes to pretty printing assertions raised exceptions during interactive application. However this change has nothing to do with the original intention of this branch.
Undoing some changes that accompanied the reverted commit before this.
|
This does not fully reach its potential: The JavaCC parser still runs over the expression which is set; this is unlike in the case for JML assertions where all expressions are supported. Hence still raises an exception for a boolean ghost variable b. |
|
I reverted commit c539948 since that has nothing to do with the problem here and introduces a GUI runtime exception due to pretty printing. The issue can be separated and be resolved properly elsewhere. |
it makes the code more conservative.
|
(this is WIP. forced updates to the branch are not unlikely in the near future.) |
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.
Replaces set statements as copy assignments with proper set statements that do not have an Java-AST for the assigned value.
Pretty much copy-pastes what JML asserts do.