Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

PropProof is mistaking "invalid input" with "harness crash" #2550

Closed
YoshikiTakashima opened this issue Jun 21, 2023 · 3 comments · Fixed by #2554
Closed

PropProof is mistaking "invalid input" with "harness crash" #2550

YoshikiTakashima opened this issue Jun 21, 2023 · 3 comments · Fixed by #2554
Assignees
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@YoshikiTakashima
Copy link
Contributor

YoshikiTakashima commented Jun 21, 2023

I tried this code:

using the following command line invocation:

 mkdir .cargo; echo "paths =[\"/Users/ytakashl/propproof\"]" > .cargo/config.toml
cargo kani  --tests -p prost-types --default-unwind 3 --harness 'tests::check_duration_roundtrip'


SUMMARY:
 ** 1 of 445 failed (10 unreachable)
Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime
 File: "/Users/ytakashl/.rustup/toolchains/nightly-2023-04-30-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/result.rs", line 1651, in std::result::unwrap_failed

VERIFICATION:- FAILED
Verification Time: 1.0923209s

with Kani version: 0.30.0

I expected to see this happen: verification success.

Instead, this happened: verification fails

@YoshikiTakashima YoshikiTakashima added the [C] Bug This is a bug. Something isn't working. label Jun 21, 2023
@YoshikiTakashima YoshikiTakashima self-assigned this Jun 21, 2023
@YoshikiTakashima
Copy link
Contributor Author

blocking 1 harness in PROST.

@zhassan-aws
Copy link
Contributor

Can you include the failure in the description?

@YoshikiTakashima
Copy link
Contributor Author

@zhassan-aws, done, but I will take this.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working.
Projects
No open projects
Status: In Progress
Development

Successfully merging a pull request may close this issue.

3 participants