VerCors usage & debugging cheatsheet

Information & questions

https://github.com/utwente-fmt/vercors/wiki

If you're doing a project with VerCors, ask us about the VerCors community chat.

Getting VerCors up and running

Required: at least java 11

Pre-build

• Download latest release (1.3.0 at the time of writing, doesn't work on windows)
• Download the build from the dev branch. Download the .tgz file, it contains a bat script for windows as well. Very likely works, but no guarantee

Should be just unzip and go.

Compile from source

Requires java 11 & sbt. Benefits: allows setting breakpoints in intellij. See VerCors README/Wiki for details.

General usage

vercors inputFile.java --backend

Where backend can be either silicon or carbon.

General flags

Of course, --help

Backends: --carbon (slower, but based on boogie, so sometimes more powerful), --silicon (faster, built by ETH Zurich, sometimes not as smart as Carbon)

Progress printing of individual passes: --progress

Slows down execution but prints more debug info upon crashes: --debug vct.main.Main

Triggers a system notification upon completion: --notify

Advanced verification flags

Detection of unsound preconditions

Flag: --disable-sat

Turns off detection of unsound preconditions. Not needed in general use of VerCors. Might be necessary if you have a lot of foralls in preconditions, and verification is slow.

Java example:

class C {
    //@ requires 1 == 2; // <-- Normally this causes an error, --disable-sat turns this off    
    void m() {

    }
}

Debugging flags

Flags: --show-before passName, --show-after passName

Show textual representation of internal AST before and after a pass. Pass names can be seen by running VerCors with --progress.

VSCode plugin + flags needed

Dump AST given to silicon/carbon into a text file: --encoded temp.sil

This can be opened in VScode with the ETH Zurich Viper plugin/extension installed (see the vscode store for this).

Note:

• The viper version between VerCors and vscode might be out of sync
• The vscode plugin has a 100 second timeout (though it can be turned off)
• The vscode plugin caches results in a wrong way sometimes (this can also be turned off)

Some starter example files

• In the example folder in the repository:
  • basic/BasicAssert-e1.java
  • parallel/block-par.pvl
  • demo/demo1.pvl, demo/demo2.pvl
• All examples in the wiki/tutorial