From 4d23445403ae0dee8550438d35c1eb78ab371738 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 20 Aug 2024 12:04:10 +0000
Subject: [PATCH] Doing proof of contract

---
 library/core/src/ptr/unique.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/core/src/ptr/unique.rs b/library/core/src/ptr/unique.rs
index 19627ce050354..11e16dbbc149c 100644
--- 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;