model-checking
Add an option to turn contract clauses into assertions
Requested feature: Enable contract checking without stubbing. Use case: Be able to detect if a function violate the contract of any of its dependencies. This can be very helpful for debbuging verification failures due to API misuse. This is especially important for functions that are only be annotated with safety contract, and for those that are not eligible for stubbing. Link to relevant documentation (Rust reference, Nomicon, RFC):
Actually, should we just insert contracts clauses as assertions so they can be used with playback? When #[cfg(not(kani))] we already ignore the contract.
Branch with progress so far: https://github.com/jaisnan/kani/tree/turn-clause-to-contract
