-
Notifications
You must be signed in to change notification settings - Fork 84
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
Report results as UNDETERMINED instead of SUCCESS if an unwinding assertion fails #889
Report results as UNDETERMINED instead of SUCCESS if an unwinding assertion fails #889
Conversation
1ca76d2
to
4e8ce4a
Compare
tests/expected/unwind_tip/expected
Outdated
@@ -1,2 +1,3 @@ | |||
UNDTERMINED |
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 assume this is a typo?
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.
Yes, fixed.
4e8ce4a
to
3250341
Compare
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!
Description of changes:
When an insufficient unwind value is specified and an unwinding assertion fails, Kani may report some checks as "SUCCESS" even though they may fail with a larger unwinding. To prevent giving this somewhat misleading result to the user, Kani will now report UNDETERMINED instead of SUCCESS if any unwinding assertion fails. The unwind tip that also gets emitted when an unwinding assertion fails:
should prompt the user to increase the unwind value.
Resolved issues:
Resolves #746
Call-outs:
Testing:
How is this change tested? Added one test
Is this a refactor change? No
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.