kani-0.53.0

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 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 #3278
• Remove deprecated --enable-stubbing by @celinval in #3309

What's Changed

• Change ensures into closures by @pi314mm in #3207
• (Re)introduce Invariant trait by @adpaco-aws in #3190
• Remove empty box creation from contracts impl by @celinval in #3233
• Add a new verify-std subcommand to Kani by @celinval in #3231
• Inject pointer validity check when casting raw pointers to references by @artemagvanian in #3221
• Do not turn trivially diverging loops into assume(false) by @tautschnig in #3223
• Fix "unused mut" warnings created by generated code. by @jsalzbergedu in #3247
• Refactor stubbing so Kani compiler only invoke rustc once per crate by @celinval in #3245
• Use cfg=kani_host for host crates by @tautschnig in #3244
• Add intrinsics and Arbitrary support for no_core by @jaisnan in #3230
• Contracts: Avoid attribute duplication and const function generation for constant function by @celinval in #3255
• Fix contract of constant fn with effect feature by @celinval in #3259
• Fix typed_swap for ZSTs by @tautschnig in #3256
• Add a #[derive(Invariant)] macro by @adpaco-aws in #3250
• Contracts: History Expressions via "old" monad by @pi314mm in #3232
• Function Contracts: remove instances of _renamed by @pi314mm in #3274
• Deprecate --visualize in favor of concrete playback by @celinval in #3281
• Fix operand in fat pointer comparison by @pi314mm in #3297
• Function Contracts: Closure Type Inference by @pi314mm in #3307
• Add support for f16 and f128 for toolchain upgrade to 6/28 by @jaisnan in #3306
• Towards Proving Memory Initialization by @artemagvanian in #3264
• Rust toolchain upgraded to nightly-2024-07-01 by @tautschnig @celinval @jaisnan @adpaco-aws

Full Changelog: kani-0.52.0...kani-0.53.0