This Visual Studio Code extension provides interactive IDE features for verifying Rusti programs with the Prusti verifier.
For advanced use cases, consider switching to the command-line version of Prusti.
In order to use this extension, please install the following components:
- Install the requirements (listed above) and restart the IDE.
- This will ensure that programs like
rustup are in the program path used by the IDE.
- Install the "Prusti Assistant" extension.
- Open a Rust file to activate the extension.
- 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.
If something fails, check the "Troubleshooting" section below.
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: show version to show the version of 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.
If Prusti fails to run, you can inspect Prusti's log from VS Code (View -> Output -> Prusti Assistant) and see if one of the following solutions applies to you.
error[E0514]: found crate 'cfg_if' compiled by an incompatible version of rustc
|There is a conflict between Prusti and a previous Cargo compilation. Run
cargo clean or manually delete the
target folder. Then, rerun Prusti.
error: the 'cargo' binary, normally provided by the 'cargo' component, is not applicable to the 'nightly-2021-09-20-x86_64-unknown-linux-gnu' toolchain
error[E0463]: can't find crate for std
error[E0463]: can't find crate for core
|The Rust toolchain installed by Rustup is probably corrupted (see issue rustup/#2417). Uninstall the nightly toolchain mentioned in the error (or all installed nightly toolchains). Then, rerun Prusti.
Thanks to @Pointerbender for reporting issues and suggesting solutions!