Apply suggestions from code review

Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>

kani-driver/src/concrete_playback/test_generator.rs

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

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

@@ -6,34 +6,37 @@
 set -o nounset
 
 run() {
- input_rs=${1:?"Missing input file"}
+ local input_rs=${1:?"Missing input file"}
 
- echo "[TEST] Generate test for $input_rs..."
- kani ${input_rs} \
+ echo "[TEST] Generate test for ${input_rs}..."
+ kani "${input_rs}" \
  -Z concrete-playback --concrete-playback=inplace \
  -Z function-contracts -Z stubbing --output-format terse
 
  # Note that today one of the tests will succeed since the contract pre-conditions are not inserted by Kani.
  # Hopefully this will change with https://github.com/model-checking/kani/issues/3326
- echo "[TEST] Run test for $input_rs..."
- summary=$(kani playback -Z concrete-playback ${input_rs} -- kani_concrete_playback | grep "test result")
- echo "Result for $input_rs: $summary"
+ echo "[TEST] Run test for ${input_rs}..."
+ summary=$(kani playback -Z concrete-playback "${input_rs}" -- kani_concrete_playback | grep "test result")
+ echo "Result for ${input_rs}: ${summary}"
 }
 
 ROOT_DIR=$(git rev-parse --show-toplevel)
 MODIFIED_DIR=modified
 rm -rf $MODIFIED_DIR
 mkdir $MODIFIED_DIR
 
-for rs in src/*.rs
-do
- [[ -e "${rs}" ]] || exit 1
- echo "Running ${rs}"
- cp "$rs" $MODIFIED_DIR
- pushd $MODIFIED_DIR
- run $(basename $rs)
- popd
+for rs in src/*.rs; do
+ if [[ -e "${rs}" ]]; then
+ echo "Running ${rs}"
+ cp "${rs}" "${MODIFIED_DIR}"
+ pushd "${MODIFIED_DIR}" > /dev/null
+ run "$(basename "${rs}")"
+ popd > /dev/null
+ else
+ echo "No .rs files found in src directory"
+ exit 1
+ fi
 done
 
  # Cleanup
-rm -rf $MODIFIED_DIR
+rm -rf "${MODIFIED_DIR}"