Fix: regression test from #3888 has version control change (#3892)

Resolves #3891 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Michael Tautschnig <[email protected]>
model-checking · Feb 19, 2025 · 006e5da · 006e5da
1 parent ac8e0b9
commit 006e5da
Show file tree

Hide file tree

Showing 6 changed files with 24 additions and 39 deletions.
diff --git a/tests/script-based-pre/cargo_playback_array/playback_target.sh b/tests/script-based-pre/cargo_playback_array/playback_target.sh
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
diff --git a/...go_playback_array/sample_crate/src/lib.rs → .../script-based-pre/playback_array/array.rs b/...go_playback_array/sample_crate/src/lib.rs → .../script-based-pre/playback_array/array.rs
diff --git a/...based-pre/cargo_playback_array/config.yml → ...cript-based-pre/playback_array/config.yml b/...based-pre/cargo_playback_array/config.yml → ...cript-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/...o_playback_array/playback_target.expected → ...re/playback_array/playback_array.expected b/...o_playback_array/playback_target.expected → ...re/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
@@ -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