inference-for-viper README

This extension enables Visual Studio Code to perform formal specification inference in Viper programs based on abstract interpretation.

Features

This extension works nicely with the Viper extension for Visual Studio Code.

1. Open a Viper program without contracts;
2. Select Infer Viper specifications in the command palette;
3. Observe your code augmented with formal specifications;
4. Run the Viper verifier to chack if the program verifies against the inferred specs.

Requirements

1. You need to download sample-silver.jar and place it in a local directory, e.g., /usr/local/Viper/sample/sample-silver.jar.

2. Specify the path to sample-silver.jar in the User Settingsm e.g.:

    {
        "inference-for-viper.path": "/usr/local/Viper/sample/sample-silver.jar"
    }
   

TODO: add permalink.

Extension Settings

This extension contributes the following settings:

• inference-for-viper.path: path to the inference backend (typically called sample-silver.jar).

Known Issues

Please file bug reports and requests here: https://bitbucket.org/viperproject/inference-for-viper-ide/issues