Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Confusing coverage result: Uncovered argument for match #3456

Open
adpaco-aws opened this issue Aug 20, 2024 · 0 comments
Open

Confusing coverage result: Uncovered argument for match #3456

adpaco-aws opened this issue Aug 20, 2024 · 0 comments
Labels
[C] Bug This is a bug. Something isn't working. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one. [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct. Z-UnstableFeature Issues that only occur if a unstable feature is enabled

Comments

@adpaco-aws
Copy link
Contributor

We noticed a confusing coverage result in #3119 where, for the code

fn print_direction(dir: Direction) {
    // For some reason, `dir`'s span is reported as `UNCOVERED` too
    match dir {
        Direction::Up => println!("Going up!"),
        Direction::Down => println!("Going down!"),
        Direction::Left => println!("Going left!"),
        Direction::Right if 1 == 1 => println!("Going right!"),
        // This part is unreachable since we cover all variants in the match.
        _ => println!("Not going anywhere!"),
    }
}

we get the result

main.rs (print_direction)\
 * 14:1 - 14:36 COVERED
 * 16:11 - 16:14 UNCOVERED
 * 17:26 - 17:47 UNCOVERED
 * 18:28 - 18:51 UNCOVERED
 * 19:28 - 19:51 COVERED
 * 20:34 - 20:63 UNCOVERED
 * 22:14 - 22:45 UNCOVERED
 * 24:1 - 24:2 COVERED

which is confusing because it reports the dir in match dir { as UNCOVERED. It's not clear to me why this is happening, but we should at least check if this is also the case for a standard execution with coverage.

@adpaco-aws adpaco-aws added the [C] Bug This is a bug. Something isn't working. label Aug 20, 2024
@adpaco-aws adpaco-aws added [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one. [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct. Z-UnstableFeature Issues that only occur if a unstable feature is enabled [C] Bug This is a bug. Something isn't working. and removed [C] Bug This is a bug. Something isn't working. labels Aug 21, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one. [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct. Z-UnstableFeature Issues that only occur if a unstable feature is enabled
Projects
None yet
Development

No branches or pull requests

1 participant