Enable concrete playback for failure of UB checks

kani-driver/src/concrete_playback/test_generator.rs

@@ -325,7 +325,7 @@ mod concrete_vals_extractor {
         result_items
             .iter()
             .filter(|prop| {
-                (prop.property_class() == "assertion" && prop.status == CheckStatus::Failure)
+                (prop.property_class() != "unwind" && prop.status == CheckStatus::Failure)
                     || (prop.property_class() == "cover" && prop.status == CheckStatus::Satisfied)
             })
             .map(|property| {

tests/ui/concrete-playback/ub/null_ptr/expected

@@ -0,0 +1,13 @@
+VERIFICATION:- FAILED
+
+Concrete playback
+```
+#[test]
+fn kani_concrete_playback_null_ptr
+    let concrete_vals: Vec<Vec<u8>> = vec![
+        // 15
+        vec![15, 0, 0, 0],
+    ];
+    kani::concrete_playback_run(concrete_vals, null_ptr);
+}
+```

tests/ui/concrete-playback/ub/null_ptr/test.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Zconcrete-playback --concrete-playback=print
+
+// This test checks that Kani generates a concrete playback test for UB checks
+// (e.g. dereferencing a null pointer)
+
+#[kani::proof]
+fn null_ptr() {
+    let x = 42;
+    let nd: i32 = kani::any();
+    let ptr: *const i32 = if nd != 15 { &x as *const i32 } else { std::ptr::null() };
+    let _y = unsafe { *ptr };
+}

tests/ui/concrete-playback/ub/oob_ptr/expected

@@ -0,0 +1,13 @@
+VERIFICATION:- FAILED
+
+Concrete playback
+```
+#[test]
+fn kani_concrete_playback_oob_ptr
+    let concrete_vals: Vec<Vec<u8>> = vec![
+        // 3ul
+        vec![3, 0, 0, 0, 0, 0, 0, 0],
+    ];
+    kani::concrete_playback_run(concrete_vals, oob_ptr);
+}
+```

tests/ui/concrete-playback/ub/oob_ptr/test.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Zconcrete-playback --concrete-playback=print
+
+// This test checks that Kani generates a concrete playback test for UB checks
+// (e.g. dereferencing a pointer that is outside the object bounds)
+
+#[kani::proof]
+fn oob_ptr() {
+    let v = vec![1, 2, 3];
+    // BUG: predicate should use strict less-than, i.e. `*idx < v.len()`
+    let idx: usize = kani::any_where(|idx| *idx <= v.len());
+    let _x = unsafe { *v.get_unchecked(idx) };
+}