kani-0.54.0

Major Changes

• We added support for slices in the #[kani::modifies(...)] clauses when using function contracts.
• We introduce an #[safety_constraint(...)] attribute helper for the Arbitrary and Invariant macros.
• We enabled support for concrete playback for harness that contains stubs or function contracts.
• We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs.

Breaking Changes

• The -Z ptr-to-ref-cast-checks option has been removed, and pointer validity checks when casting raw pointers to references are now run by default.

What's Changed

• Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in #3332
• Fix visibility of some Kani intrinsics by @artemagvanian in #3323
• Function Contracts: Modify Slices by @pi314mm in #3295
• Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in #3344
• Add support for global transformations by @artemagvanian in #3348
• Enable an #[safety_constraint(...)] attribute helper for the Arbitrary and Invariant macros by @adpaco-aws in #3283
• Fix contract handling of promoted constants and constant static by @celinval in #3305
• Bump CBMC Viewer to 3.9 by @tautschnig in #3373
• Update to CBMC version 6.1.1 by @tautschnig in #2995
• Define a struct-level #[safety_constraint(...)] attribute by @adpaco-aws in #3270
• Enable concrete playback for contract and stubs by @celinval in #3389
• Add code scanner tool by @celinval in #3120
• Enable contracts in associated functions by @celinval in #3363
• Enable log2*, log10* intrinsics by @tautschnig in #3001
• Enable powif* intrinsics by @tautschnig in #2999
• Enable fma* intrinsics by @tautschnig in #3002
• Enable sqrt* intrinsics by @tautschnig in #3000
• Remove assigns clause for ZST pointers by @carolynzech in #3417
• Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in #3374
• Unify kani library and kani core logic by @jaisnan in #3333
• Stabilize pointer-to-reference cast validity checks by @artemagvanian in #3426
• Rust toolchain upgraded to nightly-2024-08-07 by @jaisnan @qinheping @tautschnig @feliperodri

New Contributors

• @carolynzech made their first contribution in #3387

Full Changelog: kani-0.53.0...kani-0.54.0