Skip to content
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

Enable powif* intrinsics #2999

Merged
merged 7 commits into from
Aug 2, 2024
Merged

Conversation

tautschnig
Copy link
Member

@tautschnig tautschnig commented Feb 7, 2024

These are supported by CBMC with diffblue/cbmc#8192 merged.

Resolves: #2763

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

These are supported by CBMC with
diffblue/cbmc#8192 merged.

Resolves: model-checking#2763
@tautschnig tautschnig self-assigned this Feb 7, 2024
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Feb 7, 2024
@tautschnig tautschnig marked this pull request as ready for review August 1, 2024 15:36
@tautschnig tautschnig requested a review from a team as a code owner August 1, 2024 15:36
@tautschnig tautschnig assigned tautschnig and unassigned tautschnig Aug 1, 2024
@tautschnig tautschnig merged commit 6ae3f00 into model-checking:main Aug 2, 2024
27 checks passed
@tautschnig tautschnig deleted the powi-intrinsics branch August 2, 2024 14:54
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-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

powif64 intrinsic is not currently supported by Kani
3 participants