diff --git a/tests/script-based-pre/zero-size/config.yml b/tests/script-based-pre/zero-size/config.yml new file mode 100644 index 000000000000..6dd660716457 --- /dev/null +++ b/tests/script-based-pre/zero-size/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: playback_opts.sh +expected: playback_opts.expected diff --git a/tests/script-based-pre/zero-size/original.rs b/tests/script-based-pre/zero-size/original.rs new file mode 100644 index 000000000000..1a953f96d570 --- /dev/null +++ b/tests/script-based-pre/zero-size/original.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This checks that Kani zero-size playback, 2 of them in a row. + +#[kani::proof] +fn any_is_ok() { + let unit: () = kani::any(); + let unit2: () = kani::any(); + kani::cover!(unit == ()); + kani::cover!(unit2 == ()); +} diff --git a/tests/script-based-pre/zero-size/playback_opts.expected b/tests/script-based-pre/zero-size/playback_opts.expected new file mode 100644 index 000000000000..d809e2fda5e1 --- /dev/null +++ b/tests/script-based-pre/zero-size/playback_opts.expected @@ -0,0 +1,5 @@ +[TEST] Generate test... +Checking harness any_is_ok + +[TEST] Run test... +test result: ok. 1 passed; 0 failed; diff --git a/tests/script-based-pre/zero-size/playback_opts.sh b/tests/script-based-pre/zero-size/playback_opts.sh new file mode 100755 index 000000000000..7c8a23ab9643 --- /dev/null +++ b/tests/script-based-pre/zero-size/playback_opts.sh @@ -0,0 +1,18 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# Test that concrete playback -Z concrete-playback executes as expected +set -o pipefail +set -o nounset + +RS_FILE="modified.rs" +cp original.rs ${RS_FILE} + +echo "[TEST] Generate test..." +kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace + +echo "[TEST] Run test..." +kani playback -Z concrete-playback ${RS_FILE} -- kani_concrete_playback + +# Cleanup +rm ${RS_FILE}