Skip to content

Conversation

tautschnig
Copy link
Member

@tautschnig tautschnig commented Feb 7, 2024

Implemented in CBMC in diffblue/cbmc#8195.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Requires support in CBMC.
@tautschnig tautschnig self-assigned this Feb 7, 2024
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Feb 7, 2024
@tautschnig tautschnig marked this pull request as ready for review August 1, 2024 11:47
@tautschnig tautschnig requested a review from a team as a code owner August 1, 2024 11:47
@tautschnig tautschnig removed their assignment Aug 1, 2024
@tautschnig tautschnig added this pull request to the merge queue Aug 2, 2024
@tautschnig tautschnig removed this pull request from the merge queue due to the queue being cleared Aug 2, 2024
@tautschnig tautschnig enabled auto-merge (squash) August 2, 2024 18:00
@tautschnig tautschnig merged commit beccc4c into model-checking:main Aug 2, 2024
26 of 27 checks passed
@tautschnig tautschnig deleted the fma-intrinsics branch August 2, 2024 18:46
github-merge-queue bot pushed a commit that referenced this pull request Aug 9, 2024
## 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

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-EndToEndBenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants