Compile HiFrog and OpenSMT for Theory Refinement

1. First, install OpenSMT2 as a library to be used in HiFrog binary; configure & install OpenSMT2 as follows:

OpenSMT2 depends on the following libraries:

  • zlib
  • gmp
  • gmpxx
  • readline
  • flex

Guideline to install the requirements:

sudo apt-get update

sudo apt-get install gcc-6

sudo apt-get install g++-6

sudo rm /usr/bin/cpp /usr/bin/gcc /usr/bin/g++

sudo ln -s /usr/bin/cpp-6 /usr/bin/cpp

sudo ln -s /usr/bin/gcc-6 /usr/bin/gcc

sudo ln -s /usr/bin/g++-6 /usr/bin/g++

sudo apt-get install libtool

sudo apt-get install bison flex

sudo apt-get install autoconf

sudo apt-get install git-all

 

Guideline to Install GMP:

wget ftp://ftp.gmplib.org/pub/gmp/gmp-6.1.2.tar.xz

tar Jxvf gmp-6.1.2.tar.xz

cd gmp-6.1.2

./configure --enable-cxx

make

make check

sudo make install

 

2. Compile OpenSMT2 for theory refinement as in the following:

$ git clone -b opensmt_SAT2017 https://scm.ti-edu.ch/repogit/opensmt2.git

Enter the opsntm2 folder and run the configure script:

$ cd opensmt2
$ autoreconf --force --install
$ ./configure

Then run make and install.

$ make
$ sudo make install

3. Download HiFrog:

​  $ git clone -b Theoref_SAT2017 https://scm.ti-edu.ch/repogit/hifrog

4. Compile Cprover framework in HiFrog repository:

   $ cd hifrog/trunk/cprover/src; make clean; make
4. Compile HiFrog. 
   $ cd funfrog; make clean; make -f Makefile-no-itp

A small hint: During the compilation, if you happen to see such message "make: *** No rule to make target `../cpp/cpp.a', needed by `hifrog'. Stop.", please do "make" in the mentioned directory. Then again do make in funfrog directory.

Run HiFrog to use theory refinement algorithm.

./hifrog --theoref --bitwidth <n> --heuristic <n> --unwind <n> --claim <n> --custom <ids> <your code-to-verify>

./hifrog --theoref --bitwidth 32 --unwind 10 --heuristic 4 --claim 1 filename.c



You may read on the parameters: heuristic, unwind, claim and custom on ./hifrog --help

 

The git repository we use for HiFrog is hosted at https://scm.ti-edu.ch/projects/hifrog.

 

 

** If you need any assistance, please contact us **

sepideh.a65[at]gmail.com