Add some docs for is_initialized_body

kani-compiler/src/kani_middle/transform/kani_intrinsics.rs

@@ -145,6 +145,14 @@ impl IntrinsicGeneratorPass {
         new_body.into()
     }
 
+    /// Generate the body for `is_initialized`, which looks like the following
+    ///
+    /// ```
+    /// pub fn is_initialized<T>(ptr: *const T, len: usize) -> bool {
+    ///     let layout = ... // Byte mask representing the layout of T.
+    ///     __kani_mem_init_sm_get(ptr, layout, len)
+    /// }
+    /// ```
     fn is_initialized_body(&self, tcx: TyCtxt, body: Body) -> Body {
         let mut new_body = MutableBody::from(body);
         new_body.clear_body();

library/kani/src/mem.rs

@@ -290,10 +290,10 @@ unsafe fn has_valid_value<T: ?Sized>(_ptr: *const T) -> bool {
     kani_intrinsic()
 }
 
-/// Extract the layout of the pointee type.
+/// Check whether `len * size_of::<T>()` bytes are initialized starting from `ptr`.
 #[rustc_diagnostic_item = "KaniIsInitialized"]
 #[inline(never)]
-pub fn is_initialized<T: ?Sized>(_ptr: *const T, _n: usize) -> bool {
+pub fn is_initialized<T: ?Sized>(_ptr: *const T, _len: usize) -> bool {
     kani_intrinsic()
 }