model-checking / kani

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

Function Contracts: Better error messages #3273

Open pi314mm opened 3 months ago

pi314mm commented 3 months ago

tests/expected/function-contract/history/ui/ currently contains several failing test cases revolving around the old history expressions. These error messages need to be enhanced to provide clarity to the user.

Additionally, the macro rule of assert_spanned_err needs to be adapted to have better error messages upon usage and proper documentation.