kani

kani copied to clipboard

**Proposed change:** Avoid the duplication of code in `kani-cov` by extracting commonly shared data structures like `CheckStatus` into a separate crate, and force `kani-cov` and whichever modules (e.g., postprocessing) that...

adpaco-aws

FFI stubbing for libc crate only works if libc crate is imported via `feature(rustc_private)`

4

I tried this code: ```rust #[allow(unused)] mod stubs { use libc::{c_int, c_long}; pub unsafe extern "C" fn sysconf(_input: c_int) -> c_long { 1 } } #[kani::proof] #[kani::stub(libc::sysconf, stubs::sysconf)] fn verify_sysconf_stub()...

roypat

ICE: `failed to resolve instance for <dyn ThriftService as ThriftService>::foo`

1

I tried this code: ```rust use std::future::Future; pub trait Service { type Response; type Future: Future; } pub trait ThriftService: Service { fn foo(&self) {} } #[kani::proof] fn main() {...

matthiaskrgr

**Proposed change:** Upgrade the versions of the [actions/upload-artifact](https://github.com/actions/upload-artifact) and [actions/download-artifact](https://github.com/actions/download-artifact) actions to v4. **Motivation:** The version we're currently using for the [actions/upload-artifact](https://github.com/actions/upload-artifact) and [actions/download-artifact](https://github.com/actions/download-artifact) actions (v3) is scheduled for deprecation...

zhassan-aws

Stacked Borrows In Kani -- Extend Feature to handle more code

2

Currently, Stacked Borrows is implemented in the feature branch features/stacked_borrows. However, to merge it into the main code-base, the following updates are needed: 1. We need to add regression tests...

jsalzbergedu

Dependency upgrade resulting from `cargo update`.

github-actions[bot]

Introduce compiler timing script & CI job

6

We have an existing `benchcomp` script to measure Kani's performance in CI, but it is prone to noise and only focuses on the end-to-end performance of compilation and verification together,...

AlexanderPortland

Stub panics during MIR transformation

1

Modifies the `RustcIntrinsicsPass` to stub out panic functions during body transformation at the MIR level. This avoids having to bring in (and do transformation passes on) the large amounts of...

AlexanderPortland

Handle enums with zero or one variants when deriving `BoundedArbitrary`. Resolves #4170 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache...

zhassan-aws

Bloated MIR remains for `Result` functions

1

**Proposed change:** Maybe some strategy for stubbing all string formatting could be helpful for bloat and not affect our correctness? At the very least finding a way to stub `unwrap_failed()`...

AlexanderPortland