Add a expected test using the new method in a contract

tests/expected/function-contract/valid_ptr.expected

@@ -0,0 +1,11 @@
+Checking harness pre_condition::harness_invalid_ptr...
+Failed Checks: Dangling pointer is only valid for zero-sized access
+
+Checking harness pre_condition::harness_stack_ptr...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness pre_condition::harness_head_ptr...
+VERIFICATION:- SUCCESSFUL
+
+Verification failed for - pre_condition::harness_invalid_ptr
+Complete - 2 successfully verified harnesses, 1 failures, 3 total

tests/expected/function-contract/valid_ptr.rs

@@ -0,0 +1,61 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts -Zmem-predicates
+
+//! Test that it is sound to use `assert_valid_ptr` inside a contract pre-condition.
+//! We cannot validate post-condition yet. This can be done once we fix:
+//! <https://github.com/model-checking/kani/issues/2997>
+#![feature(pointer_is_aligned)]
+
+mod pre_condition {
+ /// This contract should succeed only if the input is a valid pointer.
+ #[kani::requires(kani::mem::assert_valid_ptr(ptr) && ptr.is_aligned())]
+ unsafe fn read_ptr(ptr: *const i32) -> i32 {
+ *ptr
+ }
+
+ #[kani::proof_for_contract(read_ptr)]
+ fn harness_head_ptr() {
+ let boxed = Box::new(10);
+ let raw_ptr = Box::into_raw(boxed);
+ assert_eq!(unsafe { read_ptr(raw_ptr) }, 10);
+ let _ = unsafe { Box::from_raw(raw_ptr) };
+ }
+
+ #[kani::proof_for_contract(read_ptr)]
+ fn harness_stack_ptr() {
+ let val = -20;
+ assert_eq!(unsafe { read_ptr(&val) }, -20);
+ }
+
+ #[kani::proof_for_contract(read_ptr)]
+ fn harness_invalid_ptr() {
+ let ptr = std::ptr::NonNull::<i32>::dangling().as_ptr();
+ assert_eq!(unsafe { read_ptr(ptr) }, -20);
+ }
+}
+
+/// TODO: Enable once we fix: <https://github.com/model-checking/kani/issues/2997>
+#[cfg(not_supported)]
+mod post_condition {
+
+ /// This contract should fail since we are creating a dangling pointer.
+ #[kani::ensures(kani::mem::assert_valid_ptr(result.0))]
+ unsafe fn new_invalid_ptr() -> PtrWrapper<char> {
+ let var = 'c';
+ PtrWrapper(&var as *const _)
+ }
+
+ #[kani::proof_for_contract(new_invalid_ptr)]
+ fn harness() {
+ let _ = unsafe { new_invalid_ptr() };
+ }
+
+ struct PtrWrapper<T>(*const T);
+
+ impl<T> kani::Arbitrary for PtrWrapper<T> {
+ fn any() -> Self {
+ unreachable!("Do not invoke stubbing")
+ }
+ }
+}