Viper IDE Documentation

Setting up Viper IDE

Verification backends

Viper comes with two, equally powerful verification backends with complementary advantages.

• Silicon: the symbolic execution backend for the Viper language
• Carbon: the verification condition generation backend for the Viper language

The default backend in Viper IDE is Silicon, but it is easy to switch between the two (⇧+Ctrl+X or ⇧+⌘+X):

• Viper: select verification backend

Caching

By-default, Viper IDE tries to cache verification results obtained for each method. When the verifier re-uses verification errors from the cache, it adds the label "(cached)" to the corresponding message. Because the cache is stored in program memory (not on the disk), it will be lost as soon as you close VS Code.

Managing the cache

In order to make sure that the most-recent version of the Viper program types into VS Code produces an expected result, it is sometimes convenient to run verification without consulting the cache. For this reason, Viper IDE provides the following two commands:

• Viper: flush the cache
• Viper: flush the cache for this file

The first command will discard the cache for all Viper files that have been verified in the current VS Code window. The second command will discard the cache only for the currently active Viper file. Note that verification results obtained after flushing the cache will start being cached again.

Disabling caching

In some scenarios, it is desirable to entirely switch off caching. This can be done by ensuring the following VS Code settings:

    "viperSettings.viperServerSettings": {
        "v": "674a514867b1",
        "disableCaching": true,
    }

After saving these settings, Viper IDE will not consult the cache anymore, for all new verification requests.

Backend-specific cache

Sometimes it is convenient to use different caches for different Viper backends, e.g., one for Carbon and one for Silicon. To enable this feature, ensure the following VS Code settings:

    "viperSettings.viperServerSettings": {
        "v": "674a514867b1",
        "backendSpecificCache": true,
    }

The effect takes place immediately after saving these settings. Note that changing these settings will not affect the existing cache; in particular, Viper will still remember the verification results cached earlier in the session, but it will only attempt to reuse these results if they match the currently active verification backend.