-
Notifications
You must be signed in to change notification settings - Fork 148
Back to Milestones
Coverage reports
OpenApr 1, 2026
No due date
•Last updated A milestone to capture pending issues for the new coverage reports feature, discussed in model-checking/kani#2612 and first implemented in model-checking/kani#2609
0% complete
List view
0 of 18 selected 0 issues of 18 selected
Improve tests for coverage
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Open.#2635 In model-checking/kani;Create user-friendly output for coverage
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Open.#2636 In model-checking/kani;Export coverage results to a well-supported output
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Open.#2638 In model-checking/kani;Avoid confusing results in coverage reports
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Open.#2639 In model-checking/kani;Report source-based coverage results
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Open.#2640 In model-checking/kani;Create a tool for aggregating coverage results
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Open.#2641 In model-checking/kani;Investigate how coverage checks affect performance
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Open.#2642 In model-checking/kani;Generate GCOV coverage output from
cargo kani[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.T-UserTag user issues / requestsTag user issues / requestsStatus: Open.#1706 In model-checking/kani;Generate LCOV coverage
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.T-UserTag user issues / requestsTag user issues / requestsStatus: Open.#1777 In model-checking/kani;Adding support for code coverage
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.T-UserTag user issues / requestsTag user issues / requestsStatus: Open.#2795 In model-checking/kani;Standalone assert statements lose information when converted to the irep format
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.Status: Open.Kani crashes when coverage is enabled and an unwind assertion fails
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.Status: Open.#3070 In model-checking/kani;Rust's coverage instrumentation assumes function calls never panic
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[F] SoundnessKani failed to detect an issueKani failed to detect an issueZ-UnstableFeatureIssues that only occur if a unstable feature is enabledIssues that only occur if a unstable feature is enabledStatus: Open.Coverage metadata should include mappings for all source code
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.Status: Open.#3445 In model-checking/kani;Filenames stored in raw coverage results should be absolute
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Open.#3542 In model-checking/kani;Documentation: Add a "Debugging coverage" section
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Open.#968 In model-checking/kani;Automatically check test coverage, and block PRs that decrease coverage.
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Open.#888 In model-checking/kani;kani-covis not documented[C] DocumentationAdditions and improvements to our documentationAdditions and improvements to our documentation[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Open.#3987 In model-checking/kani;