Fix assert! and cover! expansions in expression contexts

library/kani/src/lib.rs

@@ -74,15 +74,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

library/std/src/lib.rs

@@ -84,10 +84,11 @@ pub mod prelude {
 #[cfg(not(feature = "concrete_playback"))]
 #[macro_export]
 macro_rules! assert {
-    ($cond:expr $(,)?) => {
+    ($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)));
-    };
+    }};
     // 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/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

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);
+}

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);
+}