NOP concrete playback to type check during verification mode. (rust-lang#2476)

Author: Yoshiki Takashima

library/kani/src/lib.rs

@@ -21,6 +21,12 @@ pub mod vec;
 pub use arbitrary::Arbitrary;
 #[cfg(feature = "concrete_playback")]
 pub use concrete_playback::concrete_playback_run;
+#[cfg(not(feature = "concrete_playback"))]
+/// NOP `concrete_playback` for type checking during verification mode.
+pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: F) {
+    unreachable!("Concrete playback does not work during verification")
+}
+
 pub use futures::block_on;
 
 /// Creates an assumption that will be valid after this statement run. Note that the assumption

tests/cargo-kani/concrete-playback-in-verification-mode/Cargo.toml

@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "playback-test"
+version = "0.1.0"
+edition = "2018"
+
+[dependencies]
+
+[workspace]

tests/cargo-kani/concrete-playback-in-verification-mode/src/main.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#[kani::proof]
+fn main() {
+    assert!(1 == 1);
+}
+
+#[test]
+/// Purpose of this is to check if Kani can comple this code in
+/// verification mode when `kani::concrete_playback_run` is in the
+/// code,
+fn _playback_type_checks() {
+    kani::concrete_playback_run(vec![], test_sum);
+}