Skip to content

Conversation

celinval
Copy link
Contributor

@celinval celinval commented Feb 3, 2024

I tried applying #2983 fix, however, this would require user to import
__kani_workaround_core_assert. To fix that, I moved the definition to be under kani crate.

I replaced the existing fixme test. Initially I didn't check we had one, and I created a second one which is simpler (no cargo needed) but that also includes other cases.

Resolves #2187

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

I tried applying model-checking#2983 fix,
however, this would require user to import
`__kani_workaround_core_assert`. To fix that, I moved the definition to
be under `kani` crate.
@celinval celinval requested a review from a team as a code owner February 3, 2024 00:22
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Feb 3, 2024
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Awesome, thanks @celinval!

@tautschnig tautschnig merged commit 55a7f3e into model-checking:main Feb 5, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-EndToEndBenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Issue finding debug_assert in no_std crates when std enabled
4 participants