diff --git a/README.md b/README.md index b542f0f..55b2f85 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # Kani Visual Studio Code Extension -A [Visual Studio Code](https://code.visualstudio.com/) extension that allows users to run and debug their [Kani Rust Verifier](https://github.com/model-checking/kani) harnesses in vscode. +A [Visual Studio Code](https://code.visualstudio.com/) extension that allows users to run and debug their [Kani Rust Verifier](https://github.com/model-checking/kani) harnesses in VS Code. ## Usage @@ -22,7 +22,7 @@ Check [user guide](docs/user-guide.md) for more detailed information. ## Requirements - [Visual Studio Code](https://code.visualstudio.com/) 1.50 or newer -- [Kani](https://github.com/model-checking/kani) 0.29 or newer +- [Kani](https://github.com/model-checking/kani) 0.34 or newer NOTE: The extension only works on Cargo packages. For standalone Rust files, Kani is only available on the command line. diff --git a/docs/user-guide.md b/docs/user-guide.md index 87201f5..659c737 100644 --- a/docs/user-guide.md +++ b/docs/user-guide.md @@ -16,6 +16,8 @@ This guide provides the various workflows that you can use to verify and debug y - [View trace report in window](#view-trace-report-in-window) - [Kani output logging](#kani-output-logging) - [View full Kani output](#view-full-kani-output) +- [Coverage information](#coverage-information) + - [View coverage information](#view-coverage-information) ### Verify Kani harnesses @@ -81,7 +83,7 @@ By clicking the `Generate report for (your harness)` option in the error banner, You can click on the `Preview in Editor` button to view the HTML trace within VSCode. It should look like this: -![Generate Report](../resources/screenshots/view-report.png) +![View Report](../resources/screenshots/view-report.png) ### Kani output logging @@ -91,3 +93,23 @@ It should look like this: For every test run, you can view the full output from Kani logged into the output channel as a text file. To view the log, open the output channel, and click on the channel drop down list to view a channel called `Output (Kani): ...` ![Generate Report](../resources/screenshots/view-output.png) + +### Coverage information + +Line-based coverage information can be displayed for any harness as in: + +![Coverage information](../resources/screenshots/coverage-info.png) + +To enable the coverage feature in the extension, toggle on the `Codelens-kani: Highlight Coverage` setting in `Settings > Extensions > Kani`. + +#### View coverage information + +Once the coverage feature is enabled, the `Get coverage info` action should be visible on top of each Kani harness in the project. +Running the `Get coverage info` highlights all lines for which coverage information was obtained. + +Coverage information (as described in the [RFC for line coverage](https://model-checking.github.io/kani/rfc/rfcs/0008-line-coverage.html#postprocessing-coverage-checks)) is represented with three colors: + - **Green:** Indicates `FULL` coverage. + - **Yellow:** Indicates `PARTIAL` coverage. + - **Red:** Indicates `NONE` coverage. + +**NOTE**: Line-based coverage information is an unstable feature. diff --git a/resources/screenshots/coverage-info.png b/resources/screenshots/coverage-info.png new file mode 100644 index 0000000..f539092 Binary files /dev/null and b/resources/screenshots/coverage-info.png differ