Add proof for Result method `check_unwrap_unchecked`

model-checking / verify-rust-std

Verifying the Rust standard library

https://model-checking.github.io/verify-rust-std/

Other

9 stars 7 forks source link

Add proof for Result method `check_unwrap_unchecked` #35

Open jaisnan opened 2 weeks ago

jaisnan commented 2 weeks ago

Adds a simple contract that checks for memory safety in check_unwrap_unchecked. Also useful for my secret agenda of testing the PR workflow in production.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

jaisnan commented 2 weeks ago

As shown by the CI run here, this proof fails verification with the following property failure

Check 158: panicking::assert_failed_inner.assertion.2
     - Status: FAILURE
     - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime"
     - Location: library/core/src/panicking.rs:408:17 in function panicking::assert_failed_inner