kani
kani copied to clipboard
model-checking
Kani Rust Verifier
In an example introduced in #1131 , we reproduced an issue where a high offset causes a "wrapping around" behavior in CBMC. There is more information on the test, but...
These intrinsics can affect the value of a place that may be read later using safe code. It is not immediate UB to write the value to the allocation space,...
> An enum must have a valid discriminant, and all fields of the variant indicated by that discriminant must be valid at their respective type. https://doc.rust-lang.org/reference/behavior-considered-undefined.html
> A fn pointer value must be non-null. https://doc.rust-lang.org/reference/behavior-considered-undefined.html
> - A reference or [Box](https://doc.rust-lang.org/alloc/boxed/struct.Box.html) must be aligned, it cannot be [dangling](https://doc.rust-lang.org/reference/behavior-considered-undefined.html#dangling-pointers), and it must point to a valid value (in case of dynamically sized types, using the actual...
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...
I ran a small experiment to check the equivalence of the two versions of the greatest-common-divisor function, one is written with a loop and one in recursion. I tried this...
I tried this code: ```rust #[kani::proof] fn vec_failure() { let value: u8 = 1; /* set to zero and it passes */ let count: u16 = kani::any(); let vector: Vec...
Add opt-in JSON export (--export-json ) to emit structured verification results (metadata, per-harness outcomes, CBMC stats). Improves Kani by enabling reliable machine-readable output for external tools and applications. Context: Current...
