Skip to content

Make assert! and cover! expand to blocks so they work in expression position - #4897

Closed
tautschnig wants to merge 1 commit into
model-checking:mainfrom
tautschnig:assert-cover-block-expansion
Closed

tautschnig wants to merge 1 commit into
model-checking:mainfrom
tautschnig:assert-cover-block-expansion

Conversation

@tautschnig

Copy link
Copy Markdown
Member

Kani's assert! (std override) and cover! macros expand to a statement with a trailing semicolon. Used in expression position, e.g. as a match arm, this triggers the future-incompatible semicolon_in_expressions_from_non_local_macros warning in the user's code (the lint's local-macro counterpart, semicolon_in_expressions_from_macros, is already deny-by-default). Wrap the expansions in blocks.

Add a regression test, tests/kani/Macros/assert_cover_in_expression_position.rs, that denies the lint; it fails without the fix.

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

…osition

Kani's `assert!` (std override) and `cover!` macros expand to a statement
with a trailing semicolon. Used in expression position, e.g. as a `match`
arm, this triggers the future-incompatible
`semicolon_in_expressions_from_non_local_macros` warning in the user's code
(the lint's local-macro counterpart, `semicolon_in_expressions_from_macros`,
is already deny-by-default). Wrap the expansions in blocks.

Add a regression test that denies the lint.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
@tautschnig
tautschnig requested review from a team as code owners September 28, 2026 15:25
Copilot AI lite review requested due to automatic review settings September 28, 2026 15:25
@github-actions github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Sep 28, 2026

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copilot review overview

🟢 Approval recommended

The changes are reviewed and remaining comments are minor documentation nits.

Review effort: Lite
Findings: 2 Low severity

Open (2)
What changed in this PR

Updates Kani’s assert! and cover! macros to expand as blocks, avoiding semicolon lint warnings in expression positions.

Changes:

  • Wraps assert! and cover! expansions in blocks.
  • Adds regression coverage for match arms and conditional expressions.
File Summary
tests/​kani/​Macros/​assert_cover_in_expression_position.rs Adds expression-position regression coverage.
library/​std/​src/​lib.rs Updates assert! expansion.
library/​kani/​src/​lib.rs Updates cover! expansions.

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

Comment thread library/kani/src/lib.rs
Comment on lines +77 to +79
// The block wrapper keeps the expansion valid in expression position (e.g. as a
// `match` arm): a trailing semicolon there triggers the future-incompatible
// `semicolon_in_expressions_from_macros` lint in user code.
Comment thread library/std/src/lib.rs
Comment on lines +89 to +91
// The block wrapper keeps the expansion valid in expression position (e.g. as a
// `match` arm): a trailing semicolon there triggers the future-incompatible
// `semicolon_in_expressions_from_macros` lint in user code.
@feliperodri

Copy link
Copy Markdown
Member

what is the difference between this PR and #4875? @tautschnig

@tautschnig

Copy link
Copy Markdown
Member Author

Closing in favour of #4875.

@tautschnig tautschnig closed this Sep 29, 2026
@tautschnig
tautschnig deleted the assert-cover-block-expansion branch September 29, 2026 13:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants