diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 4bf81471b760..4029893ecf34 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/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 } diff --git a/tests/script-based-pre/playback_expected/playback.sh b/tests/script-based-pre/playback_expected/playback.sh index 0a1a6997e59e..722c96239371 100755 --- a/tests/script-based-pre/playback_expected/playback.sh +++ b/tests/script-based-pre/playback_expected/playback.sh @@ -6,18 +6,18 @@ 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) @@ -25,15 +25,18 @@ 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 \ No newline at end of file +rm -rf "${MODIFIED_DIR}" \ No newline at end of file