- A virtual machine containing the runnable system; if password needed, it is “hifrog”
- Preliminary evaluation reports are available here.
- Benchmarks available here whcih are mostly taken from SV-COMP16 and SV-COMP15.
Compiling HiFrog 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
$ 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
** If you need any assistance, please contact us **
sepideh.a65[at]gmail.com