Skip to content

Commit cd0e916

Browse files
author
Carolyn Zech
committed
update docs
1 parent 5bfe917 commit cd0e916

File tree

1 file changed

+3
-9
lines changed

1 file changed

+3
-9
lines changed

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)