Add more comments, remove unnecessary checks

model-checking · Jul 3, 2024 · bb2a02b · bb2a02b
1 parent fb2aa14
commit bb2a02b
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 2 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", "KaniContractsApplyClosure"];
+    &["KaniIsUnitPtrInitialized", "KaniSetUnitPtrInitialized"];
 
 /// Instrument the code with checks for uninitialized memory.
 #[derive(Debug)]

diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs
@@ -262,8 +262,11 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                                 }
                                 name if name.starts_with("atomic") => {
                                     let num_args = match name {
+                                        // All `atomic_cxchg` intrinsics take `dst, old, src` as arguments.
                                         name if name.starts_with("atomic_cxchg") => 3,
+                                        // All `atomic_load` intrinsics take `src` as an argument.
                                         name if name.starts_with("atomic_load") => 1,
+                                        // All other `atomic` intrinsics take `dst, src` as arguments.
                                         _ => 2,
                                     };
                                     assert_eq!(
@@ -529,6 +532,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> {
                 for (_, prov) in &allocation.provenance.ptrs {
                     if let GlobalAlloc::Static(_) = GlobalAlloc::from(prov.0) {
                         if constant.ty().kind().is_raw_ptr() {
+                            // If a static is a raw pointer, need to mark it as initialized.
                             self.push_target(MemoryInitOp::Set {
                                 operand: Operand::Constant(constant.clone()),
                                 count: mk_const_operand(1, location.span()),

diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs
@@ -94,7 +94,6 @@ 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)
 }