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

Improve --jobs UI #3790

Merged
merged 3 commits into from
Dec 19, 2024
Merged

Improve --jobs UI #3790

merged 3 commits into from
Dec 19, 2024

Conversation

carolynzech
Copy link
Contributor

Improve the documentation for the --jobs option, change it to use hide_short_help like other unstable options, and print the current thread number so that users can match the harness to its output.

Example:

#[kani::modifies(x)]
#[kani::ensures(|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b))]
fn zero(x: &mut [u8]) {
    x.fill(0)
}

#[kani::proof_for_contract(zero)]
fn harness() {
    let mut x = [kani::any(), kani::any(), kani::any()];
    zero(&mut x);
}

#[kani::proof]
fn harness_2() {
    assert!(true);
}

#[kani::proof]
fn harness_3() {
    assert!(false);
}
cargo kani -j --enable-unstable --output-format=terse -Z function-contracts
Kani Rust Verifier 0.57.0 (cargo plugin)
warning: Found the following unsupported constructs:
             - caller_location (1)
             - foreign function (1)
         
         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.02s
Thread 4: Checking harness harness_2...
Thread 2: Checking harness harness_3...
Thread 4: 
VERIFICATION RESULT:
 ** 0 of 1 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.0137195s

Thread 2: 
VERIFICATION RESULT:
 ** 1 of 1 failed
Failed Checks: assertion failed: false
 File: "src/lib.rs", line 26, in harness_3

VERIFICATION:- FAILED
Verification Time: 0.012914542s

Thread 0: Checking harness harness...
Thread 0: 
VERIFICATION RESULT:
 ** 0 of 217 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 18.47224s

Summary:
Verification failed for - harness_3
Complete - 2 successfully verified harnesses, 1 failures, 3 total.

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

Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

kani-driver/src/harness_runner.rs Outdated Show resolved Hide resolved
kani-driver/src/harness_runner.rs Outdated Show resolved Hide resolved
@carolynzech carolynzech added this pull request to the merge queue Dec 18, 2024
Merged via the queue into model-checking:main with commit b7ae080 Dec 19, 2024
28 checks passed
@carolynzech carolynzech deleted the threading-ui branch December 19, 2024 00:22
github-merge-queue bot pushed a commit that referenced this pull request Jan 11, 2025
## What's Changed
* Package Docker release step: ensure compiler is installed by
@tautschnig in #3789
* Improve `--jobs` UI by @carolynzech in
#3790
* Update kissat to v4.0.1 by @remi-delmas-3000 in
#3791
* Automatic cargo update to 2024-12-23 by @github-actions in
#3792
* Bump tests/perf/s2n-quic from `0b3f892` to `a54686e` by @dependabot in
#3793
* Upgrade toolchain to nightly-2024-12-18 by @zhassan-aws in
#3794
* Automatic cargo update to 2024-12-30 by @github-actions in
#3800
* fix: clippy by @ShoyuVanilla in
#3806
* Update dependencies (02.01.2025). by @remi-delmas-3000 in
#3809
* Update charon submodule by @zhassan-aws in
#3801
* Upgrade toolchain to 2024-12-19 by @zhassan-aws in
#3810
* Automatic cargo update to 2025-01-06 by @github-actions in
#3812
* Bump tests/perf/s2n-quic from `a54686e` to `ac52a48` by @dependabot in
#3813
* Generate contracts of dependencies as assertions by @carolynzech in
#3802
* Fix hanging command in `std-analysis.sh` by @carolynzech in
#3818
* Add UB checks for ptr_offset_from* intrinsics by @celinval in
#3757
* Toolchain update 06-01-2025 by @remi-delmas-3000 in
#3814
* Automatic toolchain upgrade to nightly-2025-01-07 by @github-actions
in #3820
* Include manifest-path when checking if packages are in the workspace
by @qinheping in #3819

## New Contributors
* @ShoyuVanilla made their first contribution in
#3806

**Full Changelog**:
kani-0.57.0...kani-0.58.0

---------

Co-authored-by: Celina G. Val <[email protected]>
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.

2 participants