Carolyn Zech
Carolyn Zech
This is a tracking issue for fixing the [known quantifiers limitation](https://model-checking.github.io/kani/reference/experimental/quantifiers.html#types-of-quantified-variables) that the ranges must be usizes. I tried this code: ```rust #[kani::requires(min != 0 && max != 0)] #[kani::ensures(|result|...
Document the experimental list subcommand feature in our book and stabilize the feature.
Requested feature: Make proof harnesses optional, when possible Use case: There are plenty of "boilerplate harnesses" that look something like this: ```rust fn foo(x: u8, y: u8) { ... }...
`parse_stubs` uses `resolve_fn_path` to resolve the target of the stub: https://github.com/model-checking/kani/blob/e229b691c9904c77637620070267b3939b89737a/kani-compiler/src/kani_middle/attributes.rs#L859-L862 while `interpret_for_contract_attribute` calls `resolve_mod`, https://github.com/model-checking/kani/blob/e229b691c9904c77637620070267b3939b89737a/kani-compiler/src/kani_middle/attributes.rs#L246-L249 which calls `resolve_fn` instead https://github.com/model-checking/kani/blob/cc367b34beeda1f3622c6f2daa05838c9ab0cab1/kani-compiler/src/kani_middle/attributes.rs#L335-L340 Investigate why this discrepancy exists and if alleviating it...
https://github.com/model-checking/kani/pull/3121 introduced the `kani-cov` tool. We should document it so that our users know it exists and how they can use it.
During contract instrumentation, we annotate the closures we add during instrumentation with `#[kanitool::is_contract_generated]`. However, calling `tcx.get_attrs_unchecked` on such a closure does not return this tool attribute. This means that if...
I tried this code: ```rust #[kani::proof] fn delayed_ub_slices() { unsafe { // Create an array. let mut arr = [0u128; 4]; // Get a pointer to a part of the...
Requested feature: Add support for coroutine closures Use case: async closures Link to relevant documentation (Rust reference, Nomicon, RFC): [RFC](https://rust-lang.github.io/rfcs/3668-async-closures.html), [Addition to StableMIR](https://github.com/rust-lang/rust/pull/134295) Test case: (Test taken from https://github.com/rust-lang/rust/blob/master/tests/codegen/async-closure-debug.rs) ```rust...
**Proposed change:** Make https://github.com/model-checking/kani/blob/main/kani-compiler/src/kani_middle/resolve.rs and https://github.com/model-checking/kani/blob/main/kani-compiler/src/kani_middle/attributes.rs use `rustc_public` APIs whenever possible. **Motivation:** Right now there's an odd mix of stable and unstable code there that makes the logic harder to...
**Proposed change:** Refactor path handling for contracts and stubs to check for resolution errors once at the start of codegen; then maintain state about resolved functions and paths. **Motivation:** https://github.com/model-checking/kani/pull/4249...