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

Delay printing playback harness until after verification status #2480

4 changes: 1 addition & 3 deletions kani-driver/src/call_cbmc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -66,8 +66,7 @@ impl KaniSession {

let start_time = Instant::now();

let mut verification_results = if self.args.output_format == crate::args::OutputFormat::Old
{
let verification_results = if self.args.output_format == crate::args::OutputFormat::Old {
if self.run_terminal(cmd).is_err() {
VerificationResult::mock_failure()
} else {
Expand All @@ -93,7 +92,6 @@ impl KaniSession {
VerificationResult::from(output, harness.attributes.should_panic, start_time)
};

self.gen_and_add_concrete_playback(harness, &mut verification_results)?;
Ok(verification_results)
}

Expand Down
4 changes: 2 additions & 2 deletions kani-driver/src/harness_runner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ impl KaniSession {
// Strictly speaking, we're faking success here. This is more "no error"
Ok(VerificationResult::mock_success())
} else {
let result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;

// When quiet, we don't want to print anything at all.
// When output is old, we also don't have real results to print.
Expand All @@ -99,7 +99,7 @@ impl KaniSession {
result.render(&self.args.output_format, harness.attributes.should_panic)
);
}

self.gen_and_add_concrete_playback(harness, &mut result)?;
Ok(result)
}
}
Expand Down
14 changes: 14 additions & 0 deletions tests/ui/concrete-playback/message-order/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
VERIFICATION:- SUCCESSFUL


Concrete playback unit test for `dummy`:
```
#[test]
fn kani_concrete_playback_dummy
let concrete_vals: Vec<Vec<u8>> = vec![
// 32778
vec![10, 128, 0, 0],
];
kani::concrete_playback_run(concrete_vals, dummy);
}
```
9 changes: 9 additions & 0 deletions tests/ui/concrete-playback/message-order/main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

// kani-flags: --concrete-playback=print --harness dummy -Z concrete-playback

#[kani::proof]
fn dummy() {
kani::cover!(kani::any::<u32>() != 10);
}