Add exception patterns case study & re-enable elect.pvl #635
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
Previously all usages of String were resolved to java.lang.String, while Exception#getMessage was resolved with return type PrimitiveSort.String. By resolving imported methods with return type String to java.lang.String, and converting java.lang.String to PrimitiveSort.String after all necessary external classes have been loaded, the problem is resolved, as the import and type resolution is now consistent.
Previously return values were not coerced to the return type of the method. This caused "return null" not to be converted into "return VCTNone", because the return type wasn't coerced to VCTOption, but was just left as-is. Now return values are type-coerced to the method return type, similarly as values that are being assigned to a variable.
PropagateInvariants did not rewrite signals clauses. Enabling this caused several examples to fail because the semantics of context_everywhere changed. This change required extra permission annotations.
First an explicit folder structure was needed for jstar, but this is no longer necessary. Additionally, the abstract keyword is also no longer needed in one of the tests.
|
Kudos, SonarCloud Quality Gate passed! |
Vescatur
reviewed
Jul 6, 2021
Comment on lines
1
to
4
| // -*- tab-width:2 ; indent-tabs-mode:nil -*- | ||
| //:: case LeaderElect | ||
| //:: tool silicon | ||
| //:: suite problem-fail | ||
| //:: option --check-history |
There was a problem hiding this comment.
I think this example is missing a Verdict.
Vescatur
reviewed
Jul 6, 2021
|
Kudos, SonarCloud Quality Gate passed! |
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.
Add tests made for an exception patterns case study, and fix any bugs related to those tests. Also re-enable elect.pvl, as it is no longer broken.