Fabian Zaiser
Fabian Zaiser
This was discovered in #1332, but also occurs in a synchronous context: ```rust #[kani::proof] pub fn main() { let coll: Result = std::iter::empty().collect(); assert_eq!(Ok(vec![]), coll); } ``` Running this with...
The code of `closure_sig` is copy-pasted from `fn_sig_for_fn_abi` in `compiler/rustc_middle/src/ty/layout.rs`. We may have to do something similar for generators (#416), so it would be good if we could use the...
The term "unwind" is overloaded for Rust developers. Unwinding is what Rust does when panicking (unless you set `panic = abort`). In Kani, it means the loop unrolling bound passed...
Kani's translation of `async` harnesses involves a loop (to poll the future repeatedly) and its translation of `.await` involves a loop as well. As a consequence, (almost?) all `async` harnesses...
I went through the tokio's test suite and identified a couple of test cases that don't use a lot of I/O (or replace it with a mock) so that they...
*Requested feature:* async/await *Use case:* to support popular libraries like `tokio` *Link to relevant documentation (Rust reference, Nomicon, RFC):* * [async/await primer](https://rust-lang.github.io/async-book/01_getting_started/04_async_await_primer.html) * [RFC proposing async/await (partially outdated)](https://github.com/rust-lang/rfcs/blob/master/text/2394-async_await.md) Test case...
For asynchronous code, it's important to be able to spawn tasks. Since `tokio::spawn` or something similar will be difficult to support, we should provide our own version that is optimized...
As mentioned in https://github.com/model-checking/kani/pull/1452#discussion_r938945779, users will often be greeted by messages of the form `Kani does not support concurrency for now. `{}` in {} treated as a sequential operation.`. For...
If you clone the [tokio repository](https://github.com/tokio-rs) and run `cargo kani`, you get a lot of warnings about unsupported features, one of them is `drop_in_place`, example: ``` warning: Found the following...