Check Expected Errors in Tests #126
Merged
Conversation
This file contains hidden or 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
rcosta358
commented
Nov 22, 2025
| public static void main(String[] args) { | ||
| @Refinement("InRange( _, 10)") | ||
| @Refinement("InRange(j, 10)") | ||
| int j = 15; |
Collaborator
Author
There was a problem hiding this comment.
Here we are getting a not found error instead of an argument mismatch error.
Needs to be fixed in the future by checking if the provided arguments match the alias definition.
CatarinaGamboa
approved these changes
Dec 4, 2025
Collaborator
CatarinaGamboa
left a comment
CatarinaGamboa
left a comment
There was a problem hiding this comment.
Niceee! As a follow up we should add these details in the testing section of the README.
| @@ -1,3 +1,4 @@ | |||
| // Error | |||
Collaborator
There was a problem hiding this comment.
why is this just error? we don't have a more specific type?
Collaborator
Author
There was a problem hiding this comment.
It's the most general case, a.k.a. CustomError, but we can introduce more specific errors in the future.
| @@ -1,3 +1,4 @@ | |||
| // Error | |||
| @@ -1,3 +1,4 @@ | |||
| // Error | |||
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 closes #105 by comparing the expected error with the actual error found for each test (it assumes each one contains exactly one error, and fails otherwise).
.expectedfile should be included with the expected error.The test suite now requires all failing tests to include the expected error (fails otherwise), providing more guarantees about the behavior of the verifier.