Ted Kaminski
Ted Kaminski
It might make things easier for customers if they can simply make use of a github action to run Kani on their code. Ideally this would be as simple as...
#1497 will give a basic report on features Kani does not support in a crate and its dependencies. We should be able to try running a crate's existing test suite...
In https://github.com/model-checking/kani/pull/1400 we got a nice look at what features are unimplemented in the top-100 crates. I'd like to make this less hacky and integrate it as a part of...
### Description of changes: I'm headed out on vacation, so this is a partial PR. It might be mergeable as-is though, it just doesn't complete the whole task. 1. Concentrates...
``` Failed check: assertion ``` Should state what function and that it is missing.
We should document not just how to build Kani but how to install it (just as a normal `cargo install` would do) but from source. Further, we need to improve...
In short: build with `cargo test --no-run` not `cargo build`, making the current `--tests` option the default (and only) build mode. There are three currently open issues related to this...
This was previously invisible because we either (1) had codegen hooks, so we replaced calls during codegen, or (2) were generic, and so got monomorphized into dependent crates. But as...
Kani currently doesn't complain until the verification fails because we hit the `assert(false)`, maybe we should issues warnings earlier in the compilation process.
# `any`, `Arbitrary` and `Invariant` * [ ] The current implementation of `Invariant` is basically inviting undefined behavior. For instance, an invariant like "this enum must match one of its...