Doing proof of contract

model-checking · Aug 20, 2024 · 4d23445 · 4d23445
1 parent f4233a2
commit 4d23445
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/library/core/src/ptr/unique.rs b/library/core/src/ptr/unique.rs
@@ -247,7 +247,7 @@ mod verify {
  }
 
  // pub const fn as_non_null_ptr(self) -> NonNull<T>
- #[kani::proof]
+ #[kani::proof_for_contract(Unique::as_non_null_ptr)]
  pub fn check_as_non_null_ptr() {
  let mut x : i32 = kani::any();
  let xptr = &mut x;