Make pre- and post-conditions obey behavioral subtyping #5825
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
…ns into excess-ecm-precursors
…adoc into excess-ecm-precursors
…sModified into excess-ecm-precursors
…doc into excess-ecm-precursors
…doc into excess-ecm-precursors
…rnst/checker-framework into wpiPrepareMethodForWriting-parameters
…ing-parameters into excess-ecm-precursors
…ing-parameters into excess-ecm-precursors
…ess-ecm-precursors
…ess-ecm-precursors
|
@smillst This is ready for your review. |
…nto excess-ecm-precursors
…LEAN into excess-ecm-2
…LEAN into excess-ecm-2
smillst
requested changes
May 3, 2023
There was a problem hiding this comment.
I tried making test cases for this change, but I wasn't successful because I don't know when inference should be inferring pre/post conditions. (Can inference ever infer a precondition?) It would be helpful if this pull request contained at least one test case where a pre/post condition is inferred.
...rg/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java
Outdated
Show resolved
Hide resolved
.../main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java
Outdated
Show resolved
Hide resolved
| Pair<AnnotatedTypeMirror, AnnotatedTypeMirror> pair = entry.getValue(); | ||
| AnnotatedTypeMirror inferredType = pair.first; | ||
| AnnotatedTypeMirror declaredType = pair.second; | ||
| if (otherIsSupertype ? isPrecondition : !isPrecondition) { |
There was a problem hiding this comment.
This can be moved outside the loop.
There was a problem hiding this comment.
In the common case, I expect the loop not to be entered.
.../main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java
Outdated
Show resolved
Hide resolved
.../main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java
Outdated
Show resolved
Hide resolved
@EnsuresCalledMethods obey behavioral subtyping|
@smillst I have added tests and addressed your other feedback. Could you please re-review? |
smillst
approved these changes
May 4, 2023
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.
No description provided.