kani
kani copied to clipboard
model-checking
Kani Rust Verifier
CBMC has a json interface, which can be used instead of commandline flags. It might be a cleaner way to go. https://github.com/diffblue/cbmc/tree/develop/regression/cbmc/json-interface1
Currently we do nothing, which seems likely to be incorrect.
Requested feature: The rust compiler has a rich set of tests that exercise a lot of corner cases. It would be useful to integrate some of those tests in the...
RMC compiles each Rust crate to a goto binary, and then uses the CBMC linker to link those binaries together. It is possible that the CBMC and Rust linkers may...
RMC translates MIR to a typed IR that models the GOTO language, which is then translated into Irep, which are emited as a json blob, and converted by symtab2gb into...
In #804 I made an attempt to implement `frem_fast` (floating-point remainder) as `%`, but the test I wrote was failing even though the same expression is being used to codegen...
In #804 we added support for fast math intrinsics but in the positive test cases for multiplication and division we could not compare the results with regular multiplication/division due to...
Depends on source-based coverage reports. The reorganization will probably follow a chapter-like structure that follows the Rust reference.
Add call graph analysis to scanner in order to find the distance between functions in a crate and unsafe functions. For that, we build the crate call graph and collect...
**Proposed change:** Change the raw coverage results so that the filenames are absolute and indexing them (e.g., in `kani-cov`) is faster. **Motivation:** The APIs to retrieve function coverage results in...