kani

kani copied to clipboard

I tried this code: ```rust #[derive(kani::BoundedArbitrary)] enum Foo { A(#[bounded] String), //B(#[bounded] String), } #[kani::proof] fn check_enum() { let _foo = kani::bounded_any::(); } ``` using the following command line invocation:...

zhassan-aws

Autoharness: Derive `Arbitrary` for structs and enums

1

While generating automatic harnesses, derive `Arbitrary` implementations for structs and enums that don't have implementations. ## Implementation Overview 1. In `automatic_harness_partition`, we mark a function as eligible for autoharness if...

carolynzech

Add loop-contracts support for `for` loop

1

This PR adds loop-contracts support for `for` loop for 4 types: array, slice, Iter, Vec, Range, StepBy, Map, Chain, Zip, Enumerate. Main ideas: `for` loop implementation: A `for` loop of...

thanhnguyen-aws

Relevant upstream PR: https://github.com/rust-lang/rust/pull/137944 (Sized Hierarchy: Part I). This PR implements a part of [RFC 3729](https://github.com/rust-lang/rfcs/pull/3729), which prescribes a hierarchy of `Sized` traits. Notably, this disallows instantiation of `size_of_val` and...

tautschnig

Ensure that contract closures are FnOnce

1

Rust believes that Kani's contract closures are `FnMut`. This prevents us from writing contracts for functions that return mutable references to their input arguments (#3764). To ensure Rust correctly infers...

vonaka

Updating Rust toolchain from nightly-2025-06-17 to nightly-2025-06-18 requires source changes. The failed automated run [can be found here.](https://github.com/model-checking/kani/actions/runs/15722849695) Please review the changes at https://github.com/rust-lang/rust from https://github.com/rust-lang/rust/commit/45acf54eea118ed27927282b5e0bfdcd80b7987c up to https://github.com/rust-lang/rust/commit/f3db63916e541ff039ac3cd7364c2d612749b61b. The...

github-actions[bot]

Loop Contract Issue: Check some_var is assignable

1

I tried this code: ```rust #![feature(stmt_expr_attributes)] #![feature(proc_macro_hygiene)] fn func(x: usize) { let mut j = 0; const CHUNK_SIZE: usize = 32; #[kani::loop_invariant(j Instead, this happened: ``` ** 3 of 235...

MinghuaWang

As far as I can tell we don't take advantage of GitHub's caching feature for CI. I think even just caching the cargo registry & kani dependencies could help with...

AlexanderPortland

Measure compiler performance and overall execution time as part of our benchmarks

3

**Proposed change:** Our benchmarks today only measure changes to verification time. We should also include overall execution time and the compilation time. **Motivation:** Overall execution time is probably the most...

celinval

I tried this code: ```rust #[kani::requires(*val != 0)] unsafe fn foo(val: &mut u8) -> &mut u8 { val } #[kani::proof] fn harness() { let mut x: u8 = kani::any(); unsafe...

carolynzech