diff --git a/tests/script-based-pre/cargo_playback_array/playback_target.sh b/tests/script-based-pre/cargo_playback_array/playback_target.sh deleted file mode 100755 index 17eaa66a01c6..000000000000 --- a/tests/script-based-pre/cargo_playback_array/playback_target.sh +++ /dev/null @@ -1,27 +0,0 @@ -#!/usr/bin/env bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -set +e - -function check_playback { - local OUTPUT=output.log - cargo kani playback "${@}" >& $OUTPUT - # Sort output so we can rely on the order. - echo "$(grep "test verify::.* ok" $OUTPUT | sort)" - echo - echo "======= Raw Output =======" - cat $OUTPUT - echo "==========================" - echo - rm $OUTPUT -} - -pushd sample_crate > /dev/null -cargo clean - -cargo kani --concrete-playback inplace -Z concrete-playback -check_playback -Z concrete-playback - -cargo clean -popd > /dev/null diff --git a/tests/script-based-pre/cargo_playback_array/sample_crate/Cargo.toml b/tests/script-based-pre/cargo_playback_array/sample_crate/Cargo.toml deleted file mode 100644 index 202362506011..000000000000 --- a/tests/script-based-pre/cargo_playback_array/sample_crate/Cargo.toml +++ /dev/null @@ -1,10 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT -[package] -name = "sample_crate" -version = "0.1.0" -edition = "2021" -doctest = false - -[lints.rust] -unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_playback_array/sample_crate/src/lib.rs b/tests/script-based-pre/playback_array/array.rs similarity index 100% rename from tests/script-based-pre/cargo_playback_array/sample_crate/src/lib.rs rename to tests/script-based-pre/playback_array/array.rs diff --git a/tests/script-based-pre/cargo_playback_array/config.yml b/tests/script-based-pre/playback_array/config.yml similarity index 54% rename from tests/script-based-pre/cargo_playback_array/config.yml rename to tests/script-based-pre/playback_array/config.yml index 99bfe39f95a5..88b420e8a6f0 100644 --- a/tests/script-based-pre/cargo_playback_array/config.yml +++ b/tests/script-based-pre/playback_array/config.yml @@ -1,4 +1,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -script: playback_target.sh -expected: playback_target.expected +script: playback_array.sh +expected: playback_array.expected diff --git a/tests/script-based-pre/cargo_playback_array/playback_target.expected b/tests/script-based-pre/playback_array/playback_array.expected similarity index 100% rename from tests/script-based-pre/cargo_playback_array/playback_target.expected rename to tests/script-based-pre/playback_array/playback_array.expected diff --git a/tests/script-based-pre/playback_array/playback_array.sh b/tests/script-based-pre/playback_array/playback_array.sh new file mode 100755 index 000000000000..3cceb8da6297 --- /dev/null +++ b/tests/script-based-pre/playback_array/playback_array.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -e +set -o pipefail +set -o nounset + +cleanup() +{ + rm ${RS_FILE} +} +trap cleanup EXIT + +RS_FILE="modified.rs" +cp array.rs ${RS_FILE} + +echo "[TEST] Generate test..." +kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace || true + +echo "[TEST] Run test..." +kani playback -Z concrete-playback ${RS_FILE} || true