Skip to content
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

Add a kani::futures library containing block_on #1427

Merged
merged 4 commits into from
Jul 30, 2022

Conversation

fzaiser
Copy link
Contributor

@fzaiser fzaiser commented Jul 29, 2022

Description of changes:

Following up on #1414, this adds a kani::block_on function to drive futures to completion in Kani. The block_on function from futures or tokio do not work because Kani does not understand the thread primitives these implementations use.

Callouts:

I had to add #[inline] annotations to work around the linking issue #1425. But inlining makes sense for these functions anyway (they're small and do basically nothing), so this is not a problem.

Testing:

  • How is this change tested? Added a test in tests/kani/AsyncAwait/main.rs

  • Is this a refactor change? No

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

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

@fzaiser fzaiser requested a review from a team as a code owner July 29, 2022 19:41
library/kani/src/futures.rs Show resolved Hide resolved
library/kani/src/futures.rs Show resolved Hide resolved
library/kani/src/futures.rs Outdated Show resolved Hide resolved
@fzaiser fzaiser self-assigned this Jul 30, 2022
@fzaiser fzaiser merged commit 16f10e9 into model-checking:main Jul 30, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
No open projects
Status: Done
Development

Successfully merging this pull request may close these issues.

2 participants