diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 1f6472eee8cb..7a46535093e4 100644 --- a/library/kani/src/lib.rs +++ b/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 diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs index 694e2eb4b1ef..5483cad38729 100644 --- a/library/std/src/lib.rs +++ b/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 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); +} 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::() { + 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); +}