-
Notifications
You must be signed in to change notification settings - Fork 152
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Remove references to java backend from main regression test suite #3244
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Overall looks good.
But there are still a few warnings printed by the haskell backend for missing no-evaluators
.
We should try to keep the output clean so it's easier to spot where something fails.
There was one remaining test left that still had warnings about functions without evaluators. I fixed it. Please re-review. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There are still a few warnings thrown from the haskell backend through kprove-legacy, but they are small. We may want to tackle those with another update to remove kprove-legacy.
I agree that should be a separate pr. |
Here we remove all calls to the Java backend from the main test suite in preparation for deletion of the backend itself.
Tests were converted to the llvm or haskell backend from the Java backend, run, and then gradually refined until it was either clear the test relied on behavior of the Java backend that couldn't easily be replicated, in which case we deleted the test, or until the test behaved in a sensible fashion, at which point test output files were updated as needed.
We also remove references to a couple different command line flags which will be deleted when the Java backend is removed.