kani
kani copied to clipboard
model-checking
Kani Rust Verifier
The Machine Readable Output Design needs to be approved by the Team once before merging - this can be done with a simple RFC doc or on this issue.
Requested feature: Enable verification of code that uses C-FFI Use case: Any code that has mixed language calls, and the user wants to verify Link to relevant documentation (Rust reference,...
I tried this code: https://github.com/danielsn/kani/tree/kani-1743 using the following command line invocation: ``` cd memory_model cargo kani ``` with Kani version: 0.11 I expected to see this happen: Kani verified the...
I've tried with the below code for mocking a mmio access. ``` const BUFFER: *mut u32 = 0xb8000 as *mut u32; #[cfg(kani)] #[kani::proof] fn test_write() { let val = 12;...
RMC handles dynamic traits by making a vtable for each trait, which maps virtual calls to the function pointer that implements the call. As of 2021-09-01, our implementation of dynamic...
RMC operates at the MIR level. It is possible that the MIR generated by Rustc may make implementation decisions that hide UB. ## Likelihood: We do not have data on...
While some aspects of object layout are specified by the standard, many others are not. In fact, many aspects of object layout are left explicitly implementation-defined, to allow the compiler...
Instead of taking a c in gen_function_local_variable, maintain a map from fname to int, and generate fresh variables that way. Actually: why is this index needed at all? It seems...
`POINTER_OBJECT` is used by `offset_from` to check that two raw pointers point to the same object. We can't do this with C. At the moment, I assign `POINTER_OBJECT(value) 0` no...
