The Vienna Verification Toolkit is comprised of the following components:
- smtlib2 provides an common interface to various SMT solvers.
- bindings-llvm is a low-level binding to the LLVM API for Haskell.
- vvt contains all the programs of the Vienna Verification Toolkit.
As a prequisite, you need to have a recent (version 7.8 or higher) GHC compiler and the cabal-install tool installed. The easiest way to grab both of them is to download and install the Haskell Platform. You further need to install version 3.5 of the LLVM framework and the clang compiler.
The first step is to build the SMTLib interface:
git clone https://github.com/hguenther/smtlib2.git cd smtlib2 cabal install cd backends/timing cabal install cd backends/debug cabal install cd extras/emulated-modulus cabal install cd ../..
The next step is to install the LLVM bindings. Usually this is just a simple
git clone https://github.com/hguenther/bindings-llvm.git cd bindings-llvm cabal install
However, if your LLVM installation is at an unusual place or you have different versions installed, it might be necessary to adjust the path to the llvm-config binary:
runghc Setup.hs configure --with-llvm-config=PATH runghc Setup.hs build runghc Setup.hs install
Lastly, we install the toolkit:
git clone https://github.com/hguenther/vvt.git cd vvt cabal install