Skip to content

Commit

Permalink
Remove picture
Browse files Browse the repository at this point in the history
  • Loading branch information
adpaco-aws committed Jul 26, 2023
1 parent 6cf2286 commit b2728e7
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 3 deletions.
Binary file removed rfc/src/images/0008/coverage-kani-vscode.png
Binary file not shown.
4 changes: 1 addition & 3 deletions rfc/src/rfcs/0008-line-coverage.md
Original file line number Diff line number Diff line change
Expand Up @@ -58,9 +58,7 @@ where `<status>` is either `FULL`, `PARTIAL` or `NONE`.
As mentioned, this format is designed for evaluating the [native instrumentation-based design](#detailed-design) and is likely to be substituted with another well-established format as soon as possible.

**Users are not expected to consume this output directly.**
Instead, coverage data is to be consumed by the [Kani VS Code extension](https://github.com/model-checking/kani-vscode-extension) and displayed as in the following picture:

![Coverage reported on the Kani VS Code Extension](../images/0008/coverage-kani-vscode.png)
Instead, coverage data is to be consumed by the [Kani VS Code extension](https://github.com/model-checking/kani-vscode-extension) and displayed as in [the VS Code Extension prototype](https://github.com/model-checking/kani-vscode-extension/pull/122).

How to activate and display coverage information in the extension is out of scope for this RFC.
That said, a proof-of-concept implementation is available [here](https://github.com/model-checking/kani-vscode-extension/pull/122).
Expand Down

0 comments on commit b2728e7

Please sign in to comment.