This Visual Studio Code extension provides interactive IDE features for verifying Rusti programs with the Prusti verifier.
In order to use this extension, please install the following components:
- Install the requirements (listed above). Restart Visual Studio Code to make sure that
rustup is in the program path used by the IDE.
- Install the "Prusti Assistant" extension in Visual Studio Code.
- Open a Rust file to activate the extension. At its first activation, this extension will automatically download Prusti and install the required Rust toolchain.
To verify a Rust program, open the command palette (View -> Command Palette, or Shift+Ctrl+P on Ubuntu) and run the command
Prusti: save and verify this file. You should see a "Running Prusti..." message in the status bar while Prusti is running. When Prusti terminates the result of the verification is reported in the status bar and in the "Problems" tab (open it with View -> Problems).
To automatically run Prusti when a Rust file is opened or saved, enable the corresponding flag in the settings (Preferences -> Settings -> type "Prusti" -> enable "Verify On Open" and "Verify On Save").
To update Prusti run the command
Prusti: update dependencies in the command palette.
Inline Code Diagnostics
This extension automatically provides inline diagnostics for Rust by running Prusti and parsing its output.
This extension provides the following commands:
Prusti: save and verify this file to verify a Rust program;
Prusti: update dependencies to update Prusti.
Prusti: restart Prusti server to restart the Prusti server used by this extension.
Basic code-completion snippets are provided for Prusti annotations.
The main configuration options used by this extension are the following:
prusti-assistant.verifyOnSave: Specifies if programs should be verified on save.
prusti-assistant.verifyOnOpen: Specifies if programs should be verified when opened.
prusti-assistant.buildChannel: Allows to choose between the latest Prusti release version (the default) and a slightly newer but potentially unstable Prusti development version.