Address comments

CHANGELOG.md

@@ -8,11 +8,14 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from
 
 ### Major Changes
 * The `--visualize` option is being deprecated and will be removed in a future release. Consider using the `--concrete-playback` option instead.
-* The `-Z ptr-to-ref-cast-checks` option is being introduced to check pointer validity when casting raw pointers to references. The feature is currently behind an unstable flag but is expected to be stabilized in the next release once remaining performance issues have been resolved.
+* The `-Z ptr-to-ref-cast-checks` option is being introduced to check pointer validity when casting raw pointers to references. The feature is currently behind an unstable flag but is expected to be stabilized in a future release once remaining performance issues have been resolved.
+* The `-Z uninit-checks` option is being introduced to check memory initialization. The feature is currently behind an unstable flag and also requires the `-Z ghost-state` option.
+
+### Breaking Changes
+* Remove support for the unstable argument `--function` by @celinval in https://github.com/model-checking/kani/pull/3278
 
 ### What's Changed
 
-* Add `kani_core` library placeholder and build logic by @celinval in https://github.com/model-checking/kani/pull/3227
 * Change ensures into closures by @pi314mm in https://github.com/model-checking/kani/pull/3207
 * (Re)introduce `Invariant` trait by @adpaco-aws in https://github.com/model-checking/kani/pull/3190
 * Remove empty box creation from contracts impl by @celinval in https://github.com/model-checking/kani/pull/3233
@@ -23,18 +26,14 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from
 * Refactor stubbing so Kani compiler only invoke rustc once per crate by @celinval in https://github.com/model-checking/kani/pull/3245
 * Use cfg=kani_host for host crates by @tautschnig in https://github.com/model-checking/kani/pull/3244
 * Add intrinsics and Arbitrary support for no_core by @jaisnan in https://github.com/model-checking/kani/pull/3230
-* Fix a few issues with std verification by @celinval in https://github.com/model-checking/kani/pull/3255
+* Contracts: Avoid attribute duplication and `const` function generation for constant function by @celinval in https://github.com/model-checking/kani/pull/3255
 * Fix contract of constant fn with effect feature by @celinval in https://github.com/model-checking/kani/pull/3259
-* Fix a few more issues with the std library by @celinval in https://github.com/model-checking/kani/pull/3261
 * Fix typed_swap for ZSTs by @tautschnig in https://github.com/model-checking/kani/pull/3256
-* Remove further uses of Location::none by @tautschnig in https://github.com/model-checking/kani/pull/3253
 * Add a `#[derive(Invariant)]` macro by @adpaco-aws in https://github.com/model-checking/kani/pull/3250
 * Contracts: History Expressions via "old" monad by @pi314mm in https://github.com/model-checking/kani/pull/3232
 * Function Contracts: remove instances of _renamed by @pi314mm in https://github.com/model-checking/kani/pull/3274
-* Remove support for the unstable argument `--function` by @celinval in https://github.com/model-checking/kani/pull/3278
 * Deprecate `--visualize` in favor of concrete playback by @celinval in https://github.com/model-checking/kani/pull/3281
 * Fix operand in fat pointer comparison by @pi314mm in https://github.com/model-checking/kani/pull/3297
-* C library: declare malloc by @tautschnig in https://github.com/model-checking/kani/pull/3296
 * Function Contracts: Closure Type Inference by @pi314mm in https://github.com/model-checking/kani/pull/3307
 * Add support for f16 and f128 for toolchain upgrade to 6/28 by @jaisnan in https://github.com/model-checking/kani/pull/3306
 * Towards Proving Memory Initialization by @artemagvanian in https://github.com/model-checking/kani/pull/3264