-
Notifications
You must be signed in to change notification settings - Fork 89
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
Emit an error when proof_for_contract function is not found #3609
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.
I wonder if this should be done as part of kani::middle::check_reachable_items
which is where we run our validations. The main advantage is that we emit all possible configuration errors.
I won't block this PR though since it's a clear improvement to the existing flow. Thanks!
That makes sense. I'll check if it's easy to do that. |
I moved the check to |
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.
Thanks!!!
Currently, Kani panics if the function specified in the
proof_for_contract
attribute is not found (e.g. because the function is not reachable) (see #3467). This PR adds an error message pointing out the issue.Towards #3467
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.