Update docs before 0.0.6 release (adds coverage to user guide)

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.
 

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.