Zyad Hassan

Type mismatch for `FnDefStruct`

3

Running Kani on harnesses in the `s2n-quic-transport` crate in [this branch](https://github.com/aws/s2n-quic/tree/camshaft/varint-kani) of `s2n-quic` results in a CBMC error: ``` : function call: parameter "_RINvNtCshBEb14mhtvp_4core3cmp6max_byjNvYjNtB2_3Ord3cmpECsPu7NGxNZ36_5tokio::1::var_3::compare" type mismatch: got struct_tag * identifier:...

Kani's assert macro implementation bypasses some compile-time checks

2

With PR #797, Kani's implementation of the assert macro's second form that accepts a custom message bypasses several compile-time checks. For example, while `rustc` errors out on the following program:...

In https://github.com/model-checking/kani/pull/1426, new methods for arithmetic overflow operations were added that rely on CBMC's new, more efficient operations: `add_overflow_result`, `sub_overflow_result`, and `mul_overflow_result`. There are still a few usages of the...

cargo kani --tests fails on crates with integration tests

4

Steps to reproduce: 1. cargo new foo 2. cd foo 3. Append the following to `src/main.rs`: ```rust #[cfg(test)] mod tests { #[test] #[kani::proof] fn check() { assert!(1 + 1 ==...

Parallelize the conversion of symbol tables to goto binaries

1

Requested feature: Currently, Kani converts the symbol table for each crate into a goto binary through calling CBMC's `symtab2gb` executable on one crate at a time. For packages with many...

Find out Bolero harnesses that cannot be run with Kani, and why they can't be run.

Checking result of repeated operation takes long

4

I tried this code: ```rust #[kani::proof] #[kani::unwind(2)] fn check_repeat() { let x: u32 = kani::any(); let y: u32 = kani::any(); let o1 = x.saturating_mul(y); let o2 = x.saturating_mul(y); assert_eq!(o1, o2);...

Some proof harnesses may intentionally verify some piece of code up to a certain bound, in which case, one would want to disable the unwinding assertions. There is currently no...

Verification time increased by 7X on an s2n-quic harness

2

Noticed today that s2n-quic's `vectored_copy_fuzz_test` harness takes 30 minutes to prove, even though a few weeks ago, it only took 4 minutes. The culprit commit turned out to be ab0f2add72b9fd49a8410b7de981702cc3e784d6...

- [ ] https://github.com/model-checking/kani/issues/1657 - [ ] https://github.com/model-checking/kani/issues/1673 - [ ] https://github.com/model-checking/kani/issues/1226