Skip to content

Commit 8a99568

Browse files
author
Carolyn Zech
committed
update docs
1 parent 69f376b commit 8a99568

File tree

2 files changed

+3
-10
lines changed

2 files changed

+3
-10
lines changed

README.md

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,6 @@ NOTE: The extension only works on Cargo packages. For standalone Rust files, Kan
3333
| :-------------------------------- | :------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | :------------------------------------------------------------- |
3434
| `kani.enable-codelens` | Enable Codelens actions for `Run Test (Kani)` & `Debug Test (Kani)`. | `true` |
3535
| `kani.show-output-window` | Toggle to show the output terminal window containing the full output from Kani. | `false` |
36-
| `kani.highlight-coverage` | Toggle to enable the codelens button for `Generage Coverage` by default. | `false`
3736

3837
## Installation
3938

docs/user-guide.md

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -75,23 +75,17 @@ For every test run, you can view the full output from Kani logged into the outpu
7575

7676
### Coverage information
7777

78-
Line-based coverage information can be displayed for any harness as in:
78+
Source-based coverage information can be displayed for any harness as in:
7979

8080
![Coverage information](../resources/screenshots/coverage-info.png)
8181

82-
To enable the coverage feature in the extension, toggle on the `Codelens-kani: Highlight Coverage` setting in `Settings > Extensions > Kani`.
83-
8482
#### View coverage information
8583

8684
Once the coverage feature is enabled, the `Get coverage info` action should be visible on top of each Kani harness in the project.
8785
Running the `Get coverage info` highlights all lines for which coverage information was obtained.
8886

89-
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:
90-
- **Green:** Indicates `FULL` coverage.
91-
- **Yellow:** Indicates `PARTIAL` coverage.
92-
- **Red:** Indicates `NONE` coverage.
93-
94-
**NOTE**: Line-based coverage information is an unstable feature.
87+
Coverage information (as described in the [RFC for source coverage](https://model-checking.github.io/kani/rfc/rfcs/0011-source-coverage.html#user-experience)) is represented by highlighting the portion of the line that is covered.
88+
Red means that that portion is not covered; green means that it is covered.
9589

9690

9791
#### De-highlight coverage information

0 commit comments

Comments
 (0)