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

library/kani/src/lib.rs

@@ -74,15 +74,18 @@ pub use core::assert as __kani__workaround_core_assert;
 
 #[macro_export]
 macro_rules! cover {
-    () => {
+    // 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.
+    () => {{
         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

library/std/src/lib.rs

@@ -84,10 +84,13 @@ 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
+        // 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.
         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

tests/kani/Macros/assert_cover_in_expression_position.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that Kani's `assert!` and `cover!` macros can be used in expression
+//! position (e.g. as `match` arms) without tripping the future-incompatible
+//! `semicolon_in_expressions_from_non_local_macros` lint on the user's code.
+
+#![deny(semicolon_in_expressions_from_non_local_macros)]
+
+#[kani::proof]
+fn check_macros_in_expression_position() {
+    let x: u8 = kani::any();
+    let _r = match x {
+        0 => assert!(x == 0),
+        _ => kani::cover!(x > 0),
+    };
+    let _s = if x > 3 { assert!(x > 3, "x is large") } else { kani::cover!() };
+    let _t = if x == 7 { kani::cover!(x == 7, "seven") } else { assert!(x != 7) };
+}