Error when using assert in a match arm #1572
Description
I tried this code:
enum Foo {
A,
B,
}
#[cfg_attr(kani, kani::proof)]
fn main() {
let f = Foo::A;
match f {
Foo::A => assert!(1 + 1 == 2, "Message"),
Foo::B => panic!("Failed"),
}
}using the following command line invocation:
kani assert_in_match.rs
with Kani version:
I expected to see this happen: Verification succeeded
Instead, this happened:
$ kani assert_in_match.rs
error: macro expansion ignores token `if` and any following
--> /home/ubuntu/git/kani/library/std/src/lib.rs:56:9
|
56 | if false {
| ^^
|
::: assert_in_match.rs:10:19
|
10 | Foo::A => assert!(1 + 2 == 2, "Message"),
| ------------------------------- help: you might be missing a semicolon here: `;`
| |
| caused by the macro expansion here
|
= note: the usage of `assert!` is likely invalid in expression context
error: aborting due to previous error
Error: "Failed to compile crate."
Error: /home/ubuntu/git/kani/target/debug/kani-compiler exited with status exit status: 1