search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.27k stars 96 forks source link

Add an option to turn contract clauses into assertions #3326

Open celinval opened 4 months ago

celinval commented 4 months ago

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):

celinval commented 4 months ago

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.

jaisnan commented 3 weeks ago

Branch with progress so far: https://github.com/jaisnan/kani/tree/turn-clause-to-contract