You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
// indirect.rsexterncrate kani;use std::convert::TryFrom;/// Constrain `val` to be a valid character.#[kani::requires(u32::from(_char) == val)]#[kani::ensures(|res| *res == _char)]pubfnindirect_assumption(val:u32,_char:char) -> char{
char::try_from(val).unwrap()}mod verify {usesuper::*;use kani::Arbitrary;#[kani::proof_for_contract(indirect_assumption)]fncheck_indirect_contract(){indirect_assumption(kani::any(), kani::any());}/// This harness that encodes the pre-condition using`kani::assume` succeeds#[kani::proof]fncheck_indirect(){let val = kani::any();let c = kani::any();
kani::assume(u32::from(c) == val);indirect_assumption(val, c);}}
using the following command line invocation:
kani indirect.rs -Z function-contracts
with Kani version: 0.53.0-dev
I expected to see this happen: Verification should succeed
Instead, this happened: Verification failed.
Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime
File: "/home/ubuntu/.rustup/toolchains/nightly-2024-07-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs", line 1679, in std::result::unwrap_failed
The text was updated successfully, but these errors were encountered:
Verification succeeds in Kani v0.56. git bisect revealed that #3305 fixed the issue. @celinval I can go ahead and close, but I see you have an open PR for fixme tests that references this issue, so wanted to loop you in first. (It doesn't seem like #3305 was meant to fix this problem, so I can do some investigation as to why it did if we think it's worth it).
I tried this code:
using the following command line invocation:
with Kani version: 0.53.0-dev
I expected to see this happen: Verification should succeed
Instead, this happened: Verification failed.
The text was updated successfully, but these errors were encountered: