kani-0.54.0
github-actions
released this
13 Aug 19:57
·
247 commits
to main
since this release
Major Changes
- We added support for slices in the
#[kani::modifies(...)]
clauses when using function contracts. - We introduce an
#[safety_constraint(...)]
attribute helper for theArbitrary
andInvariant
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 theArbitrary
andInvariant
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