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

Add kani harness and auto-generated bolero harnesses #227

Draft
wants to merge 2 commits into
base: main
Choose a base branch
from

Conversation

cvick32
Copy link

@cvick32 cvick32 commented Sep 5, 2024

Summary of the PR

Adds failing 5 Kani harnesses and 7 auto-generated Bolero harnesses.

Running cargo kani fails with:

SUMMARY:
 ** 1 of 334 failed (7 unreachable)
Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime
 File: "/Users/ec2-user/.rustup/toolchains/nightly-2024-05-28-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/result.rs", line 1679, in std::result::unwrap_failed

VERIFICATION:- FAILED
Verification Time: 28.542933s

Summary:
Verification failed for - fam::kani_harnesses::prove_capacity
Verification failed for - fam::kani_harnesses::prove_len
Verification failed for - fam::kani_harnesses::prove_as_fam_struct_ptr
Verification failed for - fam::kani_harnesses::prove_into_raw
Verification failed for - fam::kani_harnesses::prove_as_mut_fam_struct
Complete - 0 successfully verified harnesses, 5 failures, 5 total.

Requirements

Before submitting your PR, please make sure you addressed the following
requirements:

  • All commits in this PR have Signed-Off-By trailers (with
    git commit -s), and the commit message has max 60 characters for the
    summary and max 75 characters for each description line.
  • All added/changed functionality has a corresponding unit/integration
    test.
  • All added/changed public-facing functionality has entries in the "Upcoming
    Release" section of CHANGELOG.md (if no such section exists, please create one).
  • Any newly added unsafe code is properly documented.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant