Skip to content

Latest commit

 

History

History
62 lines (36 loc) · 3.33 KB

README.md

File metadata and controls

62 lines (36 loc) · 3.33 KB
Raw

Kani Visual Studio Code Extension

A Visual Studio Code extension that allows users to run and debug their Kani Rust Verifier harnesses in vscode.

Usage

Kani Usage

  1. Open a Rust package in Visual Studio Code.
  2. Navigate to the testing panel and expand on the Kani harness tree view where the harnesses are shown.
  3. Click on the play button beside the harness or the filename or the crate to run Kani on the respective test case.

Check user guide for more detailed information.

Features

  • Automatically indexes and shows Kani harnesses in a tree view.
  • One-click button for verifying Kani harnesses.
  • Generate counterexamples as Rust unit tests.
  • Debug counterexamples using a standard debugger.

Requirements

NOTE: The extension only works on Cargo packages. For standalone Rust files, Kani is only available on the command line.

Extension Settings

Setting Description Default
kani.enable-codelens Enable Codelens actions for Run Test (Kani) & Debug Test (Kani). true
kani.show-output-window Toggle to show the output terminal window containing the full output from Kani. false

Installation

The Kani VSCode Extension is available as a VSCode plugin. You can install the Kani VSCode Extension from the Visual Studio Marketplace.

If you want to build and package from source directly, see dev-documentation for more information.

Troubleshooting

Check troubleshooting for frequently asked questions and potential fixes.

If you have a question that is not answered there, please file an issue with your question.

Security

See SECURITY for more information.

License

This code is distributed under the terms of both the MIT license and the Apache License (Version 2.0). See LICENSE-APACHE and LICENSE-MIT for details.

Code of conduct

This project has adopted the Rust Code Of Conduct. See CODE OF CONDUCT for details.