Partially integrate uninit memory checks into verify_std (#3470)

This PR partially integrates uninitialized memory checks into the
`verify_std` pipeline, which makes it possible to enable them for the
Rust Standard Library verification.

Changes:
- Move `mem_init.rs` library code into `kani_core`.
- Add a conditional compilation flag to disable uninitialized memory
checks whenever some functionality is not yet supported.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

library/kani/src/lib.rs

@@ -32,7 +32,6 @@ pub mod shadow;
 pub mod slice;
 pub mod vec;
 
-mod mem_init;
 mod models;
 
 #[cfg(feature = "concrete_playback")]

library/kani_core/src/lib.rs

@@ -22,6 +22,7 @@
 
 mod arbitrary;
 mod mem;
+mod mem_init;
 
 pub use kani_macros::*;
 
@@ -45,6 +46,10 @@ macro_rules! kani_lib {
             pub mod mem {
                 kani_core::kani_mem!(core);
             }
+
+            mod mem_init {
+                kani_core::kani_mem_init!(core);
+            }
         }
     };
 
@@ -56,6 +61,10 @@ macro_rules! kani_lib {
         pub mod mem {
             kani_core::kani_mem!(std);
         }
+
+        mod mem_init {
+            kani_core::kani_mem_init!(std);
+        }
     };
 }