Address PR comments

kani-compiler/src/kani_middle/codegen_units.rs

@@ -104,7 +104,7 @@ impl CodegenUnits {
     /// Generate [KaniMetadata] for the target crate.
     fn generate_metadata(&self) -> KaniMetadata {
         let (proof_harnesses, test_harnesses) =
-            self.harness_info.values().cloned().partition(|md| md.attributes.is_proof());
+            self.harness_info.values().cloned().partition(|md| md.attributes.is_proof_harness());
         KaniMetadata {
             crate_name: self.crate_info.name.clone(),
             proof_harnesses,

kani-driver/src/concrete_playback/test_generator.rs

@@ -257,18 +257,20 @@ fn gen_test_doc(harness: &HarnessMetadata, property: &Property) -> String {
         property.description
     ));
     if !harness.attributes.stubs.is_empty() {
-doc_str.push_str(r#"/// 
+        doc_str.push_str(
+            r#"///
 /// # Warning
-/// 
-/// Concrete playback tests combined with stubs or contracts is highly 
+///
+/// Concrete playback tests combined with stubs or contracts is highly
 /// experimental, and subject to change.
-/// 
+///
 /// The original harness has stubs which are not applied to this test.
 /// This may cause a mismatch of non-deterministic values if the stub
 /// creates any non-deterministic value.
 /// The execution path may also differ, which can be used to refine the stub
 /// logic.
-"#);
+"#,
+        );
     }
     doc_str
 }

kani_metadata/src/harness.rs

@@ -75,7 +75,7 @@ impl HarnessAttributes {
     }
 
     /// Return whether this is a proof harness.
-    pub fn is_proof(&self) -> bool {
+    pub fn is_proof_harness(&self) -> bool {
         matches!(self.kind, HarnessKind::Proof | HarnessKind::ProofForContract { .. })
     }
 }

tests/script-based-pre/playback_expected/playback.sh

@@ -22,8 +22,8 @@ run() {
 
 ROOT_DIR=$(git rev-parse --show-toplevel)
 MODIFIED_DIR=modified
-rm -rf $MODIFIED_DIR
-mkdir $MODIFIED_DIR
+rm -rf "${MODIFIED_DIR}"
+mkdir "${MODIFIED_DIR}"
 
 for rs in src/*.rs; do
   if [[ -e "${rs}" ]]; then