Home

Welcome to the Viper IDE User Documentation

Viper IDE is a visual environment for developing and verifying programs in the Viper language. It is built as an extension of Microsoft's Visual Studio Code, on top of the Viper command line tools.

Table of Contents

• Installation
  • Installing Viper IDE with binary packages
  • Installing Viper IDE with package managers
• Working with Viper IDE

Installation

Further we assume that Java Runtime Environment is installed and the java command is accessible in the default environment. Make sure to have Java 11 64-bit (preferably with the JavaServer component installed). Both Oracle JDK and OpenJDK are supported.

Installing Viper IDE with binary packages

1. Install the latest version of Visual Studio Code: https://code.visualstudio.com/Download

2. Run VS Code, open the extensions interface (View→Extensions), and search for an extension called Viper. After the Viper extension is installed, click Enable and agree to restart the VS Code application.

3. Viper IDE will be activated once a .vpr file is opened.

4. Viper IDE will ask for permission to download the necessary dependencies.

    If something went wrong, continue reading. 

The dependencies are installed to <VSCode Installation>/User/globalStorage/viper-admin.viper, where <VSCode Installation> usually corresponds to:

• c:\Users\<user>\AppData\Roaming\Code on Windows
• ~/.config/Code on Linux
• ~/Library/Application Support/Code on macOS

Within the viper-admin.viper folder, Viper IDE creates subfolders for Stable and Nightly releases of its dependencies. If you do not want to use released versions of the dependencies, you can change the Viper IDE settings to use build version Local. In this configuration, Viper IDE looks at a fully customizable location for the dependencies. More information can be found here.

Working with Viper IDE

1. After the first launch on Windows, you will be asked for restarting the IDE. Press Restart Now.

   

2. After restarting, Viper IDE shows an empty file. You can either type your new Viper program in it, or open an existing one (as a separate .vpr file, or as a project folder containing any number of .vpr files).

   

3. In this demo, we open the main.vpr file from the viper-example-project folder, which is located in the same archive as the portable distribution. Verification starts automatically, and we get the verification failure as a result.

   Note: due to a known bug (issue #16) in the extension, the current MacOS X app requires manually starting verification after opening a new file and after selecting a verification back end.

   

4. In order to get the message from the verifier, one could hover the cursor over the erroneous part of the source code (underlined with the red squiggly line), as shown on the picture below.

   

5. The list of all verification results could be accessed through the button. The list will appear at the top of the window. Clicking on a verification result will shift the focus towards the corresponding error in the sources.

   

6. One could get the complete list of supported commands by typing viper in the command palette (View→Command Palette...). Currently we support 3 commands:

   1. select verification back end — two back ends are supported: Silicon (default, based on symbolic execution) and Carbon (based on Microsoft Boogie).
   2. stop the running verification — especially useful for long-running examples or non-terminating verification, e.g., caused by matching loops.
   3. verify the opened document — manual verification.

   

7. Selecting a back end automatically invokes a new verification of the current file.

   

8. Sometimes, the verification back end generates an unparsable output which might cause the extension to detect an Internal error or even crash. In order to get the full information from the system, one should set the maximum logging depth in the user settings. This could be done with the following steps:

   1. Open the command palette (View→Command Palette...).
   2. Start typing Settings.
   3. Select the following command: Preferences: Open User Settings.
   4. This will open two editor panels side-by-side. The left one contains default settings and is non-modifiable, whereas the right one in for user-specific settings.
   5. Find the following setting: viperSettings.logLevel and change its value from 1 to 5. The new settings are active immediately after they are saved.
   6. Close the settings and return to the problematic example.
   7. Open the extension's output panel (View→Toggle Output).
   8. Select the output Viper from the list on the right of the panel, as shown on the picture below.