Viper mode for Emacs

Viper language support for Emacs.

Dependencies

• Z3 (tested with versions 4.8.7 and 4.12.1)
• Boogie (for using carbon as a backend)
• ViperServer

Installation

This package is under heavy development and does not support all Viper features. Thus, it is not published in any package archives.

To install it, one must clone the repository:

git clone git@github.com:viperproject/vpr-mode.git

Then, add the following lines in your init.el.

(add-to-list 'load-path "<vpr-mode path>")

(use-package vpr-mode)

Last the following variables must be set

(setq vpr-z3-path "<path/to/z3 exe>")
(setq vpr-viperserver-path "/path/to/viperserver.jar")
(setq vpr-boogie-path "<path/to/boogie exe>") ; required only for running viper with carbon

If you want the verification to happen on save:

(add-hook 'after-save-hook #'vpr-verify)

Note that the name of the mode is vpr-mode to not clash with the built-in viper-mode.

Usage

Current keybindings are:

• C-c C-c: Start Viper server
• C-c C-v: Verify this file
• C-c C-x: Stop Viper server
• C-c C-b: Alternate the backend between silicon and carbon
• C-c C-a: Edit the arguments given to Viper through a construction buffer

Who do I talk to?

This project is maintained by Dionisios Spiliopoulos