search

model-checking / kani

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

Adding support for code coverage #2795

Open mahircg-aws opened 1 year ago

mahircg-aws commented 1 year ago

Requested feature: It would be useful for kani --coverage to report coverage percentage

Use case: As it stands, kani --coverage reports line coverage to indicate which lines are covered by a specific testing harness. It would be useful for the coverage feature to generate code coverage percentage to indicate the percentage of lines covered in a function (#lines_covered/#total_lines), potentially also to include branch coverage that takes control-flow into account.

adpaco-aws commented 1 year ago

Thanks @mahircg-aws for opening this feature request!

@mahircg-aws also mentioned to me that pytest has an intuitive coverage output for coverage metrics: https://coverage.readthedocs.io/en/7.3.1/

A similar output could be added to Kani.