Delay printing playback harness until after verification status

kani-driver/src/call_cbmc.rs

@@ -53,6 +53,8 @@ pub struct VerificationResult {
     pub runtime: Duration,
     /// Whether concrete playback generated a test
     pub generated_concrete_test: bool,
+    /// the test case to print for concrete playback.
+    pub maybe_concrete_test_to_print: Option<String>,
 }
 
 impl KaniSession {
@@ -266,6 +268,7 @@ impl VerificationResult {
                 results: Ok(results),
                 runtime,
                 generated_concrete_test: false,
+                maybe_concrete_test_to_print: None,
             }
         } else {
             // We never got results from CBMC - something went wrong (e.g. crash) so it's failure
@@ -276,6 +279,7 @@ impl VerificationResult {
                 results: Err(output.process_status),
                 runtime,
                 generated_concrete_test: false,
+                maybe_concrete_test_to_print: None,
             }
         }
     }
@@ -288,6 +292,7 @@ impl VerificationResult {
             results: Ok(vec![]),
             runtime: Duration::from_secs(0),
             generated_concrete_test: false,
+            maybe_concrete_test_to_print: None,
         }
     }
 
@@ -302,6 +307,7 @@ impl VerificationResult {
             results: Err(42),
             runtime: Duration::from_secs(0),
             generated_concrete_test: false,
+            maybe_concrete_test_to_print: None,
         }
     }
 

kani-driver/src/concrete_playback/test_generator.rs

@@ -43,15 +43,18 @@ impl KaniSession {
                     let generated_unit_test = format_unit_test(&pretty_name, &concrete_vals);
                     match playback_mode {
                         ConcretePlaybackMode::Print => {
-                            println!(
-                                "Concrete playback unit test for `{}`:\n```\n{}\n```",
-                                &harness.pretty_name,
-                                &generated_unit_test.code.join("\n")
-                            );
-                            println!(
-                                "INFO: To automatically add the concrete playback unit test `{}` to the \
-                        src code, run Kani with `--concrete-playback=inplace`.",
-                                &generated_unit_test.name
+                            verification_result.maybe_concrete_test_to_print = Some(
+                                format!(
+                                    "Concrete playback unit test for `{}`:
+```rust
+{}
+```
+INFO: To automatically add the concrete playback unit test `{}` to the src code, \
+run Kani with `--concrete-playback=inplace`.",
+                                    &harness.pretty_name,
+                                    &generated_unit_test.code.join("\n"),
+                                    &generated_unit_test.name,
+                                )
                             );
                         }
                         ConcretePlaybackMode::InPlace => {

kani-driver/src/harness_runner.rs

@@ -95,8 +95,11 @@ impl KaniSession {
             // When output is old, we also don't have real results to print.
             if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old {
                 println!(
-                    "{}",
-                    result.render(&self.args.output_format, harness.attributes.should_panic)
+                    "{}{}",
+                    result.render(&self.args.output_format, harness.attributes.should_panic),
+                    result.maybe_concrete_test_to_print.as_ref()
+                        .map(|message| format!("\n\n{}", message))
+                        .unwrap_or("".to_string())
                 );
             }
 

tests/ui/concrete-playback/message-order/expected

@@ -0,0 +1,14 @@
+VERIFICATION:- SUCCESSFUL
+
+
+Concrete playback unit test for `dummy`:
+```rust
+#[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);
+}
+```

tests/ui/concrete-playback/message-order/main.rs

@@ -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);
+}