Finish polishing contracts and create expected

Author: celinval

tests/std-checks/core/Cargo.toml

@@ -8,3 +8,6 @@ description = "This crate contains contracts and harnesses for core library"
 
 [package.metadata.kani]
 unstable = { function-contracts = true, mem-predicates = true }
+
+[package.metadata.kani.flags]
+output-format = "terse"

tests/std-checks/core/expected

@@ -0,0 +1,3 @@
+Summary:
+Verification failed for - mem::verify::check_swap_unit
+Complete - 3 successfully verified harnesses, 1 failures, 4 total.

tests/std-checks/core/mem.expected

@@ -0,0 +1,3 @@
+Summary:
+Verification failed for - ptr::verify::check_replace_unit
+Complete - 5 successfully verified harnesses, 1 failures, 6 total.

tests/std-checks/core/ptr.expected

@@ -42,6 +42,10 @@ mod verify {
         contracts::swap(&mut x, &mut y)
     }
 
+    /// FIX-ME: Modifies clause fail with pointer to ZST.
+    /// <https://github.com/model-checking/kani/issues/3181>
+    /// FIX-ME: `typed_swap` intrisic fails for ZST.
+    /// <https://github.com/model-checking/kani/issues/3182>
     #[kani::proof_for_contract(contracts::swap)]
     pub fn check_swap_unit() {
         let mut x: () = kani::any();

tests/std-checks/core/src/mem.rs

@@ -72,16 +72,22 @@ mod verify {
 
     #[kani::proof_for_contract(contracts::as_ref)]
     pub fn check_as_ref() {
+        let ptr = kani::any::<Box<usize>>();
+        let non_null = NonNull::new(Box::into_raw(ptr)).unwrap();
+        let _rf = unsafe { contracts::as_ref(&non_null) };
+    }
+
+    #[kani::proof_for_contract(contracts::as_ref)]
+    #[kani::should_panic]
+    pub fn check_as_ref_dangling() {
         let ptr = kani::any::<usize>() as *mut u8;
         kani::assume(!ptr.is_null());
-        let Some(non_null) = NonNull::new(ptr) else {
-            unreachable!();
-        };
+        let non_null = NonNull::new(ptr).unwrap();
         let _rf = unsafe { contracts::as_ref(&non_null) };
     }
 
     /// FIX-ME: Modifies clause fail with pointer to ZST.
-    #[cfg(fixme)]
+    /// <https://github.com/model-checking/kani/issues/3181>
     #[kani::proof_for_contract(contracts::replace)]
     pub fn check_replace_unit() {
         check_replace_impl::<()>();