-
Notifications
You must be signed in to change notification settings - Fork 89
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Bump Kani version to 0.54.0 #3430
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -4,6 +4,46 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.) | |
|
||
This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards. | ||
|
||
## [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 https://github.com/model-checking/kani/pull/3332 | ||
* Fix visibility of some Kani intrinsics by @artemagvanian in https://github.com/model-checking/kani/pull/3323 | ||
* Function Contracts: Modify Slices by @pi314mm in https://github.com/model-checking/kani/pull/3295 | ||
* Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in https://github.com/model-checking/kani/pull/3344 | ||
* Add support for global transformations by @artemagvanian in https://github.com/model-checking/kani/pull/3348 | ||
* Enable an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros by @adpaco-aws in https://github.com/model-checking/kani/pull/3283 | ||
* Fix contract handling of promoted constants and constant static by @celinval in https://github.com/model-checking/kani/pull/3305 | ||
* Bump CBMC Viewer to 3.9 by @tautschnig in https://github.com/model-checking/kani/pull/3373 | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Move to the end of the list |
||
* Update to CBMC version 6.1.1 by @tautschnig in https://github.com/model-checking/kani/pull/2995 | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Move to the end of the list. |
||
* Define a struct-level `#[safety_constraint(...)]` attribute by @adpaco-aws in https://github.com/model-checking/kani/pull/3270 | ||
* Enable concrete playback for contract and stubs by @celinval in https://github.com/model-checking/kani/pull/3389 | ||
* Add code scanner tool by @celinval in https://github.com/model-checking/kani/pull/3120 | ||
* Enable contracts in associated functions by @celinval in https://github.com/model-checking/kani/pull/3363 | ||
* Enable log2*, log10* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3001 | ||
* Enable powif* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/2999 | ||
* Enable fma* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3002 | ||
* Enable sqrt* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3000 | ||
* Remove assigns clause for ZST pointers by @carolynzech in https://github.com/model-checking/kani/pull/3417 | ||
* Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in https://github.com/model-checking/kani/pull/3374 | ||
* Unify kani library and kani core logic by @jaisnan in https://github.com/model-checking/kani/pull/3333 | ||
* Stabilize pointer-to-reference cast validity checks by @artemagvanian in https://github.com/model-checking/kani/pull/3426 | ||
* Rust toolchain upgraded to `nightly-2024-08-07` by @jaisnan @qinheping @tautschnig @feliperodri | ||
|
||
## New Contributors | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We don't add new contributors. |
||
* @carolynzech made their first contribution in https://github.com/model-checking/kani/pull/3387 | ||
|
||
**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.53.0...kani-0.54.0 | ||
|
||
## [0.53.0] | ||
|
||
### Major Changes | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This doesn't have a user impact, so should be removed.