From fc25a4a06a83b84ec3a113cb0c4a3e842c0b489f Mon Sep 17 00:00:00 2001
From: Trevor Campbell <55037769+trevordcampbell@users.noreply.github.com>
Date: Fri, 25 Sep 2026 20:10:36 -0400
Subject: [PATCH 1/2] Fix no-message assert expansion in expression contexts

Emit an explicit block expression so strict warnings do not reject the
no-message assert macro in constant and other expression positions.
Add focused regression coverage for expression forms, single evaluation,
and an expected assertion failure.

Fixes model-checking/kani#4874
---
 library/std/src/lib.rs                   |  4 +--
 tests/kani/Assert/expression_contexts.rs | 40 ++++++++++++++++++++++++
 2 files changed, 42 insertions(+), 2 deletions(-)
 create mode 100644 tests/kani/Assert/expression_contexts.rs

diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs
index 694e2eb4b1ef..d60ab5de21da 100644
--- a/library/std/src/lib.rs
+++ b/library/std/src/lib.rs
@@ -84,10 +84,10 @@ pub mod prelude {
 #[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! assert {
-    ($cond:expr $(,)?) => {
+    ($cond:expr $(,)?) => {{
         // The double negation is to resolve https://github.com/model-checking/kani/issues/2108
         kani::assert(!!$cond, concat!("assertion failed: ", stringify!($cond)));
-    };
+    }};
     // Before edition 2021, the `assert!` macro could take a single argument
     // that wasn't a string literal. This is not supported in edition 2021 and above.
     // Because we reexport the 2021 edition macro, we need to support this
diff --git a/tests/kani/Assert/expression_contexts.rs b/tests/kani/Assert/expression_contexts.rs
new file mode 100644
index 000000000000..41b167a6764f
--- /dev/null
+++ b/tests/kani/Assert/expression_contexts.rs
@@ -0,0 +1,40 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Regression for https://github.com/model-checking/kani/issues/4874:
+//! No-message assertions must expand to expressions without trailing semicolons.
+
+#![deny(warnings)]
+
+const _: () = assert!(true);
+const _: () = const { assert!(true) };
+
+fn require_unit(_: ()) {}
+
+#[kani::proof]
+fn expression_contexts() {
+    assert!(true);
+    let () = assert!(true);
+    require_unit(assert!(true,));
+    let () = { assert!(true) };
+    match kani::any::<bool>() {
+        true => assert!(true),
+        false => assert!(true,),
+    }
+}
+
+#[kani::proof]
+fn condition_is_evaluated_once() {
+    let mut evaluations = 0u8;
+    assert!({
+        evaluations += 1;
+        true
+    });
+    assert_eq!(evaluations, 1);
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn false_assertion_still_fails() {
+    assert!(false);
+}

From cb23c2070d1c5a68319d23e2118a150e85036f82 Mon Sep 17 00:00:00 2001
From: Trevor Campbell <55037769+trevordcampbell@users.noreply.github.com>
Date: Mon, 28 Sep 2026 00:18:08 -0400
Subject: [PATCH 2/2] Fix cover macro expression expansions and document
 assertion block

Wrap all three cover macro arms in explicit unit-valued blocks and add
an expected-output regression for emitted properties and single evaluation.
Explain the assertion macro braces requested in review.
---
 library/kani/src/lib.rs                       | 12 +++++------
 library/std/src/lib.rs                        |  1 +
 .../cover/expression-contexts/expected        | 15 +++++++++++++
 .../cover/expression-contexts/main.rs         | 21 +++++++++++++++++++
 4 files changed, 43 insertions(+), 6 deletions(-)
 create mode 100644 tests/expected/cover/expression-contexts/expected
 create mode 100644 tests/expected/cover/expression-contexts/main.rs

diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 74c53363d390..492f46bb26a8 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -72,15 +72,15 @@ pub use core::assert as __kani__workaround_core_assert;
 
 #[macro_export]
 macro_rules! cover {
-    () => {
+    () => {{
         kani::cover(true, "cover location");
-    };
-    ($cond:expr $(,)?) => {
+    }};
+    ($cond:expr $(,)?) => {{
         kani::cover($cond, concat!("cover condition: ", stringify!($cond)));
-    };
-    ($cond:expr, $msg:literal) => {
+    }};
+    ($cond:expr, $msg:literal) => {{
         kani::cover($cond, $msg);
-    };
+    }};
 }
 
 /// `implies!(premise => conclusion)` means that if the `premise` is true, so
diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs
index d60ab5de21da..5483cad38729 100644
--- a/library/std/src/lib.rs
+++ b/library/std/src/lib.rs
@@ -85,6 +85,7 @@ pub mod prelude {
 #[macro_export]
 macro_rules! assert {
     ($cond:expr $(,)?) => {{
+        // Emit a block expression so assert! works in expression positions (#4874).
         // The double negation is to resolve https://github.com/model-checking/kani/issues/2108
         kani::assert(!!$cond, concat!("assertion failed: ", stringify!($cond)));
     }};
diff --git a/tests/expected/cover/expression-contexts/expected b/tests/expected/cover/expression-contexts/expected
new file mode 100644
index 000000000000..6f000411e92f
--- /dev/null
+++ b/tests/expected/cover/expression-contexts/expected
@@ -0,0 +1,15 @@
+Status: SATISFIED\
+Description: "cover location"\
+main.rs:16:17 in function cover_expression_contexts
+
+Status: SATISFIED\
+Description: "cover condition: counted_true(&mut evaluations)"\
+main.rs:17:17 in function cover_expression_contexts
+
+Status: UNSATISFIABLE\
+Description: "unsatisfiable cover condition"\
+main.rs:18:17 in function cover_expression_contexts
+
+ ** 2 of 3 cover properties satisfied
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/cover/expression-contexts/main.rs b/tests/expected/cover/expression-contexts/main.rs
new file mode 100644
index 000000000000..379bf299e9cf
--- /dev/null
+++ b/tests/expected/cover/expression-contexts/main.rs
@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#![deny(warnings)]
+
+fn counted_true(evaluations: &mut u8) -> bool {
+    *evaluations += 1;
+    *evaluations == 1
+}
+
+// Regression for #4874: expression-position cover! calls must still emit coverage properties.
+#[kani::proof]
+fn cover_expression_contexts() {
+    let mut evaluations = 0;
+
+    let _: () = kani::cover!();
+    let _: () = kani::cover!(counted_true(&mut evaluations),);
+    let _: () = kani::cover!(false, "unsatisfiable cover condition");
+
+    assert!(evaluations == 1);
+}