Do not crash when rustfmt fails.

kani-driver/src/concrete_playback/test_generator.rs

@@ -119,7 +119,8 @@ impl KaniSession {
                 file: file_name,
                 line_range: Some((unit_test_start_line, unit_test_end_line)),
             }];
-            self.run_rustfmt(&file_line_ranges, Some(&path))?;
+            self.run_rustfmt(&file_line_ranges, Some(&path))
+                .unwrap_or_else(|err| println!("WARNING: {}", err));
         }
 
         Ok(())

tests/script-based-pre/playback_no_rustfmt/bin/rustfmt

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# This is a fake `rustfmt` for testing what happens when rustfmt is not found
+# or overridden.
+
+exit 1

tests/script-based-pre/playback_no_rustfmt/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: playback_no_rustfmt.sh
+expected: playback_no_rustfmt.expected

tests/script-based-pre/playback_no_rustfmt/original.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani correctly adds tests to the cover checks reachable in a harness.
+extern crate kani;
+
+#[cfg(kani)]
+mod verify {
+    use kani::cover;
+    use std::convert::TryFrom;
+    use std::num::NonZeroU8;
+
+    #[kani::proof]
+    fn try_nz_u8() {
+        let val: u8 = kani::any();
+        let result = NonZeroU8::try_from(val);
+        match result {
+            Ok(nz_val) => {
+                cover!(true, "Ok");
+                assert_eq!(nz_val.get(), val);
+            }
+            Err(_) => {
+                cover!(true, "Not ok");
+                assert_eq!(val, 0);
+            }
+        }
+    }
+}

tests/script-based-pre/playback_no_rustfmt/playback_no_rustfmt.expected

@@ -0,0 +1,8 @@
+[TEST] Generate test...
+Checking harness verify::try_nz_u8
+
+WARNING: Failed to rustfmt modified source code
+
+[TEST] Run test...
+test result: ok. 2 passed; 0 failed;
+

tests/script-based-pre/playback_no_rustfmt/playback_no_rustfmt.sh

@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+# Test that concrete playback -Z concrete-playback executes as expected
+set -o pipefail
+set -o nounset
+
+RS_FILE="modified.rs"
+cp original.rs ${RS_FILE}
+
+# override rustfmt binary to make it crash.
+export PATH=$(pwd)/bin:$PATH
+
+echo "[TEST] Generate test..."
+kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace
+
+echo "[TEST] Run test..."
+kani playback -Z concrete-playback ${RS_FILE} -- kani_concrete_playback
+
+# Cleanup
+rm ${RS_FILE}