kani
kani copied to clipboard
model-checking
Kani Rust Verifier
Since Kani 0.57.0, support for OS's with older versions of glibc (e.g. 2.26) has been dropped, e.g. AL2, Ubuntu 18.04, etc. The result is that on those OS's, Kani has...
``` ~/rmc/tests$ git grep union kani/Unit/main.rs:/// - As a variable type in a struct or union kani/Unit/main.rs:union U { ``` Just one test of a `repr(C)` `union`. We uh, could...
Requested feature: a finer-grained unwinding values Use case: a big harness containing multiple loops or iterators Currently, the unwinding attribute(`#[kani::unwind(x)]`) could be applied to the granular of a harness. This...
https://github.com/rust-lang/project-stable-mir/issues/95 When the upstream issue is fixed, remove the workaround found in /kani-compiler/src/kani_middle/reachability.rs for function [filter_crate_items](https://github.com/model-checking/kani/blob/b93e591556d1aaf054b73148604256521a0424fa/kani-compiler/src/kani_middle/reachability.rs#L77)
This is a tracking issue to disable CMBC NaN checks since producing a NaN does not seem to be Undefined Behavior, continued from #3873
It would be nice if Kani worked on Windows. Also you should probably say somewhere near the start of the Readme or book that it doesn't.
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...
Towards #3769 If no default unwind value is given, we default it to 1 to prevent the harness from running forever. By submitting this pull request, I confirm that my...
Currently Kani does not contain a default unwind, and users end up having issues with Kani consuming tons of memory, and unexpectedly freezing their computer. Instead, we should create an...
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...