/vpr-mode

Language highlighting for viper

Primary LanguageEmacs LispMozilla Public License 2.0MPL-2.0

This project has been moved to vpr-mode

viperlanguage-mode

Viper language support for Emacs.

Installation

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

For the moment, the package uses viper through silicon with the default arguments.

To install it, one must clone the repository:

git clone git@github.com:Dspil/viperlanguage-mode.git

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

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

(use-package viperlanguage-mode)

(setq viperlanguage-viper-path "<viper path>")
(setq viperlanguage-z3-path "<path to Z3>")
(setq viperlanguage-boogie-path "<path to Boogie>")

If you want the verification to happen on save:

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

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