Fix issues with std-checks

model-checking · Jul 2, 2024 · 068b9af · 068b9af
1 parent 8af4c07
commit 068b9af
Show file tree

Hide file tree

Showing 4 changed files with 27 additions and 3 deletions.
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
@@ -30,7 +30,7 @@ pub use ty_layout::{PointeeInfo, PointeeLayout};
 use uninit_visitor::{CheckUninitVisitor, InitRelevantInstruction, MemoryInitOp};
 
 const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] =
-    &["KaniIsUnitPtrInitialized", "KaniSetUnitPtrInitialized"];
+    &["KaniIsUnitPtrInitialized", "KaniSetUnitPtrInitialized", "KaniContractsApplyClosure"];
 
 /// Instrument the code with checks for uninitialized memory.
 #[derive(Debug)]

diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs
@@ -94,6 +94,7 @@ pub fn init_contracts() {}
 /// This should only be used within contracts. The intent is to
 /// perform type inference on a closure's argument
 #[doc(hidden)]
+#[rustc_diagnostic_item = "KaniContractsApplyClosure"]
 pub fn apply_closure<T, U: Fn(&T) -> bool>(f: U, x: &T) -> bool {
     f(x)
 }
diff --git a/tests/std-checks/core/mem.expected b/tests/std-checks/core/mem.expected
@@ -1,7 +1,30 @@
+Checking harness mem::verify::check_swap_large_adt_no_drop...
+
+Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit<mem::verify::CannotDrop<[u128; 5]>>.
+
+VERIFICATION:- FAILED
+
+Checking harness mem::verify::check_swap_adt_no_drop...
+
+Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit<mem::verify::CannotDrop<u8>>.
+
+VERIFICATION:- FAILED
+
 Checking harness mem::verify::check_swap_unit...
 
 Failed Checks: ptr NULL or writable up to size
 
+VERIFICATION:- FAILED
+
+Checking harness mem::verify::check_swap_primitive...
+
+Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit<u8>.
+
+VERIFICATION:- FAILED
+
 Summary:
+Verification failed for - mem::verify::check_swap_large_adt_no_drop
+Verification failed for - mem::verify::check_swap_adt_no_drop
 Verification failed for - mem::verify::check_swap_unit
-Complete - 6 successfully verified harnesses, 1 failures, 7 total.
+Verification failed for - mem::verify::check_swap_primitive
+Complete - 3 successfully verified harnesses, 4 failures, 7 total.
diff --git a/tests/std-checks/core/slice.expected b/tests/std-checks/core/slice.expected
@@ -1 +1 @@
-Complete - 1 successfully verified harnesses, 0 failures, 1 total.
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.