-
Notifications
You must be signed in to change notification settings - Fork 97
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
Fix std overrides in crates where std is used as a feature #2194
Conversation
fn foo() { | ||
let x: i32 = kani::any(); | ||
let y = 0; | ||
std::debug_assert!(x + y == x, "Message"); |
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.
Should we also have a test where the assertion fails?
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 don't think this is necessary, since we're mainly checking that compilation goes through. There are many other tests that check for failing assertions.
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'm worried that this is getting out of control. We should investigate a more robust solution.
Thanks for the quick fix though.
Description of changes:
Kani's std overrides relied on creating an alias for
core::assert
up front to use for error checking in various macros (assert
,panic
, etc.). Creating the alias upfront doesn't work properly in crates withno_std
wherestd
is used as a feature (see #2187). This PR updates the std overrides to usecore::assert
directly when anstd
feature is enabled.Resolved issues:
Resolves #2187
Related RFC:
Optional #ISSUE-NUMBER.
Call-outs:
To avoid code duplication, I tried creating a macro that calls
__kani__workaround_core_assert
undernot(std)
andcore::assert
otherwise. However, I ran into the same error reported in #2187.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.