search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.13k stars 83 forks source link

Generate GCOV coverage output from `cargo kani` #1706

Open allenste-aws opened 1 year ago

allenste-aws commented 1 year ago

Requested feature: Generate GCOV coverage output from cargo kani --visualize Use case: GCOV coverage reports are integrated with our CI framework and Code review tools. We can fail builds if coverage drops. Reviewers can see what lines have not been covered by tests and proofs.

tedinski commented 1 year ago

Absolutely good idea.

Just some additional background:

The rust book has a section on coverage (https://doc.rust-lang.org/rustc/instrument-coverage.html) which states:

The Rust compiler includes two code coverage implementations:

  • A GCC-compatible, gcov-based coverage implementation, enabled with -Z profile, which derives coverage data based on DebugInfo.
  • A source-based code coverage implementation, enabled with -C instrument-coverage, which uses LLVM's native, efficient coverage instrumentation to generate very precise coverage data.

So between it seeming to be a Rust thing and user request, gcov seems like a good option. But we should consider whether the other format should be supported as well. So far I haven't found good documentation about what's "typical" out there for Rust projects, in terms of measuring test coverage...

carolynzech commented 1 week ago

Closing this since we are now deprecating --visualize option.

carolynzech commented 1 week ago

Reopening with --visualize removed from title instead.