Skip to content

Add support for edition 2018 crates using assert! (Fixes #3717) #4096

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 5 commits into from
May 28, 2025
Merged

Add support for edition 2018 crates using assert! (Fixes #3717) #4096

merged 5 commits into from
May 28, 2025

Conversation

sintemal
Copy link
Contributor

We export core::assert as __kani__workaround_core_assert! to every crate which uses assert. Because kani uses edition 2021, crates which are built edition 2018 now use the 2021 assert.

The behaviour of assert changed between both editions (see https://doc.rust-lang.org/nightly/edition-guide/rust-2021/panic-macro-consistency.html).

This commit adds an extra clause to handle the case, if the first message parameter isn't of string type and adds a format string accordingly

This resolves #3717 .

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

@sintemal
Before edition 2021, the assert! macro could take a single argument
96e636d 
that wasn't a literal. This is not supported in edition 2021 and above.
Because we reexport the 2021 edition macro, we need to support this
case. This commits adds a special case, if there is only one argument
to the assert macro
@sintemal sintemal requested a review from a team as a code owner May 21, 2025 21:28
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label May 21, 2025
sintemal and others added 2 commits May 22, 2025 14:25
@zhassan-aws
Copy link
Contributor

Thanks for creating this PR, @sintemal! I've push a tweak that should make the regressions pass.

@sintemal
Copy link
Contributor Author

Thank you very much!

@zhassan-aws zhassan-aws added this pull request to the merge queue May 28, 2025
Merged via the queue into model-checking:main with commit ff15fed May 28, 2025
26 checks passed
zhassan-aws added a commit that referenced this pull request May 28, 2025
@zhassan-aws
Add support for edition 2018 crates using assert! (Fixes #3717) (#4096)
8b306bb 
We export `core::assert` as `__kani__workaround_core_assert!` to every
crate which uses `assert`. Because kani uses edition 2021, crates which
are built edition 2018 now use the 2021 `assert`.

The behaviour of `assert` changed between both editions (see
https://doc.rust-lang.org/nightly/edition-guide/rust-2021/panic-macro-consistency.html).

This commit adds an extra clause to handle the case, if the first
message parameter isn't of string type and adds a format string
accordingly

This resolves #3717 .

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

---------

Co-authored-by: Zyad Hassan <zyadh@amazon.com>
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
github-merge-queue bot pushed a commit that referenced this pull request Jun 9, 2025
@zhassan-aws @carolynzech
Bump Kani Version (#4147)
37fb634 
These are the automatically-generated release notes:
```
## What's Changed
* Toolchain upgrade to nightly-2025-05-04 by @thanhnguyen-aws in #4059
* Automatic toolchain upgrade to nightly-2025-05-05 by @github-actions in #4060
* Automatic toolchain upgrade to nightly-2025-05-06 by @github-actions in #4061
* Enable target features: x87 and sse2 by @thanhnguyen-aws in #4062
* Fix the bug: Loop contracts are not composable with function contracts  by @thanhnguyen-aws in #3979
* Automatic cargo update to 2025-05-12 by @github-actions in #4066
* Bump tests/perf/s2n-quic from `6aa9975` to `5f323b7` by @dependabot in #4068
* Fix stabilization instructions in RFC intro by @carolynzech in #4067
* Add support for quantifiers by @qinheping in #3993
* Toolchain upgrade to nightly-2025-05-07 by @thanhnguyen-aws in #4070
* Automatic toolchain upgrade to nightly-2025-05-08 by @github-actions in #4071
* Automatic toolchain upgrade to nightly-2025-05-09 by @github-actions in #4072
* Automatic toolchain upgrade to nightly-2025-05-10 by @github-actions in #4073
* Clippy/Stylistic Fixes by @carolynzech in #4074
* Upgrade toolchain to 2025-05-14 by @zhassan-aws in #4076
* Autoharness argument validation: only error on `--quiet` if `--list` was passed by @carolynzech in #4069
* Upgrade Rust toolchain to 2025-05-16 by @zhassan-aws in #4080
* Automatic toolchain upgrade to nightly-2025-05-17 by @github-actions in #4081
* Add setup scripts for Ubuntu 20.04 by @zhassan-aws in #4082
* Automatic toolchain upgrade to nightly-2025-05-18 by @github-actions in #4083
* Automatic cargo update to 2025-05-19 by @github-actions in #4086
* Automatic toolchain upgrade to nightly-2025-05-19 by @github-actions in #4085
* Automatic toolchain upgrade to nightly-2025-05-20 by @github-actions in #4091
* Bump tests/perf/s2n-quic from `5f323b7` to `22434aa` by @dependabot in #4089
* Fix the error that Kani panics when there is no external parameter in quantifier's closure. by @thanhnguyen-aws in #4088
* Update toolchain to 2025-05-22 by @carolynzech in #4098
* Use our toolchain when invoking `cargo metadata` by @carolynzech in #4090
* Automatic toolchain upgrade to nightly-2025-05-23 by @github-actions in #4099
* Automatic toolchain upgrade to nightly-2025-05-24 by @github-actions in #4101
* Automatic toolchain upgrade to nightly-2025-05-25 by @github-actions in #4102
* Fix a bug codegening `SwitchInt`s with only an otherwise branch by @bkirwi in #4095
* Automatic toolchain upgrade to nightly-2025-05-26 by @github-actions in #4104
* Automatic cargo update to 2025-05-26 by @github-actions in #4105
* Bump tests/perf/s2n-quic from `22434aa` to `550afb3` by @dependabot in #4106
* Automatic toolchain upgrade to nightly-2025-05-27 by @github-actions in #4107
* Update `kani::mem` pointer validity documentation by @carolynzech in #4092
* Add support for edition 2018 crates using assert! (Fixes #3717) by @sintemal in #4096
* Automatic toolchain upgrade to nightly-2025-05-28 by @github-actions in #4113
* Automatic toolchain upgrade to nightly-2025-05-29 by @github-actions in #4115
* Automatic toolchain upgrade to nightly-2025-05-30 by @github-actions in #4118
* Handle generic defaults in BoundedArbitrary derives by @zhassan-aws in #4117
* Automatic cargo update to 2025-06-02 by @github-actions in #4121
* Bump tests/perf/s2n-quic from `550afb3` to `8f54b57` by @dependabot in #4122
* Upgrade Rust toolchain to 2025-06-02 by @zhassan-aws in #4123
* Automatic toolchain upgrade to nightly-2025-06-03 by @github-actions in #4125
* Finish deprecating `--enable-unstable`, `--restrict-vtable`, and `--write-json-symtab` by @carolynzech in #4110
* `ty_mangled_name`: only use non-mangled name if `-Zcffi` is enabled. by @carolynzech in #4114
* Improve Help Menu by @carolynzech in #4109
* Start stabilizing `--jobs` and `list`; deprecate default memory checks by @carolynzech in #4108
* Refactor simd_bitmask to reduce the number of iterations by @zhassan-aws in #4129
* Set target features depending on the target architecture by @zhassan-aws in #4127
* Bump some versions suggested by cargo-outdated by @zhassan-aws in #4131
* Improve linking error output for `#[no_std]` crates by @AlexanderPortland in #4126
* Fix the git log command in the toolchain update script by @zhassan-aws in #4139
* Gate quantifiers behind an experimental feature by @thanhnguyen-aws in #4141
* Automatic cargo update to 2025-06-09 by @github-actions in #4145

## New Contributors
* @bkirwi made their first contribution in #4095
* @sintemal made their first contribution in #4096
* @AlexanderPortland made their first contribution in #4126

**Full Changelog**: kani-0.62.0...kani-0.63.0
```


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

---------

Co-authored-by: Carolyn Zech <carolynzech@gmail.com>
zhassan-aws added a commit that referenced this pull request Jul 23, 2025
@sintemal @zhassan-aws
Add support for edition 2018 crates using assert! (Fixes #3717) (#4096)
d8814a6 
We export `core::assert` as `__kani__workaround_core_assert!` to every
crate which uses `assert`. Because kani uses edition 2021, crates which
are built edition 2018 now use the 2021 `assert`.

The behaviour of `assert` changed between both editions (see
https://doc.rust-lang.org/nightly/edition-guide/rust-2021/panic-macro-consistency.html).

This commit adds an extra clause to handle the case, if the first
message parameter isn't of string type and adds a format string
accordingly

This resolves #3717 . 

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

---------

Co-authored-by: Zyad Hassan <zyadh@amazon.com>
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@zhassan-aws zhassan-aws zhassan-aws approved these changes

Assignees
No one assigned
Labels
Z-EndToEndBenchCI Tag a PR to run benchmark CI
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Compilation error when using string in assert
2 participants
@sintemal @zhassan-aws