Add more comments and split test

library/kani_core/src/models.rs

@@ -3,7 +3,8 @@
 //! Contains definitions that Kani compiler may use to model functions that are not suitable for
 //! verification or functions without a body, such as intrinsics.
 //!
-//! Note that these are models that Kani uses by default; thus, we keep them separate from stubs.
+//! Note that these are models that Kani uses by default, and they should not be user visible.
+//! Thus, we separate them from stubs.
 //! TODO: Move SIMD model here.
 
 #[macro_export]
@@ -18,6 +19,16 @@ macro_rules! generate_models {
             ///
             /// Where `U` is a trait, and `T` is either equal to `U` or has a tail `U`.
             ///
+            /// In cases where `T` is different than `U`,
+            /// `T` may have a sized portion, the head, while the unsized portion will be at its
+            /// tail.
+            ///
+            /// Arguments `head_size` and `head_align` represent the size and alignment of the sized
+            /// portion.
+            /// These values are known at compilation time, and they are extracted by the compiler.
+            /// If `T` doesn't have a sized portion, or if `T` is equal to `U`,
+            /// `head_size` will be set to `0`, and `head_align` will be set to 1.
+            ///
             /// This model is used to implement `checked_size_of_raw`.
             #[kanitool::fn_marker = "SizeOfDynObjectModel"]
             pub(crate) fn size_of_dyn_object<T, U: ?Sized>(
@@ -50,6 +61,16 @@ macro_rules! generate_models {
             ///
             /// Where `U` is a trait, and `T` is either equal to `U` or has a tail `U`.
             ///
+            /// In cases where `T` is different than `U`,
+            /// `T` may have a sized portion, the head, while the unsized portion will be at its
+            /// tail.
+            ///
+            /// `head_align` represents the alignment of the sized portion,
+            /// and its value is known at compilation time.
+            ///
+            /// If `T` doesn't have a sized portion, or if `T` is equal to `U`,
+            /// `head_align` will be set to 1.
+            ///
             /// This model is used to implement `checked_aligned_of_raw`.
             #[kanitool::fn_marker = "AlignOfDynObjectModel"]
             pub(crate) fn align_of_dyn_object<T, U: ?Sized>(

tests/kani/MemPredicates/foreign_type.rs

@@ -44,13 +44,26 @@ pub fn check_read_is_unsafe() {
 ///
 /// However, foreign APIs that have knowledge of the type can still safely set new values.
 #[kani::proof]
-#[kani::should_panic]
 pub fn check_write_with_extern() {
     let mut var = 0usize;
     let ptr = &mut var as *mut _ as *mut __CPROVER_size_t;
     unsafe {
         __CPROVER_havoc_object(ptr as *mut c_void);
     };
+}
+
+/// Kani APIs cannot tell if that's safe to write to a foreign type.
+///
+/// However, foreign APIs that have knowledge of the type can still safely set new values, and
+/// any side effect will be taken into consideration in the verification.
+#[kani::proof]
+#[kani::should_panic]
+pub fn check_write_with_extern_side_effect() {
+    let mut var = 0usize;
+    let ptr = &mut var as *mut _ as *mut __CPROVER_size_t;
+    unsafe {
+        __CPROVER_havoc_object(ptr as *mut c_void);
+    };
     assert!(var == 0);
 }