At its first activation, this extension will automatically download Prusti and install the required Rust toolchain.
Click on the "Verify with Prusti" button in the status bar.
Alternativelly, you can run the Prusti: verify the current crate or file command.
If the program is in a folder with a Cargo.toml file, Prusti will verify the crate in which the file is contained.
If no Cargo.toml file can be found in a parent folder of the workspace, Prusti will verify the file as a standalone Rust program. No Cargo dependencies are allowed in this mode.
Follow the progress from the status bar.
You should see a "Verifying crate [folder name]" or "Verifying file [name]" message while Prusti is running.
The result of the verification is reported in the status bar and in the "Problems" tab.
You can open the "Problems" tab by clicking on Prusti's status bar.
Be aware that the "Problems" tab is shared by all extensions. If you are not sure which extension generated which error, try disabling other extensions. (Related VS Code issue: #51103.)
To update Prusti, run the command Prusti: update verifier in the command palette.
This extension provides the following commands:
Prusti: verify the current crate or file to verify a Rust program;
Prusti: update verifier to update Prusti.
Prusti: restart Prusti server to restart the Prusti server used by this extension.
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.
prusti-assistant.checkForUpdates: Specifies if Prusti should check for updates at startup.
Inline Code Diagnostics
This extension automatically provides inline diagnostics for Prusti errors.
Basic code-completion snippets are provided for Prusti annotations.
Incompatible version of rustc
If after an upgrade you get the error "found crate [name] compiled by an incompatible version of rustc" while verifying a crate, run cargo clean or manually delete the target folder. Then, rerun Prusti.